Интерполяция Крейга

В математической логике интерполяционная теорема Крейга является результатом взаимосвязи между различными логическими теориями . Грубо говоря, теорема гласит, что если из формулы φ следует формула ψ, и они имеют хотя бы один общий символ атомной переменной, то существует формула ρ, называемая интерполянтом, такая, что каждый нелогический символ в ρ встречается как в φ, так и в ψ, φ влечет за собой ρ, а ρ влечет за собой ψ. Теорема была впервые доказана для логики первого порядка в Уильямом Крейгом 1957 году. Варианты теоремы справедливы и для других логик, таких как логика высказываний . Более сильная форма интерполяционной теоремы Крейга для логики первого порядка была доказана Роджером Линдоном в 1959 году; ^[1]^[2] общий результат иногда называют теоремой Крейга-Линдона .

Пример [ править ]

В логике высказываний пусть

\varphi =\lnot (P\land Q)\to (\lnot R\land Q)

\psi =(S\to P)\lor (S\to \lnot R)

.

Затем $\varphi$ тавтологически подразумевает $\psi$ . В этом можно убедиться, написав $\varphi$ в конъюнктивной нормальной форме :

\varphi \equiv (P\lor \lnot R)\land Q

.

Таким образом, если $\varphi$ держится, тогда $P\lor \lnot R$ держит. По очереди, $P\lor \lnot R$ тавтологически подразумевает $\psi$ . Поскольку две пропозициональные переменные, встречающиеся в $P\lor \lnot R$ происходят в обоих $\varphi$ и $\psi$ , это означает, что $P\lor \lnot R$ является интерполянтом для импликации $\varphi \to \psi$ .

Линдона Интерполяционная теорема

Предположим, что S и T — две теории первого порядка. В качестве обозначения пусть S ∪ T обозначает наименьшую теорию, включающую как S, так и T ; подпись содержащая S подписи ∪ T — наименьшая, S и T . Пусть также S ∩ T — пересечение языков двух теорий; сигнатура S ∩ T является пересечением сигнатур двух языков.

Теорема Линдона утверждает, что если S ∪ T невыполнимо, то существует интерполяционное предложение ρ в языке S ∩ T , которое истинно во всех моделях S и ложно во всех моделях T . Более того, ρ обладает более сильным свойством: каждый символ отношения, который имеет положительное вхождение в ρ, имеет положительное вхождение в некоторой формуле S и отрицательное вхождение в некоторой формуле T , а каждый символ отношения с отрицательным вхождением в ρ имеет отрицательное вхождение в ρ. вхождение в некоторую формулу S и положительное вхождение в некоторую формулу T .

Крейга интерполяционной Доказательство теоремы

Мы представляем здесь конструктивное доказательство интерполяционной теоремы Крейга для логики высказываний . ^[3] Формально теорема гласит:

Если ⊨φ → ψ, то существует ρ ( интерполянт ) такой, что ⊨φ → ρ и ⊨ρ → ψ , где атомы(ρ) ⊆ атомы(φ) ∩ атомы(ψ) . Здесь атомы(φ) — это набор пропозициональных переменных, встречающихся в φ , а ⊨ — это семантическое отношение следования для логики высказываний.

Доказательство. Предположим, ⊨φ → ψ. Доказательство проводится индукцией по числу пропозициональных переменных, входящих в φ, но не входящих в ψ, обозначаемых | атомы (φ) − атомы (ψ)|.

Базовый вариант | атомы (φ) − атомы (ψ)| = 0: Поскольку | атомы (φ) − атомы (ψ)| = 0, то атомы (φ) ⊆ атомы (φ) ∩ атомы (ψ). Более того, имеем ⊨φ → φ и ⊨φ → ψ. Этого достаточно, чтобы показать, что φ в данном случае является подходящим интерполянтом.

Предположим на шаге индукции, что результат получен для всех х, где | атомы (χ) − атомы (ψ)| = п . Теперь предположим, что | атомы (φ) − атомы (ψ)| = п +1. Выберите q ∈ атомы (φ), но q ∉ атомы (ψ). Теперь определите:

φ':= φ[⊤/ q ] ∨ φ[⊥/ q ]

Здесь φ[⊤/ q ] то же самое, что φ, с заменой каждого вхождения q на ⊤, а φ[⊥/ q ] аналогичным образом заменяет q на ⊥. Из этого определения мы можем отметить три вещи:

⊨φ' → ψ

( 1 )

