Читаем Искусственный интеллект полностью

- принципиальное отличие предложенных и опубликованных автором с 1970 г. секвенциальных исчислений, имеющих два яруса, от широко известных одноярусных Аристотелевских аксиоматических исчислений Гильбертовского типа (с ограничениями теоремами Гёделя о неполноте);

- необходимость изучения по Колмогорову канторовской («наивной») теории множеств с её двумя неограниченными принципами, на основе которых строятся все выводы единой КМ (без каких-либо ограничений).

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

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

Тем самым впервые Центральная проблема Гильберта построения доказуемо полных и доказуемо непротиворечивых (как абсолютно, так и относительно отрицания 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] как обобщающие известные свойства равенства). Она (конвертируемость) используется и при образовании исходных элементов (М-термов и М-формул) исчисления КЧГ.

Перейти на страницу:

Похожие книги