Искусственный интеллект

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

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

Если 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_l2.

Используя структурные правила *К*, *W*, *С*, *Х*, выюд 3 можно построить: (1) как продолжение К при Л (выражение с"к> Ф означает, что в наборе Ф нет оба h такого, что с <-» И) или при А <т> ®; (2) как продолжение 91 при Л 1<-»/'или при А А.

В дальнейшем предполагаем, что А]^> А@;Лх>А;Лх>/'. Пусть у = (г,Д а).

Гипотеза индукции: допустим, что по любым выводам К и 91 и индикатору т при р [К, 91, т] < у можно указать вывод 3 секвенцииН.

Рассмотрим выводы К и 91 и индикатор г > 0 такие, что р [К, 91, г] = у. Здесь <р[Щ> \ и ср [91] > 1. Доказательство существования вывода 3 проведем путем разбора случаев построения заключительных секвенцийEnGвыводов К и91.

Если Е или G получена по одному из операциональных правил *П*, *Р*, *1 *, то индикатор главного его члена Рfg, 1 g или Y\f как слова (оба), независимо от выводов, убывает при переходе к указанным в посылках оснащенным М-формулам fng.g или fc.

Заметим, что случаи <р [К] = 1 или ср [91] = 1 уже рассмотрены: вывод 3 получен как продолжение одного из данных выводов X или 91.

Разбор различных случаев далее в доказательстве леммы о смешении осуществляем точно так, как это делается в литературе, начиная с публикаций Г. Генцена (1934 г.) для логики предикатов 1-го порядка и автора (с 1973 г.) в классах выводов таких, как М или КЧГ, бести-повых двухъярусных секвенциальных исчислений. Остановимся на «новых» правилах *А,*.

Рассмотрим случаи применения правил *Х*, являющихся последними в К или 91. При вычеркивании В ^г, когда, например, применяется правило X* со второй посылкой С —>D, где С <-» А, по гипотезе индукции, обращаясь к выводу первой (дедуктивной) посылки правила X*, вычеркиваются и все оснащенные М-формулы D ^г, поскольку /) о- А. т.е. сразу строится искомый вывод 3 секвенции Н. Так, можно сказать, «согласованы» правила *Х* и лемма о смешении.

Лемма о смешении в КЧГ доказана.

Доказательство непротиворечивости КЧГ относительно отрицания