| атомы (φ') − атомы (ψ) | = п

( 2 )

⊨φ → φ'

( 3 )

Из ( 1 ), ( 2 ) и индуктивного шага мы получаем, что существует интерполянт ρ такой, что:

⊨φ' → п

( 4 )

⊨ρ → ψ

( 5 )

Но из ( 3 ) и ( 4 ) мы знаем, что

⊨φ → п

( 6 )

Следовательно, ρ является подходящим интерполянтом для φ и ψ.

ЯВЛЯЕТСЯ

Поскольку приведенное выше доказательство конструктивно , можно извлечь алгоритм вычисления интерполянтов. Используя этот алгоритм, если n = | атомы (φ') − атомы (ψ)|, то интерполянт ρ имеет на O (exp( n )) больше логических связок , чем φ ( см. в обозначении Big O подробности относительно этого утверждения ). Аналогичные конструктивные доказательства могут быть предоставлены для базовой модальной логики K, интуиционистской логики и µ-исчисления с аналогичными мерами сложности.

Интерполяцию Крейга можно доказать и другими методами. Однако эти доказательства, как правило, неконструктивны :

с точки зрения теории моделей , через теорему совместной непротиворечивости Робинсона : при наличии компактности , отрицания и конъюнкции теорема совместной непротиворечивости Робинсона и интерполяция Крейга эквивалентны.
Теоретико-доказательное , посредством секвенциального исчисления . Если исключение разреза возможно и в результате сохраняется свойство подформулы , то интерполяция Крейга доказуема посредством индукции по выводам.
алгебраически , используя теоремы объединения для множества алгебр, представляющих логику.
посредством перевода в другую логику, использующую интерполяцию Крейга.

Приложения [ править ]

Интерполяция Крейга имеет множество применений, среди которых доказательство непротиворечивости , проверка моделей , ^[4] доказательства в модульных спецификациях , модульных онтологиях .

Ссылки [ править ]

^ Линдон, Роджер (1959), «Интерполяционная теорема в исчислении предикатов», Pacific Journal of Mathematics , 9 : 129–142, doi : 10.2140/pjm.1959.9.129 .
^ Троэльстра, Энн Шерп ; Швихтенберг, Хельмут (2000), Основная теория доказательств , Кембриджские трактаты по теоретической информатике, том. 43 (2-е изд.), Издательство Кембриджского университета, с. 141, ISBN 978-0-521-77911-1 .
^ Харрисон, стр. 426–427
^ Визель, Ю.; Вайсенбахер, Г.; Малик, С. (2015). «Решатели логической выполнимости и их применение при проверке моделей». Труды IEEE . 103 (11): 2021–2035. дои : 10.1109/JPROC.2015.2455034 . S2CID 10190144 .

Дальнейшее чтение [ править ]

Джон Харрисон (2009). Справочник по практической логике и автоматизированному рассуждению . Кембридж, Нью-Йорк: Издательство Кембриджского университета . ISBN 978-0-521-89957-4 .
Хинман, П. (2005). Основы математической логики . АК Петерс. ISBN 1-56881-262-0 .
Дов М. Габбай ; Лариса Максимова (2006). Интерполяция и определимость: модальная и интуиционистская логика (Оксфордские руководства по логике) . Оксфордские научные публикации, Clarendon Press . ISBN 978-0-19-851174-8 .
Ева Хугланд, Определимость и интерполяция. Теоретико-модельные исследования . Кандидатская диссертация, Амстердам, 2001 г.
У. Крейг, Три использования теоремы Эрбрана-Гентцена в связи теории моделей и теории доказательств , Журнал символической логики 22 (1957), вып. 3, 269–285.

[1] Линдон, Роджер (1959), «Интерполяционная теорема в исчислении предикатов», Pacific Journal of Mathematics , 9 : 129–142, doi : 10.2140/pjm.1959.9.129 .

[2] Троэльстра, Энн Шерп ; Швихтенберг, Хельмут (2000), Основная теория доказательств , Кембриджские трактаты по теоретической информатике, том. 43 (2-е изд.), Издательство Кембриджского университета, с. 141, ISBN 978-0-521-77911-1 .

[3] Харрисон, стр. 426–427

[4] Визель, Ю.; Вайсенбахер, Г.; Малик, С. (2015). «Решатели логической выполнимости и их применение при проверке моделей». Труды IEEE . 103 (11): 2021–2035. дои : 10.1109/JPROC.2015.2455034 . S2CID 10190144 .

[1]

[2]

[3]

[4]