2. Секвенциальное исчисление предикатов

Зафиксируем некоторую произвольную сигнатуру Σ и определим секвенциальное исчисление предикатов сигнатуры Σ (ИПС^).

Алфавит ИПС^ получается из алфавита ИΠ^Σ добавлением символа следования ├, т.е. Α(ИΠС^Σ) = Σ  V  {,¬,,, , , , (,),,, ├}. Формулами ИПС^ будут формулы сигнатуры Σ.

Секвенциями ИПС^ называются конечные последовательности следующих двух видов, где φ₁,...,φ_n,φ — формулы ИПС^:

φ₁,…,φ_n ├φ

φ₁,…,φ_n├ .

Примем следующие соглашения. Пусть x₁,... ,х_n — переменные, t₁,...,t_n — термы сигнатуры Σ и φ — формула сигнатуры Σ. Запись будет обозначать результат одновременной подстановки термов t₁,...,t_n вместо всех свободных вхождений в φ переменных x₁,... ,х_n соответственно, причем, если в тексте встречается запись , то предполагается, что для всех i = 1,..,n ни одно свободное вхождение в φ переменной x_i не входит в подформулу φ вида yφ₁ или yφ₁, где у — переменная, входящая в t_i. Вместо записи будем иногда писать φ( t₁,...,t_n). При этом, наряду с тем, что переменные x₁,... ,х_n в записи φ(x₁,... ,х_n) будут всегда предполагаться попарно различными, среди t₁,...,t_n могут быть равные термы.

Пример . 1. Обозначим через φ формулу х R(x, у, z), через t₁ — терм F₁(y,z,u), через t₂ — терм F₂(F₃(z), w). Результат подстановки равен xR(x, F₁ (y,z,u),F₂(F₃(z),w)), a результат подстановки равен х R(x, F₁(y,z,u), F₁(y,z,u)). Заметим, что результат последовательной подстановки может не совпадать с результатом одновременной подстановки.

2. Для формулы φ = х R(x, у, z) и терма t = F(y, x, и) запись (φ)_t^y недопустима, поскольку после подстановки терма t вместо свободной переменной у в формуле хR(x,F(y,x,u),z) вхождение переменной x в терм t становится связанным.

Аксиомами ИПС^ являются следующие секвенции:

1. φ├φ, где φ — формула сигнатуры Σ;

2. ├(xx), где x— переменная;

3. (t₁q₁),...,( t_nq_n), ├

где t₁,...,t_n , q₁,...,q_n — термы сигнатуры Σ, φ — формула, удовлетворяющая условиям на записи и

Правила вывода ИПС^ задаются следующими записями, где Г — произвольные (возможно пустые) конечные последовательности формул ИΠС^Σ, φ, ψ, χ — произвольные формулы ИПС^:

1. (введение Λ).

2. (удаление ).

3. (удаление ).

4. (введение ).

5. (введение ).

6. (удаление , или правило разбора двух случаев).

7. (введение →).

8. (удаление →).

9. (удаление , или доказательство от противного).

10. (выведение противоречия)

11. (перестановка посылок).

12. (утончение, или правило лишней посылки).

13. где переменная х не входит свободно в формулы из Г (введение  справа)

14. (введение  слева)

15. (введение  справа)

16. где переменная х не входит свободно в ψ и в формулы из Г (введение  слева)

Понятия линейного доказательства в ИПС^, доказательства в виде дерева в ИПС, доказуемой в ИПС секвенции (теоремы ИПС^) и доказуемой в ИПС^ формулы определяются аналогично соответствующим понятиям ИС на основе аксиом 1-3 и правил вывода 1-16. Также аналогично предложению 1.2.1 устанавливается

Предложение 1. Секвенция S имеет доказательство в ИПС^ в виде дерева тогда и только тогда, когда S — теорема ИПС^.

Пример. Приведем доказательство секвенции хyφ(x,y)├yхφ(х,у) в виде дерева для любой формулы φ(х,у):

Следующая теорема является синтаксическим аналогом теоремы 2.1.2 и позволяет преобразовывать доказуемые формулы ИС в доказуемые формулы ИПС^.

Теорема 2. Пусть φ(Α_ι,..., Α_n) — доказуемая формула ИС, φ₁,...,φ_n — формулы сигнатуры Σ. Тогда в результате подстановки формул φ₁,...,φ_n вместо всех соответствующих вхождений пропозициональных переменных Α_ι,..., Α_n образуется доказуемая в ИПС^ формула φ(φ₁,...,φ_n).

