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

В работе предлагается вариант реализации программы А.Н. Колмогорова по основаниям математики. Впервые показывается, что КМ (классическая теоретико-множественная математика) доказуемо полностью и доказуемо непротиворечиво (как абсолютно, так и относительно отрицания ] ) представляется одним исчислением (теорией).

Теория строится ступенчато по Андрею Андреевичу Маркову (1903-1979) в виде двухъярусного секвенциального исчисления, названного автором КЧГ (исчислением Кантора-Чёрча-Генцена): первый ярус задаёт неограниченное теоретико-множественное свёртывание Г. Кантора в алгоритмической (вычислительной) форме исчисления ^-конверсии Алонзо Чёрча (1903-1995); второй ярус задаёт классическую логику (предикатов 1-го порядка) в секвенциальной (без постулируемого правила сечения) форме Герхарда Генцена (1909-1945); связь между ярусами обеспечивают правила *Х и X* (пишем: *Х*), введенные автором и названные канторовскими (см., например, [20]). Такие двухъярусные исчисления строятся, следуя идее ступенчатых конструкций А.Н. Колмогорова и А.А. Маркова, исследуются автором на механико-математическом факультете МГУ с 1968 г. и публикуются с 1970 г.

Тем самым впервые Центральная проблема Гильберта построения доказуемо полных и доказуемо непротиворечивых (как абсолютно, так и относительно отрицания 1) оснований классической теоретикомножественной математики КМ в виде одного (хотя и двухъярусного) исчисления решается автором по Колмогорову.

На основании сказанного теория КЧГ строится как двухъярусное секвенциальное исчисление М (без постулируемого правила сечения) из [20, 21]. В отличие от [20, 21] дедуктивные секвенции как слова вида (1=>Ф) имеют наборы I и Ф, в которые могут входить только вводимые в данной работе оснащенные М-формулы (оснащение М-формул в работе осуществляется с помощью индикаторов).

Результат получает завершение ниже формулируемой и доказанной Теоремой Cut (о допустимости в КЧГ правила сечения), из которой в дополнение к абсолютной непротиворечивости [20,21], вытекает непротиворечивость КЧГ относительно отрицания 1: не существует оснащенной М-формулы B sтакой, что в КЧГ выводимы две секвенции (=>B S) и (=>(|В)''). где В есть М-формула, s и s| суть индикаторы.

Формулировка и доказательство Теоремы Cut в случае КЧГ осуществляются точно так, как это делается в соответствующей секвенциальной (генценовской) логике предикатов (1-го порядка) без постулируемого правила сечения с тем новшеством, что и аналог ранга логических формул участвует в построении двухярусного исчисления КЧГ.

Непротиворечивость относительно ] следует из Теоремы Cut в случае КЧГ точно так же, как в случае соответствующей генценовской секвенциальной логики предикатов.

Построив исчисление КЧГ, показываем, что в нем известные «парадоксы» отражаются выводимыми дедуктивными секвенциями, не влияющими на непротиворечивость КЧГ (еще до доказательства Теоремы Cut). Так, например, «парадокс» Б. Рассела 1902 г. представляется выводимыми в КЧГ секвенциями (=>D r) и (=>(1 D) K|), где г и к - различные индикаторы (ср. в исчислении М из [20] две выводимые секвенции (=>D) и (=>~|D), но «пустая» секвенция ®=>®, где ® - пустой набор слов, в М по его построению не выводима - как принято говорить, исчисление М (абсолютно) непротиворечиво (см. [20, 21]); имея две указанные выводимые секвенции и невыводимость пустой секвенции, легко доказываем недопустимость в М из [20, 21] правила сечения).

Подчеркнём, что здесь, вопреки сложившейся практике, слово «парадокс» взято в кавычки, так как подразумеваемого под словом «парадокс» противоречия в данном случае нет.

Всё богатство КМ сохраняется в КЧГ, а выводимые в КЧГ типа «расселовских» секвенции =>D rи =>(lD) K| (сразличными индикаторами гик) можно рассматривать, следуя Хаскеллу Карри (1900— 1981), как «монстры», не влияющие на непротиворечивость КЧГ.

Отметим особую роль исчисления Х-конверсии А. Чёрча [20, ГУ, п. 6] не только в теории КЧГ (например, 1-ый ярус КЧГ образует само исчисление /.-конверсии), но и в метатеории этой теории КЧГ. Так, конвертируемость [20, IV, п. 7] заменяет равенство объектов (обов) [20, IV, п. 3], являясь его обобщением (см. постулаты ^-конверсии [20, IV, п. 6] как обобщающие известные свойства равенства). Она (конвертируемость) используется и при образовании исходных элементов (М-термов и М-формул) исчисления КЧГ.

Вообще, можно говорить о внутренней замкнутости теории КЧГ на себя: всё в теории КЧГ и её метатеории определяется средствами теории КЧГ с учетом двух ярусов КЧГ, отражающих две составляющие (компоненты) КМ.

Отношение конвертируемости, как известно, неразрешимо (это один из фундаментальных алгоритмических результатов школы Шейнфинкеля-Карри-Чёрча). В работе используется закон «исключенного третьего» с рассмотрением всех соответствующих случаев.

IV. Оснащенные М-формулы и индикаторы

В связи с предлагаемым доказательством Теоремы Cut к пункту 9 определения М-формул и М-термов [20, IV, с. 741-742] добавим новый подпункт (замыкая по определению указанные в нем классы объектов (обов) относительно подстановки):

Если А - атомарная формула, формула, М-формула или М-терм, Ъ есть М-терм, х - переменная, то об [Ых\ А (результат подстановки Ь вместо х в А, естественно определяемой средствами ^-конверсии) считаем по определению соответственно атомарной формулой, формулой, М-формулой и М-термом.

Теперь определим индикаторы как (конечные, возможно, пустые) слова в однобуквенном алфавите | (буква «палочка»). Для пустого индикатора введем обозначение 0.

Если а есть индикатор, то а | называем индикатором.

Для индикатора | используем обозначение 1 («единица»). Соответственно, для индикатора | | используем обозначение 2 («два») и так далее. Так, к примеру, 5 есть индикатор | | 11 |. Таким образом, все (натуральные) числа в работе воспринимаем как индикаторы.

По индукции доказываем, что конкатенация а[3 индикаторов а и /3 является индикатором (иногда вместо аД пишем а+Д).

Ниже равенство слов в алфавите | означает совпадение слов.

Считается, что индикатор s не равен индикатору г, если существует непустой индикатор t такой, что или s = rt, или г = st.

Аналогично вводится неравенство г < s и другие знаки для индикаторов.

Определим далее новые слова, называемые М -формулами с индикаторами следующим образом:

Если А есть М-формула и г - индикатор, то конкатенация А гназывается М-формулой с индикатором г , иногда пишем ind (А) = г.

Наконец, М-формулы с индикаторами будем называть оснащенными М-формулами.

Далее большими греческими буквами будем обозначать конечные (возможно пустые) упорядоченные наборы (списки) оснащенных М-формул. Слово (Г => А) называем дедуктивной секвенцией (ср. [20]), в отличие от [20] в дедуктивных секвенциях наборы состоят из оснащенных М-формул, пустой набор иногда обозначается ®.