Искусственный интеллект - [153]
В дальнейшем предполагаем, что А]^> А@;Лх>А;Лх>/'. Пусть у = (г,Д а).
Гипотеза индукции: допустим, что по любым выводам К и 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 секвенции Н. Так, можно сказать, «согласованы» правила *Х* и лемма о смешении.
Лемма о смешении в КЧГ доказана.
Доказательство непротиворечивости КЧГ относительно отрицания
Предположим, что КЧГ противоречива. Тогда по определению в КЧГ выводимы, в частности, секвенции => В>s и =>(1 By для некоторой оснащенной М-формулы В*. Из секвенции => В>s по правилу *1 следует секвенция (1 Д)>я| => ®, где ® - пустой набор. Применив к выводам секвенций =xW и(\В)>1 =^>® Теорему Cut, получим в КЧГ вывод «пустой» секвенции <8>=><8>, что невозможно (см. [20,21]) - поскольку постулаты исчисления КЧГ не кончаются «пустыми» секвенциями. Поэтому теория КЧГ непротиворечива относительно отрицания, что и требовалось доказать.
Теперь читателю рекомендуется прочесть еще раз [20,21], заменяя исчисление М на КЧГ и понимая под непротиворечивостью и непротиворечивость относительно отрицания 1.
Обратим внимание на работу «Solution of Hilbert Central Problem Following Kolmogorov» [25], являющуюся переводом [21] на английский язык. В [25] название [21] получило естественное уточнение.
Центральная проблема Гильберта впервые решена автором по Колмогорову; при этом в [20, 21, 25] непротиворечивость теорий М и, следовательно, КЧГ понимается только абсолютно, в данной работе доказывается, что КЧГ непротиворечива и относительно отрицания 1.
В доказательстве непротиворечивости КЧГ относительно отрицания используется абсолютная непротиворечивость КЧГ, то есть если теория КЧГ непротиворечива абсолютно, то она непротиворечива и относительно отрицания. Из абсолютной непротиворечивости КЧГ следует её непротиворечивость и относительно отрицания. А абсолютная непротиворечивость вытекает непосредственно из построения КЧГ точно так же, как в [20, 21] это делается для теории М.
Поэтому для теории КЧГ, как у Г. Генцена для логики (предикатов 1-го порядка), непротиворечивость относительно отрицания является следствием построения соответствующего исчисления КЧГ или (как у Генцена) логики предикатов.
При этом КЧГ выступает как логика с генценовскими постулатами ( / ), К* - *1, расширенная алгоритмическим исчислением ^-конверсии А. Чёрча [20, IV, п. 6], представляющим теоретико-множественное свертывание Г. Кантора; связь между свертыванием и логикой осуществляется правилами *А,*. В таком смысле можно рассматривать теорию КЧГ как логический вариант (с аналогом теоремы К. Гёделя 1930 г. о полноте) формализации КТМ (канторовской теории множеств). Причем (с точностью до языка) «парадокс» КТМ, формульно выражаемый А и ~\А, представляется в КЧГ выводимыми дедуктивными секвенциями =>А>К и =>(14)>г с различными индикаторами к иг.
Итак, два яруса исчисления КЧГ, как аналоги двух составляющих КМ, позволяют в КЧГ применением двух принципов КТМ, представленных в КЧГ логическими и алгоритмическими постулатами, получить в соответствии с программой А.Н. Колмогорова доказуемо полным и непротиворечивым образом все выводы КМ без ограничений естественно на основе колмогоровского пакета законов рассуждений, заданного указываемыми по постулатам исчисления КЧГ всеми свойствами выводимости при замене символа => на знак выводимости |-, или секвенциально в исчислении КЧГ.
Первый алгоритмический ярус КЧГ с его неразрешимостью используется не только при построении 2-го, логического, яруса КЧГ, но и при задании исходных элементов (М-термов и М-формул) исчисления КЧГ, а также в других случаях.