Доказательство. Пусть D — дерево доказательства секвенции ├ φ (Α_ι,..., Α_n) в ИС. Тогда, заменяя в дереве D переменные Α_ι,..., Α_n соответственно на φ₁,...,φ_n, а остальные пропозициональные переменные — на формулу (x х), получаем дерево D₁, являющееся деревом доказательства секвенции ├ φ(φ₁,...,φ_n).

Предложение 3. Для любой формулы φ, удовлетворяющей условиям на запись , в ИПС^ доказуемы следующие секвенции:

1. x₁,…,x_n├

2. ├ x₁,…,x_n

Доказательство. а) Пусть y₁,…,y_n – попарно различные переменные, не входящие в , в t₁,…,t_n и отличных от x₁,…,x_n. Для k=1..n имеет место равенство: т.е. одновременная подстановка совпадает с последовательной, (т.к. y_i так выбраны) и выполнены все условия на запись формулы. Тогда следующее дерево будет доказательством в ИПС^:

обозначим =. Для  выполнено условие на запись и для всех k=1..n , тогда т.е. секвенция доказуема. Т.к. , то доказана секвенция . Осталось применить правило сечения к данным секвенция:

пункт b) доказать аналогично с помощью правил 15 и 16.

Предложение 4. В ИПС^ допустимы правила а) …о) и

п) (подстановка термов)

р) (удаление )

Доказательство. Первые 14 правил доказываются как и в ИС. Докажем правило п). Будем использовать Предложение 3.

докажем р):

.

Покажем, что для отношения  на множестве термов доказуемы обычные свойства равенства (рефлексивности, симметричности и транзитивности), т.е. доказуемо в ИПС^ , что  — отношение эквивалентности.

Предложение 5. Для любых термов t,q,r  Τ(Σ) следующие секвенции доказуемы в ИПС^:

1. ├(tt);

2. (tq)├(qt);

3. (tq),(qr)├(tr).

Доказательство. Доказуемость секвенции ├ (tt) устанавливается применением допустимого правила (п) из предложения.4:

Для доказательства секвенции (б) рассмотрим аксиому которая равна секвенции (tq),( tt)├ (qt). Выпишем дерево, которое с участием этой аксиомы представляет доказательство свойства симметричности:

Доказуемость секвенции (в) устанавливает следующее дерево:

.

Пусть A = <Α;Σ> — алгебраическая система, S = S(x₁,..., x_n) — секвенция ИПС^, все свободные переменные формул которой содержатся среди x₁,..., x_n. Будем говорить, что секвенция S истинна на элементах a₁,...,a_n А в алгебраической системе A и писать A ╞ S(a₁,...,a_n), если выполняется одно из следующих условий:

1. S равна φ₁,..., φ_n ├ψ и из A |= φ_i(a₁,...,a_n) для всех i = 1,... n следует A ╞ ψ(a₁,...,a_n);

2. S равна φ₁,..., φ_n ├ и хотя бы одна из формул φ₁,..., φ_n ложна на элементах a₁,...,a_n  А в алгебраической системе A.

Если секвенция S не истинна на элементах a₁,...,a_n  А в алгебраической системе A, то будем говорить, что S ложна на элементах a₁,...,a_n  А в A. В частности, секвенция ├ ложна на любой алгебраической системе.

Секвенция S = S(x₁,..., x_n) в ИПС^ называется тождественно истинной, если S истинна на любых элементах a₁,...,a_n  А в любой алгебраической системе A = <Α; Σ>.

В дальнейшем нам предстоит доказать теорему о полноте для исчисления предикатов, установленную К. Гёделем и утверждающую, что класс доказуемых в ИПС^ секвенций совпадает с классом тождественно истинных секвенций ИПС^. Одна часть этого утверждения — это

Теорема 6. (теорема о непротиворечивости ИПС^). Если секвенция S доказуема в ИПС^, то S тождественно истинна. В частности, не все формулы ИПС^ доказуемы в ИПС^.

Доказательство проводится индукцией по высоте дерева доказательства секвенции S. Тождественная истинность аксиом ИПС^ очевидна. Проверку сохранения тождественной истинности при переходе по правилам 1-16 мы проведем на примере правила 14

оставив рассмотрения остальных правил в качестве упражнения. Итак, пусть секвенция Г, (φ)_t^x├ψ тождественно истинна, т.е. в предположении истинности в системе A = <Α; Σ> на каких-то элементах a₁,...,a_n  А всех формул из Г и формулы (φ)_t^x мы имеем A |= ψ(a₁,...,a_n). Если в системе A на каких-то элементах a₁,...,a_n  А истинны все формулы из Г и формула х φ, то, в частности, будет справедливо A ╞ ψ(a₁,...,a_n). Значит, по условию будет верно A╞ ψ(аι,..., α_η). Следовательно, секвенция Г, x φ├ψ тождественно истинна. 