Рассмотрим случаи применения правил *Х*, являющихся последними в К или 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-го, логического, яруса КЧГ, но и при задании исходных элементов (М-термов и М-формул) исчисления КЧГ, а также в других случаях.
Реализация программы А.Н. Колмогорова
В статьях [20, 21, 25] и настоящей работе показано, что КМ, имея две компоненты и базируясь на двух принципах КТМ, доказуемо полностью и доказуемо непротиворечиво представляется двухъярусным секвенциальным исчислением (теорией) Кантора - Чёрча - Ген-цена (КЧГ).
Таким образом, программа А.Н. Колмогорова по основаниям математики реализована.
Формализацию областей математики, основания которых образует КТМ или ее части, можно осуществить в КЧГ аналогично тому, как, например, Уильям С. Хэтчер [26] проводит формализацию в известной аксиоматической системе Г. Фреге.