Искусственный интеллект - [151]

Тем самым впервые Центральная проблема Гильберта построения доказуемо полных и доказуемо непротиворечивых (как абсолютно, так и относительно отрицания 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 и другие знаки для индикаторов.

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