32. Полнота логики второго порядка с сечением

Мы будем теперь рассматривать логику второго порядка, получаемую из логики первого порядка (предыдущий раздел) добавлением замкнутых предикатных переменных к списку символов и разрешением применять в формулах кванторы по предикатам.

К аксиомам и правилам вывода для первого порядка мы добавляем кванторные правила второго порядйа и правило сечения

Здесь обозначает предикатный терм, А — свободную предикатную переменную, не входящую в

Зафиксируем взаимно однозначную рекурсивную нумерацию

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

Мы переходим к определению внутреннего предельного множества V в канторовом пространстве, которое образует множество всех полных оценок. V — это пересечение следующих открытых множеств:

1 Для любой формулы открытые множества

2 Для любой формулы открытые множества

3 Для любой формулы открытые множества

4 Для любой формулы открытые множества где объединение берется по всем предметным термам и открытое множество Для любого предметного терма

5 Для любой формулы открытое множество и открытое множество для любого предметного терма

6 Для любой формулы открытое множество где объединение берется по всем предикатным термам от подходящего числа переменных, и открытое множество для каждого предикатного терма

7 Для любой формулы открытое множество и открытое множество для любого предикатного терма

Формула истинна для всех полных оценок, если если выводима в исчислении борелевских множеств. Мы докажем следующий конструктивный вариант теоремы Генкина [1] о полноте для логики второго порядка с сечением.

Формула истинна для всех полных оценок тогда и только тогда, когда она доказуема в логике второго порядка с сечением.

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

Как и в случае логики первого порядка, секвенция выводима посредством этих бесконечных правил тогда и только тогда, когда она выводима в обычной логике второго порядка.

Непосредственным следствием построения У является доказуемость следующих семи типов борелевских секвенций:

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

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

утончением. Шаг индукции. Допустим, например, что и что последнее применение правила в доказательстве есть

По индукционному предположению имем для всех Поведение дает Далее, мы знаем, что выводима в исчислении борелевских множеств. Сечение, примененное двум посылкам, дает что и требовалось. Остальные правила вывода рассматриваются аналогично.

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

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

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

Множество имеет вид или где некоторая формула. В первом случае заменим на во втором — на Сделаем это для всех Далее мы просто вычеркнем множества наконец, заменим на Таким образом мы преобразуем каждую секвенцию из данного вывода в секвенцию, состоящую из формул второго порядка. Конечная секвенция

реходит в Мы получили вывод в котором каждая аксиома и применение правила является частным случаем следующих аксиом и правил вывода.

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

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

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