Определение 4: Всякий терм, не содержащий переменных, называется замкнутым термом

Счётная интерпретация теории будет иметь своей областью множество замкнутых термов теории . Согласно лемме 3, это множество является счётным. Если есть предметная константа в теории , то она сама и будет своей интерпретацией. Функциональная буква теории будет интерпретироваться операцией в , имеющей своими аргументами замкнутые термы теории , а значением – замкнутый терм той же теории. Отношение , интерпретирующее предикатную букву теории , будет считаться выполненным в для аргументов тогда и только тогда, когда ├ . Чтобы доказать, что является моделью достаточно показать, что произвольная замкнутая формула теории истинна в тогда и только тогда, когда ├ , так как все теоремы теории являются также теоремами и теории .

Мы докажем это индукцией по числу логических операций и кванторов в формуле . Пусть сначала - есть замкнутая элементарная формула. В этом случае, по определению, формула истинна в тогда и только тогда, когда ├ . Допустим теперь, что всяка замкнутая формула с числом операций и кванторов меньшим, чем в формуле , истинна в тогда и только тогда, когда ├ .

Случай 1: Формула имеет вид . Если формула истинна в , то формула ложна в и, следовательно, в силу индуктивного предположения, неверно, что ├ . Так как теория полна, а формула замкнута, то ├ , т. е. ├ . С другой стороны, если - ложна в , то формула истинна в , и тогда ├ . А так как непротиворечива, то неверно, что ├ , т. е. ├ .

Случай 2: Формула имеет вид импликации . Из замкнутости вытекает замкнутость и . Если формула ложна в , то и . А силу полноты имеем: ├ . Тогда из тавтологии имеем: ├ , т. е. ├ . В силу непротиворечивости : не ├ . С другой стороны, если неверно, что ├ , то, в силу полноты , получим: ├ . Принимая во внимание тавтологии и , получаем: ├ и ├ . Следовательно, формула истинна в . В силу непротиворечивости , имеем: не ├ . Значит, формула ложна в . Таким образом, ложна в .

Случай 3: Формула есть . Тогда при некотором значении формула есть , а - есть . Здесь есть ещё возможность того, что замкнута и не содержит свободно. Но в таком случае формула истинна тогда и только тогда, когда истинна. Формула будет истинной в данной интерпретации только в том случае, когда в этой интерпретации истинна формула . Поэтому ├ тогда и только тогда, когда ├ . Таким образом, интересующее нас утверждение для следует из соответствующего утверждения для .

Предположим, что формула истинна в , но не ├ . В силу полноты теории имеем: ├ , т. е. ├ . Однако, известно, что ├ . Следовательно, ├ . Так как формула истинна в , то истинной в будет также формула .По индуктивному допущению, получаем: ├ . Таким образом, получили противоречие с фактом непротиворечивости теории .

Допустим теперь, что - ложна в , но ├ . Из ложности формулы в и из определения , как множества всех замкнутых термов вытекает, что для некоторого замкнутого терма теории значение будет ложным. Однако, по предположению, имеем: ├ . Следовательно, по аксиоме 4: ├ . Далее по индуктивному допущению: формула истинна в . Снова пришли к противоречию.

Итак, является счётной моделью для теории , а, следовательно, и для теории . Так как всякая теорема теории является также теоремой теории , то множество служит моделью и для теории . Теорема доказана полностью.

Следствие 1: Всякая логически общезначимая формула теории первого порядка является теоремой теории .

Доказательство: Достаточно рассмотреть лишь замкнутые формулы , поскольку всякая формула логически общезначима тогда и только тогда, когда логически общезначимой будет её замыкание, и выводима в теории тогда и только тогда, когда в выводимо её замыкание.

Пусть - логически общезначимая замкнутая формула теории . допустим, что не является теоремой в . Тогда, если добавить к теории формулу в качестве новой аксиомы, то получим новую теорию , которая будет непротиворечивой (по лемме 2). Теория имеет (согласно теореме 2) модель . Так как формула является аксиомой в , то истинна в . А так как формула - логически общезначима, то она истинна в . Получили противоречие: формула одновременно истинна и ложна в , чего быть не может. Противоречие возникло из-за неверного допущения. Значит, формула должна быть теоремой теории . Что и требовалось доказать.

Следствие 2: (теорема Геделя (1930) о полноте).

Во всяком исчислении предикатов первого порядка теоремами являются все те, и только те формулы, которые логически общезначимы.

Доказательство: Доказательство этого утверждения следует из теоремы 1 и следствия 2 из теоремы 2, хотя первоначальное доказательство самого Геделя было получено другим путём.

Следствие 3: a) Формула истинна в каждой счётной модели теории тогда и только тогда, когда ├_К . Следовательно, истинна в каждой модели теории тогда и только тогда, когда ├_К .

b) Если во всякой модели теории формула выполнена при условии выполнения всех формул некоторого множества формул , тогда ├_К .

c) Если формула теории является логическим следствием данного множества формул теории , то ├_К .

d) Если формула теории является логическим следствием формулы из этой же теории, то ├_К .

Доказательство: a) Можно считать, что формула замкнута. Допустим, что формула истинна в любой счётной модели теории . Если не ├_К , то теория непротиворечива. Следовательно, теория имеет счётную модель . Формула , как аксиома теории , является истинной в . Но является также моделью и для теории , поэтому формула истинна в . Таким образом, формула одновременно истинна и ложна в . Получили противоречие, которое возникло из-за неверного допущения. Требуемое утверждение доказано.

b) Рассмотрим теорию .Формула истинна в каждой модели этой теории. Тогда из утверждения (а) имеем: ├_К+Г , следовательно, ├_К .

c) Данное утверждение следует из пункта (b).

d) Последнее утверждение является частным случаем пункта (c).

Раньше было доказано, что в формальном исчислении высказываний (теория ) произвольная формула является тавтологией тогда и только тогда, когда эта формула является теоремой теории . Следствия 1-3 показывают, что и для логики предикатов справедливы соответствующие утверждения.

Следствие 4: Если теория первого порядка имеет какую-нибудь модель, то она имеет и счётную модель.

Доказательство: Если имеет модель, то теория - непротиворечива. Следовательно, по теореме 2, имеет счётную модель. Что и требовалось доказать.

Замечание: Можно доказать, что для любого кардинального числа всякая непротиворечивая теория имеет модель мощности .

Правило индивидуализации: Если терм свободен для переменной в формуле , то ├ .

Доказательство: Из формулы и схемы аксиом (А4) имеем: , по правилу получаем . Верно и обратное. Не сложно доказать, что формула - общезначима, а значит является теоремой, т. е. .

Не сложно также доказать следующие формулы: , , .

В качестве примера приведём доказательство следующей формулы:

.

Доказательство:

1) - гипотеза;

2) - гипотеза;

3) - выводится из пункта 1 по правилу индивидуализации;

4) - выводится из пункта 2 по правилу индивидуализации;

5) - получается из пунктов 3 и 4 с помощью правила и тавтологии ;

6) - выводится из пункта 5 по правилу ;

7) ├ - получается из пунктов 1 – 6;

8) ├ - получается из пунктов 1 – 7;

9) ├ - аналогично пункту 8;

10) ├ - из пунктов 8 и 9;

11) ├ - из пунктов 1 – 10.