Доказательство. Пусть

(1) ├ _L (" x)A(x). Далее

(2) ├ _L (" x)A(x) ® A(0), АБ1;

(3) ├ _L A(0), П3(1,2);

(4) ├ _L (" x)A(x) ® A(l), АБ1;

(5) ├ _L A(l), П3(1,4);

и так далее. Получили ├ _L A(0), ├ _L A(l),..., ├ _L A(k),....

Пусть теперь ├ _L A(k), k = 0,1,2,.... Допустим, что в L формула (" x)A(x) не доказуема. Так как формализм L полон, то

(1) ├ _L ù (" x)A(x). Далее

(2) ├ _L ù (" x)A(x) ® ($ х) ù А(х), Т12;

(3) ├ _L ($х) ù А(х), П3(1,2).

Последняя формула есть некоторая формула ($х_k)В_k(х). Тогда

(4) ├ _L ($х_k)B_k(x) Далее имеем

(5) ├ _L ($x_k)B_k(x) ® B_k (p_k), аксиома E_k;

(6) ├ _L B_k(p_k),П3(4,5);

(7) ├ _L ù А(р_k).

Получили, что в формализме L доказуема формула А(р_k) и ее отрицание. Противоречие с непротиворечивостью L.

Лемма. Если А(х) есть формула с единственной свободной пере­менной х, то

├ _L ($х)А(х) «(├ _L А(0) V ├ _L А(1) V...V ├ _L A(k) V...).

Доказательство. Пусть ├ _L ($х)А(х), Допустим противное: формулы A(k) не доказуемы в L ни при каком k. Так как формализм L полон, то ├ _L ù А(0),
├ _L ù А(1),..., ├ _L ù A(k),...). Тогда

(1) ├ ("x) ù A(x). Далее

(2) ├ ("x) ù A(x) ® ù ($х)А(х), Т14;

(3) ├ ù ($х)А(х), П3(1,2).

Получили, что в исчислении L доказуема формула ù ($х)А(х) и ее отрицание одновременно. Противоречие с непротиворечивостью L. Следовательно, справедливо ├ _L А(0) V ├ _L A(l) V....

Пусть теперь существует такое натуральное число р, для которого

(1) ├ _L A(p). Далее

(2) ├ _L А(р) ® ($х)А(х), АБ2;

(3) ├ _L ($х)А(х), П3(1,2). Лемма доказана.

Лемма. Всякий непротиворечивый класс К замкнутых формул УИП выполним на множестве натуральных чисел.

Доказательство. Пусть N = {0,1,2,...} есть множество натураль­ных чисел. Индукцией по построению формул из класса К зададим на N предикаты так, чтобы доказуемые в L формулы стали истинными вы­сказываниями, т.е. покажем, что формулы класса T _L, доказуемые в исчислении L, выполнимы на множестве натуральных чисел. Пусть Р(а₁,а₂,...,а_n) - элементарная формула в L, где Р - предикатная буква; а₁,а₂,...,а_n - символы натуральных чисел. В силу полноты L либо ├ _L Р(а₁,а₂,...,а_n), либо ├ _L ù Р(а₁,а₂,...,а_n). Пусть предикат

P (a₁,a₂,…,a₃) =

Индукцией по глубине k построения формулы покажем, что при так определенных предикатах замкнутые доказуемые в L формулы принимают истинные значения.

БАЗИС. k = 1. Пусть ├ _L А. Тогда А есть элементарная формула Р(а₁,а₂,...,а_n), причем ├ _L Р(а₁,а₂,...,а_n). Поэтому Р (а ₁, а ₂,..., а _n) = И.

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

ШАГ ИНДУКЦИИ. Покажем, что все доказуемые в L замкнутые формулы с глубиной построения k при выше определенных на N предикатах принимают значение И.

Пусть ├ _L А, причем формула А имеет глубину построения k. Возможны следующие случаи.

1. А есть ("x)B(x). Тогда

(1) ├ _L ("x)B(x). Далее имеем

(2) ├ _L ("x)B(x) «(├ _L B(0), ├ _L B(l),..., ├ _L B(p),...);

(3) ├ _L B(0), ├ _L B(l),..., ├ _L B(p),....

Так как глубины построения формул В(р), р = 0,1,2,..., меньше k, то по предположению индукции высказывания

B(0) = И, B(1) = И,..., B(p) = И,....

По смыслу квантора общности высказывание (" х)В(х) истинно.

2. ├ _L А и А есть ($х)В(х). Тогда

(1) ├ _L ($х)В(х). Далее имеем

(2) ├ _L ($х)В(х) «(├ _L B(0) V ├ _L B(1) V...V ├ _L B(p) V...);

(3) ├ _L B(0) V ├ _L B(l) V... V ├ _L B(p) V....

Пусть для определенности ├ _L В(р). Так как глубина построения формулы В(р) меньше k, то по предположению индукции высказывание В(р)истинно. По смыслу квантора общности высказывание (" х)В(х) истинно.

3. ├ _L А и А есть В & С. Тогда ├ _L В & С, откуда по ПВ2 полу­чаем ├ _L В и
├ _L С. Так как глубины построения формул В и С меньше k, то по предположе-нию индукции высказывания В и С истинны. Тогда В & С истинно, т.е. высказывание А истинно.

Случаи, когда А есть В V С, В ® С, ù В, рассматриваются анало­гично.

Итак, все доказуемые в L замкнутые формулы при выше опреде­ленных на N предикатах принимают истинные значения. Так как формулы класса К доказуемы в L как аксиомы, то класс К замкнутых формул выполним на множестве натуральных чисел. Иначе говоря, не­противоречивый класс замкнутых формул УИП имеет модель.

Теорема. Всякая замкнутая общезначимая в логике предикатов формула доказуема в УИП.

Доказательство. Пусть А - общезначимая формула логики преди­катов. Допустим противное: формула А в УИП не доказуема. Тогда класс формул К = { ù А} непротиворечив и по предыдущей лемме формула ù А выполнима на мно-жестве натуральных чисел. Противоречие с общезначимостью формулы А. Следовательно, общезначимая формула А доказуема в УИП.

Из двух выше доказанных теорем следует следующая теорема.

Теорема (Геделя о полноте). Замкнутая формула доказуема в УИП тогда и только тогда, когда она общезначима.

Замечание. К узкому исчислению предикатов можно добавить специальный предикат равенства х = у и две характеризующие его аксиомы равенства (АР):

AP1) х = х;

АР2) х = у ® (А(х) ® А(у)),

где А(х) - произвольная формула УИП, имеющая свободную переменную х (возможно и другие переменные).

В УИП с равенством справедлива теорема о совпадении класса общезначимых формул (с равенством) и класса формул, доказуемых в УИП (с равенством).

УИП с равенством можно расширить далее, допустив при построе­нии элементарных формул использование функциональных термов. И здесь справедлива выше приведенная теорема.

Заметим еще, что если формула А(Р₁,...,Р_n) с указанным множе­ством предикатных переменных доказуема в исчислении предикатов, то можно построить такое ее доказательство, в котором не встреча­ются предикатные переменные, отличные от Р₁,..., Р_n.