Полнота исчисления предикатов 1-го порядка

Теорема. Формула логически общезначима тогда и только тогда, когда логически общезначимо ее замыкание.

Формула выводима (доказуема) в ИП1 тогда и только тогда, когда выводимо ее замыкание.

Это относится и к истинности формулы в любой интепретации.

Теорема (Лемма 2.9, [М].) Если замкнутая формула A теории K не доказуема в K, то теория K’, полученная добавлением формулы A в качестве аксиомы, непротиворечива.

Доказательство. Допустим, что теория K’ противоречива. Тогда найдется формула B этой теории, для которой + K’  B и + K’ B. Тогда, в силу известной тавтологии (секвенция 5) имеем: + K’ (B >(B > A). Дважды применяя MP, получим + K’ A.  Следовательно,

A+ K’ A, тем самым (если считать A только гипотезой) такая же секвенция доказуема и в исходной теории K: A + K A. Но  так как A замкнута, то можно применить теорему дедукции и получить + K (A > A) = ( A ? A). Тогда, в силу эквивалентности (для любой формулы B) B ?  B ? B, получим + K A, что противоречит условию.

Теорема (лемма 2.10). Множество всех выражений всякой теории первого порядка счетно. Определение. Теория K первого порядка называется полной, если в ней доказуема любая ее формула, либо отрицание этой формулы. Определение. Теория K’ называется расширением теории K, если ее алфавит совпадает с алфавитом теории K и всякая теорема теории K является также и теоремой теории K’. Теорема (лемма 2.11[ Линдебаум]). Если теория K первого порядка непротиворечива, то существует ее непротиворечивое полное расширение.

Доказательство. Пусть B1, B2, …, Bn, … - какая-нибудь нумерация всех замкнутых формул теории K. Определим последовательность теорий T0, T1,…, Tn,…, положив T0 = K, а при условии, что теория Tn (n ? 0) уже определена, теория Tn+1 строится следующим образом: если формула Bn+1 не доказуема в Tn, то формулу Bn+1 вводим в теорию Tn+1 в качестве аксиомы; если же Bn+1 доказуема в Tn, то полагаем Tn = Tn+1. Заметим сразу, что в силу теоремы п. 2 (лемма 2.9) теория Tn+1 непротиворечива при условии непротиворечивости теории Tn (и является расширением последней или совпадает с ней).

НЕ нашли? Не то? Что вы ищете?

Определим теперь «предельную» теорию T, множество аксиом которой есть объединение множеств аксиом всех теорий Ti.  Поскольку каждый вывод в теории T конечен и использует конечное множество аксиом, то в предположении непротиворечивости каждой теории Ti теория T также непротиворечива. Но непротиворечивость всех теорий Ti следует из непротиворечивости исходной теории K и сделанного выше замечания о непротиворечивости Tn+1 при условии непротиворечивости Tn.

Остается доказать полноту теории T (которая, очевидно, является расширением всех теорий Ti и, в частности, исходной теории K).

Для произвольной формулы A теории K  имеет местно A = Bn+1 для некоторого неотрицательного n. Но тогда либо отрицание Bn+1 не доказуемо в  Tn, и при этом Bn+1 доказуемо в  Tn+1 (и тем самым в T), либо отрицание Bn+1 доказуемо в  Tn (и тем самым в T).

Итак, любая формула A теории K (а, стало быть, и теории T) либо доказуема в T, либо в T доказуемо ее отрицание, т. е. теория T полна.


Теорема (предложение 2.12). Всякая непротиворечивая теория 1-го порядка имеет счетную модель.

Доказательство. Пусть K – непротиворечивая теория 1-го порядка. Добавим в ее алфавит счетное множество новых предметных констант: b1, b2, …, bn,… Построенную таким образом теорию назовем K0. Множество аксиом теории  K0 включает в себя все аксиомы теории K, а также все аксиомы, полученные подстановкой новых констант из схем (1) – (5) аксиом ИП1.

Утверждение 1. Теория K0 непротиворечива.

Доказательство. Допустим противное, т. е. пусть для некоторой формулы A + K0  A&A. Тогда в доказательстве конъюнкции A&A в теории K0 каждую константу bi заменим переменной yi, которой нет в этом доказательстве. Получим тогда вывод (доказательство) уже в теории K формулы A(yi|bi)& A(yi|bi), т. е. теория K оказывается противоречивой вопреки условию. #

Построим теперь теории Kn (n – положительное натуральное число) и K?.

Пусть - какая-нибудь нумерация формул теории K0, содержащих не более одной свободной переменной. Если , то полагаем .

Строим последовательность констант из ранее введенного множества новых констант так, чтобы константа не содержалась ни в одной из формул и была отлична от .

Введем формулу

.

  Теория Kn определяется как теория, полученная из K0 добавлением к множеству аксиом формул S1,…, Sn, а теория K? - как теория, содержащая в качестве аксиом все формулы Sn (при n > 0).

       Утверждение 2. Теория K? непротиворечива.

       Доказательство. Достаточно доказать непротиворечивость всех теорий Ki (i = 0,1,…), так как любой вывод в теории K? содержит лишь конечное множество аксиом и является выводом в некоторой теории Kn.

       Индукция по i. Непротиворечивость теории K0 уже доказана.

       Пусть теория Kn-1 непротиворечива, а теория Kn противоречива. Тогда в ней доказуема любая формула, в частности Sn. Значит, в Kn доказуема формула (Sn > Sn),  в теории Kn-1 доказуема секвенция Sn + Sn, но поскольку формула Sn замкнута, то, применяя теорему дедукции, получим +Kn-1 (Sn > Sn).

       Далее используем тавтологию (A > A) > A (скобка – отрицание конъюнкции), получая

+Kn-1  Sn. Но

       .

Следовательно, +Kn-1  и +Kn-1  .

В доказательстве формулы в теории Kn-1  заменим всюду константу переменной xp, которая в этом выводе не встречается (точнее, она вообще «новая» переменная). Тогда в этой теории доказана формула и, применяя правило обобщения, получим

+Kn-1  . Так как последняя формула подобна формуле , то доказуема и она, причем, вместе со своим отрицанием (см. выше). То есть, теория Kn-1 противоречива вопреки индукционному предположению.

       Итак, каждая теория Kn непротиворечива, откуда следует непротиворечивость теории K?. #

       На следующем шаге доказательства определяется теория T как полное непротиворечивое расширение теории K? (существующее согласно доказанному выше) и строится модель M теории K (исходной) следующим образом.

       Область интерпретации A определяется как множество всех замкнутых (т. е., не содержащих переменных) термов теории K0. Каждой константе соответствует она сама, каждому функциональному символу сопоставляется n-арная операция , аргументами которой являются замкнутые термы , а результатом терм ; каждому предикатному символу сопоставляется n-арный предикат , истинный в M (по определению) тогда и только тогда, когда + T . Очевидно, что множество A счетно.

       Утверждение 3. Замкнутая формула теории K истинна в M тогда и только тогда, когда она доказуема в теории T.

       Доказательство. Индукция по числу связок и кванторов в формуле A. Базис (атомарная формула) следует сразу из определения.

Пусть A =  B. Тогда, если + M A, то неверно, что + M B, и, по предположению индукции, неверно, что + T B. Отсюда, в силу полноты теории T, + T B=A (формула B, очевидно, тоже замкнута). Если же + M A, то + M B и (опять по предположению)

+ T B, а так как теория T непротиворечива, то + T B=A. Итак, + M A ? + T A.


A = B >C. Из замкнутости формулы A следует замкнутость формул B и C. Если + M A (A ложна в M), то + M B и + M C. Тогда, в силу полноты теории T, + M C, и по предположению индукции + T C. Таким образом, в T доказуемы B и C, откуда по секвенции (8) получаем, что в T доказуемо отрицание импликации: ( B >C), т. е. A, и, поскольку теория T непротиворечива, неверно, что + T A.

Обратно, если неверно, что + T A, то + T A=( B >C)=B&C. Следовательно, в теории T доказуема формула B и не доказуема формула C. Значит, по предположению индукции C ложна в M, а B истинна M, т. е. импликация B >C=A ложна в M, что и требовалось.


Пусть, наконец, . Так как формула A замкнута, то формула B содержит не более одной свободной переменной. Если и формула B замкнута, то + M A ? + M B, и остается применить предположение индукции. Иначе, ввиду нумерации всех формул теории K0 (а, стало быть, и теории T) не более, чем с одной свободной переменной, для некоторого k , а .

Пусть + M A, но + T A. Тогда (в силу полноты теории T) + T A = .

Но формула является аксиомой теории T. Тогда формула доказуема в T, но, так как, формула A истинна в M, то, согласно правилу (А4), истинной в M будет  и формула , а по предположению индукции она доказуема в T. Получается, что теория T противоречива вопреки условию. Итак, если + M A, то + T A.

Если же формула A ложна в M, то, предполагая доказуемость A в T, будем иметь следующее. Ложность формулы означает, что существует замкнутый терм t такой, что формула ложна. Но A доказуема в T, и, по правилу (А4), для любого замкнутого терма t + T , и, по предположению индукции, +  M . Противоречие.

Итак, окончательно + M A ? + T A, и счетная модель для теории K ( и вместе с ней для теорий K0 и T) построена.


Теорема (Гёделя о полноте, следствия 2.13 и 2.14). Формула логически общезначима тогда и только тогда, когда она доказуема в теории ИП1.

Доказательство. Утверждение теоремы достаточно доказать для любой замкнутой формулы A.

Пусть формула A логически общезначима, но не доказуема в теории K. Тогда, добавив отрицание A как аксиому, получим непротиворечивое расширение K’ теории K. Теория K’ имеет счетную модель M, и + M A. Но как логически общезначимая формула A также истинна в M. То есть, формула A истинна в модели M вместе со своим отрицанием, что невозможно.

То, что любая теорема ИП1  является логически общезначимой, было доказано ранее.