Непротиворечивость УИП

Узкое исчисление предикатов непротиворечиво, если ни для ка­кой его формулы недоказуемы одновременно ни она сама, ни ее отри­цание.

Построим соответствие h, согласно которому каждой формуле УИП сопоставим некоторую формулу исчисления высказываний следующим образом.

1. Если А - элементарная формула Р(х₁,...,х_n), то h(А) = Р.

2. Если формулам А и В из УИП сопоставлены формулы h(А) и h(В) в ИВ, то h(ù А) = ù h(А), h(А * В) = h(А) * h(В), где * есть один из знаков: &, V, ®.

3. Если формуле А(х) сопоставлена формула h(А), то h(($х)А(х)) = h(А); h(("х)А(х)) = h(А), т.е. кванторы вместе с их переменными стираются.

Если А - формула в УИП, то h(А) получается из А стиранием в А всех кванторов и всех предметных переменных.

Лемма. Если формула А доказуема в УИП, то формула h(А) дока­зуема в ИВ.

Доказательство. Индукция по длине k доказательства.

БАЗИС. k = 1. Возможны следующие случаи.

1. ├ С в УИП, причем формула С - аксиома, полученная по одной из схем аксиом А1-А11. Тогда h(С) есть формула в ИВ, построенная по той же схеме аксиом.

2. ├ С, причем С есть ("x)A(x) ® А(у) - аксиома Бернайса. Тогда h(С) = h(("х)А(х) ® А(y)) = h(А) ® h(А). Поэтому h(С) дока­зуема в ИВ. Если С есть А(у) ® ($х)А(х) - вторая аксиома Бернай­са, то доказуемость А(С) в ИВ следует из тех же соображений.

ПРЕДПОЛОЖЕНИЕ ИНДУКЦИИ. Допустим, что лемма справедлива для всех доказуемых в УИП формул с длиной доказательства меньше k.

ШАГ ИНДУКЦИИ. Покажем, что лемма справедлива для всех дока­зуемых в УИП формул с длиной доказательства k. Пусть ├ А в УИП и A₁,A₂,…,A_k (=А) есть доказательство формулы А в УИП длины k. Возможны следующие случаи.

1. А - аксиома. Тогда это рассмотренный выше случай базиса.

2. ├ А в УИП и А₁,А₂,…,А_i,...,А_i ® A_k,...,A_k(=A) есть доказательство форму-лы А в УИП длины k, причем А_k получено из А_i и А_i ® А_k по правилу заключения. Так как длины доказательств A₁,A₂,...,А_i и A₁,A₂,…,A_i,…,A_i ®A_k формул А_i и А_i ® А_k меньше k, то по предположению индукции

(1) ├ h(А_i) в ИВ; (2) ├ h(А_i ® А_k) в ИВ.

Так как h(А_i ® А_k) = h(А_i) ® h(А_k), то

(3) ├ h(А_i) ® h(A_k)в ИВ; (4) h(А_k), П3(1,3).

3. ├ А в УИП и А₁,А₂,...,А_i,...,А_k (=А) есть доказательство формулы А в УИП длины k, причем формула А_k, равная С ® ("x)B(x) получена из формулы
А_i = С ® В(х) с помощью "-правила. Так как длина доказательства A₁,A₂,…,A_i формулы А_i меньше k, то по предположению индукции ├ h(А_i). Так как h(А_i) = h(С ® В(х)) = h(С ® ("x)B(x)) = h(А_k), то ├ h(A_k) в ИВ.

4. ├ А в УИП и А₁,А₂,...,А_i,...,А_k (=А) есть доказательство формулы А в УИП длины k, причем формула А_k, равная ($х)В(х) ® С получена из формулы
А_i = В(х) ® С с помощью $-правила. Далее ана­логично предыдущему случаю.

Теорема. УИП непротиворечиво.

Доказательство. Если ├ А и ├ ù А в УИП, то ├ h(А) и ├ ù h(А) в ИВ. Проти-воречие с непротиворечивостью ИВ.