Искусственный интеллект - [152]

следующим образом:

Если А есть М-формула и г - индикатор, то конкатенация А^г называется М-формулой с индикатором г, иногда пишем ind (А) = г.

Наконец, М-формулы с индикаторами будем называть оснащенными М-формулами.

Далее большими греческими буквами будем обозначать конечные (возможно пустые) упорядоченные наборы (списки) оснащенных М-формул. Слово (Г => А) называем дедуктивной секвенцией (ср. [20]), в отличие от [20] в дедуктивных секвенциях наборы состоят из оснащенных М-формул, пустой набор иногда обозначается ®.

V. Построение теории Кантора - Чёрча - Генцена (КЧГ)

Как известно, в схеме аксиом - основной секвенции Генцена (А => А) - секвенциального формализма логики предикатов, не уменьшая общности, можно ограничиться только случаем атомарной формулы А.

Этот результат естественно распространить на построение исчисления КЧГ по исчислению М из [20] следующим образом.

Первый ярус исчисления М в КЧГ сохраняется без изменений; во 2-ом ярусе вместо правила подъема ¹¹⁵ из [20], не уменьшая общности, возьмем схему аксиом

(/'): (А⁰ => А⁰), где А - атомарная формула (но в М, с термами и М-термами), имеющая по определению индикатор 0, то есть А является оснащенной атомарной М-формулой с индикатором 0;

правила К¹¹⁵ - ¹¹⁵А из [20] сохраняются, только в них все дедуктивные секвенции состоят из оснащенных М-формул; при этом правила П¹¹⁵ - ¹¹⁵А определяют индуктивно по построению выводов соответствующие индикаторы главных членов (что отражает в КЧГ известное определение рангов (по Генцену 1934 г.) формул логики предикатов), правила П¹¹⁵ - ¹¹⁵А имеют следующий вид.

П¹¹⁵: Г=>0. (avf-; ¹¹⁵П: (acf. Г=>0 ;

Г=>0, (Пд)^г~ (Ш)^Г|,Г^0

Р¹¹⁵: d. Г=>0.d ; Г=>0, (Рае)"

1¹¹⁵: d. Г=>0 Г=>0,(Ь)^г|

*Р: (А=>А d) (d Г^01 ; (Pae)^rs',A, Г=>А, 0

А,¹¹⁵: (А=>А. d) (а—н:)

А^А,е^г

(в—>а) (d.Г=>©1 в\Г=>0

(в правилах г и s - произвольные индуктивно определенные (по гипотезе индукции) индикаторы, вводимые по посылкам правил; ограничения на у и с, указанные в [20], естественно сохраняются). Построение теории КЧГ закончено.

Исчисление, в котором все М-формулы дедуктивной части являются оснащенными, будем называть оснащенным исчислением.Аналогично КЧГ можно строить после известных результатов Г. Генцена 1934 г. оснащенные секвенциальные исчислениялогики предикатов 1-го порядка.

VI. Теорема Cut и непротиворечивость теории Кантора -Чёрча - Генцена

Формулировка Теоремы Cut

Если в КЧГ выводимы секвенции (А => Л, А^г ) и (А^г, Г=> 0), то в КЧГ существует вывод секвенции (А, Г=>Л, 0), где А есть М-формула с индикатором г; А, Г, Л. ©суть наборы оснащенных М-формул.

Доказательство Теоремы непосредственно следует из следующей леммы о смешении в КЧГ, по формулировке и доказательству являющейся обобщением генценовской леммы о смешении в логике предикатов.

Лемма о смешении в теории КЧГ

Если X и 91 - выводы секвенций Е = (А => Л) и G = (Г => 0) в исчислении КЧГ, А¹ - оснащенная М-формула, г - индикатор, то в КЧГ можно построить вывод 3 секвенции Н = (А, Г_А => Л_А, 0), где выражение вида Ф_А обозначает результат вычеркивания из набора Ф всех оснащенных М-формул В^г таких, что В есть М-формула и В^А(В конвертируется в А, то есть в исчислении ^-конверсии [20, IV, п. 6] выводимы А-ссквснции 4->5иб-> А), здесь = выступает как символ равенства по определению, А, А, Г и 0 - наборы оснащенных М-формул.

Доказательство леммы о смешении в КЧГ

Доказательство Леммы проводим индукцией по кортежу (г, Д а), где Д = <р[91] и а = (р[К] (выражение вида (р \ у; | (длина вывода р) означает число вхождений в вывод р дедуктивных секвенций). Разбор случаев (включая базис и шаг индукции) осуществляем обычным образом по Г. Генцену 1934 г., например, аналогично тому, как это делается в статье «Теорема о сечении для 93-теорий в комбинаторно полных системах» [24] и других публикациях (список некоторых работ автора см., например, в [16] на с. 414-416).

Доказательство (с точностью до языка) отличается от известного логико-предикатного генценовского тем, что из наборов вычеркиваются не только все вхождения оснащенной М-формулы А' (как по Генцену в случае формул логики предикатов), но и все конвертирующиеся в А¹ оснащенные М-формулы В^г[5о А, в частности, А <-» А].

Кроме того, новые (по отношению к генценовским) правила *Х*. связывающие между собой два яруса КЧГ, не нарушают индикаторов вводимых М-формул (см. эти правила *\*) и относятся к структурным генценовским правилам.

Кортеж, сопоставленный выводам К, 91 и индикатору г, будем иногда обозначать через р [ К, 91, г |, где г = ind(H).

В доказательстве используем (в случае последних правил П* в К и *П в 91) лемму о подстановке М-термов вместо переменных в выводы исчисления КЧГ, сохраняющую все рассматриваемые параметры, формулируемую и доказываемую индукцией по длине данного вывода аналогично тому, как это делается в [16] и др. публикациях с 1970 г.

Кортежи (e,f у), где e,f у- индикаторы, считаем упорядоченными лексикографически, то есть {e\,f, у\) < (e₂,f₂, у2) тогда и только тогда, когда выполняется одно из условий: (1) e_t < е₂; (2) e_t = е₂ и /j < /i;

(3) e_l = e₂,f_l=f₂ny_l>2.

Используя структурные правила *К*, *W*, *С*,