Тем самым впервые Центральная проблема Гильберта построения доказуемо полных и доказуемо непротиворечивых (как абсолютно, так и относительно отрицания 1) оснований классической теоретикомножественной математики КМ в виде одного (хотя и двухъярусного) исчисления решается автором по Колмогорову.
На основании сказанного теория КЧГ строится как двухъярусное секвенциальное исчисление М (без постулируемого правила сечения) из [20, 21]. В отличие от [20, 21] дедуктивные секвенции как слова вида (1=>Ф) имеют наборы I и Ф, в которые могут входить только вводимые в данной работе оснащенные М-формулы (оснащение М-формул в работе осуществляется с помощью индикаторов).
Результат получает завершение ниже формулируемой и доказанной Теоремой Cut (о допустимости в КЧГ правила сечения), из которой в дополнение к абсолютной непротиворечивости [20,21], вытекает непротиворечивость КЧГ относительно отрицания 1: не существует оснащенной М-формулы Bs такой, что в КЧГ выводимы две секвенции (=>BS) и (=>(|В)''). где В есть М-формула, s и s| суть индикаторы.
Формулировка и доказательство Теоремы Cut в случае КЧГ осуществляются точно так, как это делается в соответствующей секвенциальной (генценовской) логике предикатов (1-го порядка) без постулируемого правила сечения с тем новшеством, что и аналог ранга логических формул участвует в построении двухярусного исчисления КЧГ.
Непротиворечивость относительно ] следует из Теоремы Cut в случае КЧГ точно так же, как в случае соответствующей генценовской секвенциальной логики предикатов.
Построив исчисление КЧГ, показываем, что в нем известные «парадоксы» отражаются выводимыми дедуктивными секвенциями, не влияющими на непротиворечивость КЧГ (еще до доказательства Теоремы Cut). Так, например, «парадокс» Б. Рассела 1902 г. представляется выводимыми в КЧГ секвенциями (=>Dr) и (=>(1 D)K|), где г и к - различные индикаторы (ср. в исчислении М из [20] две выводимые секвенции (=>D) и (=>~|D), но «пустая» секвенция ®=>®, где ® - пустой набор слов, в М по его построению не выводима - как принято говорить, исчисление М (абсолютно) непротиворечиво (см. [20, 21]); имея две указанные выводимые секвенции и невыводимость пустой секвенции, легко доказываем недопустимость в М из [20, 21] правила сечения).
Подчеркнём, что здесь, вопреки сложившейся практике, слово «парадокс» взято в кавычки, так как подразумеваемого под словом «парадокс» противоречия в данном случае нет.
Всё богатство КМ сохраняется в КЧГ, а выводимые в КЧГ типа «расселовских» секвенции =>Dr и =>(lD)K| (с различными индикаторами гик) можно рассматривать, следуя Хаскеллу Карри (1900— 1981), как «монстры», не влияющие на непротиворечивость КЧГ.
Отметим особую роль исчисления Х-конверсии А. Чёрча [20, ГУ, п. 6] не только в теории КЧГ (например, 1-ый ярус КЧГ образует само исчисление /.-конверсии), но и в метатеории этой теории КЧГ. Так, конвертируемость [20, IV, п. 7] заменяет равенство объектов (обов) [20, IV, п. 3], являясь его обобщением (см. постулаты ^-конверсии [20, IV, п. 6] как обобщающие известные свойства равенства). Она (конвертируемость) используется и при образовании исходных элементов (М-термов и М-формул) исчисления КЧГ.
Вообще, можно говорить о внутренней замкнутости теории КЧГ на себя: всё в теории КЧГ и её метатеории определяется средствами теории КЧГ с учетом двух ярусов КЧГ, отражающих две составляющие (компоненты) КМ.
Отношение конвертируемости, как известно, неразрешимо (это один из фундаментальных алгоритмических результатов школы Шейнфинкеля-Карри-Чёрча). В работе используется закон «исключенного третьего» с рассмотрением всех соответствующих случаев.
IV. Оснащенные М-формулы и индикаторы
В связи с предлагаемым доказательством Теоремы Cut к пункту 9 определения М-формул и М-термов [20, IV, с. 741-742] добавим новый подпункт (замыкая по определению указанные в нем классы объектов (обов) относительно подстановки):
Если А - атомарная формула, формула, М-формула или М-терм, Ъ есть М-терм, х - переменная, то об [Ых\ А (результат подстановки Ь вместо х в А, естественно определяемой средствами ^-конверсии) считаем по определению соответственно атомарной формулой, формулой, М-формулой и М-термом.