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

Предположим, что КЧГ противоречива. Тогда по определению в КЧГ выводимы, в частности, секвенции => В ^s и =>(1 By для некоторой оснащенной М-формулы В*. Из секвенции => В ^s по правилу *1 следует секвенция (1 Д)^я| => ®, где ® - пустой набор. Применив к выводам секвенций =xW и(\В) ¹ =^>® Теорему 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] проводит формализацию в известной аксиоматической системе Г. Фреге.

При этом соответствующие определения и конструкции в КЧГ можно ввести, следуя за определениями и построениями В.К. Захарова и А.В. Михалева (см., например, [27]) общей концепции произвольной математической системы в рамках теории множеств NBG Неймана - Бернайса- Гёделя.

Подробности о неразрешимых бесгиповых алгоритмических исчислениях чистой комбинаторной логики Шейнфинкеля-Карри и X-конверсии Чёрча (не образующих теории 1-го порядка, но каждое из которых, обладающее неограниченной комбинаторной полнотой, можно положить в основу двухъярусной секвенциальной теории типа КЧГ) хорошо изложены, например, в монографиях Барендрегта 1985 г. и Вольфенгагена 2004 г. [28, 29] (см. также библ. в [28, 29], работу Резуса 1982 г. [30], труд Хиндли и Кардоне 2005 г. по истории ^.-исчисления и комбинаторной логики [31]). Указанная неограниченная комбинаторная полнота (Х-полнота) является принятой в КЧГ формализацией неограниченного канторовского теоретико-множественного свертывания.