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

Рассмотрим случаи применения правил *Х*, являющихся последними в К или 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] проводит формализацию в известной аксиоматической системе Г. Фреге.

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

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

С логическими секвенциальными конструкциями, используемыми в КЧГ, читатель может предварительно познакомиться, например, по известным трудам Генцена, Клини, Ершова и Палютина [32-34].

Когда данная работа была уже подготовлена к печати, автор ознакомился со статьей В.Я. Яцука [35], которую можно рассматривать как введение в предмет; процитирую частично резюме из [35]:

«АКЛ (аппликативная компьютерная логика) представляет собой систему прикладного исчисления секвенций с неограниченным принципом свертывания в форме комбинаторной полноты и состоит из двух частей, первая из которых называется теорией выводимости и является инвариантной к рассматриваемым областям знания. Вторая часть отражает конкретное знание о заданной предметной области. Теория выводимости реализуется в виде двух ступеней: алгоритмической и структурной. Логические связки (с некоторыми ограничениями - А.С.К.) определяются в рамках заданного комбинаторнополного базиса и могут быть выведены автоматически» ([35], с. 29).

В статье [35] имеется интересное неформальное введение (с. 29-30).

Настоящая работа выполнена на кафедре теории вероятностей в кабинете истории и методологии математики и механики механикоматематического факультета МГУ. Впервые основные её положения были доложены 22 апреля 2002 г. на научной конференции «Ломоносовские чтения МГУ».