31. Конструктивный вариант теоремы Гёделя о полноте

Множество всех оценок (т. е. распределений истинностных значений) атомарных формул, выполняющих данную формулу классического исчисления предикатов первого порядка, — это борелевское множество конечного бэровского класса в канторовом пространстве. Конструктивизация теории борелевских множеств, предпринятая в предыдущем пункте, позволяет нам дать конструктивный вариант теоремы Гёделя [1] о полноте.

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

Конечная последовательность формул

будет называться секвенцией. Мы отождествляем секвенции, если они равны как конечные множества.

Аксиома — это секвенция, построенная из атомарных формул и их отрицаний и содержащая как так и для некоторой атомарной формулы Правила вывода следующие:

Для правила Д-введения имеется обычное условие: свободная переменная а не должна входить в заключение.

Зафиксируем теперь взаимно однозначную рекурсивную нумерацию атомарных формул

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

формул мы определяем индукцией по числу логических знаков в

Здесь мы предположили, что

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

Так как в формуле есть лишь конечное число логических знаков, то бэровский класс конечен,

Формула называется логически истинной, если она истинна для всех оценок атомарных формул, т. е. если где X обозначает все канторовское пространство. Мы готовы теперь сформулировать наш вариант теоремы Гёделя о полноте.

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

Заменим временно правило Д-введения, сформулированное выше, на бесконечное правило

Выводы в модифицированном таким образом исчислении предикатов изоморфны выводам в формальной системе для борелевских множеств, построенной в предыдущем пункте, если мы сопоставим каждой формуле борелевское множество . С другой стороны, приведенное выше бесконечное правило, эквивалентно обычному правилу Д-введения. Действительно, если доказуемо для всех термов то, в частности, доказуемо где а — свободная переменная, не входящая в так как свободная переменная является термом. Обратно, если даны произвольный терм и вывод секвенции где а — свободная переменная, не входящая в

то позаботимся сначала о том, чтобы переменные, связываемые при -введениях в доказательстве не входили бы в Затем мы можем заменить а на во всем доказательстве, получая тем самым вывод Доказательство закончено.

Основная теорема Генцена утверждает, что правило сечения имеет место для исчисления предикатов как производное правило вывода:

Это утверждение оказывается непосредственным следствием справедливости правила сечения для исчисления борелевских множеств (через теорему о полноте). Действительно, если то по одной половине теоремы о полноте мы получаем и Отсюда правило сечения для борелевских множеств позволяет нам заключить , а другая половина теоремы о полноте дает , что и требовалось. Хотя это доказательство основной теоремы и конструктивно, оно, в отличие от доказательства Генцена [1], не финитно в строгом гильбертовском смысле.