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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

V. Построение теории Кантора - Чёрча - Генцена (КЧГ)

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

Этот результат естественно распространить на построение исчисления КЧГ по исчислению М из [20] следующим образом.

Первый ярус исчисления М в КЧГ сохраняется без изменений; во 2-ом ярусе вместо правила подъема ¹¹⁵ из [20], не уменьшая общности, возьмем схему аксиом

(/'): (А⁰ => А⁰), где А - атомарная формула (но в М, с термами и М-термами), имеющая по определению индикатор 0, то есть А является оснащенной атомарной М-формулой с индикатором 0;

правила К¹¹⁵ - ¹¹⁵А из [20] сохраняются, только в них все дедуктивные секвенции состоят из оснащенных М-формул; при этом правила П¹¹⁵ - ¹¹⁵А определяют индуктивно по построению выводов соответствующие индикаторы главных членов (что отражает в КЧГ известное определение рангов (по Генцену 1934 г.) формул логики предикатов), правила П¹¹⁵ - ¹¹⁵А имеют следующий вид.

П¹¹⁵: Г=>0. (avf-; ¹¹⁵П: (acf. Г=>0 ;

Г=>0, (Пд)^г~ (Ш)^Г|,Г^0

Р¹¹⁵: d. Г=>0.d ; Г=>0, (Рае)"

1¹¹⁵: d. Г=>0 Г=>0,(Ь)^г|

*Р: (А=>А d) (d Г^01 ; (Pae)^rs',A, Г=>А, 0

А,¹¹⁵: (А=>А. d) (а—н:)

А^А,е^г

(в—>а) (d.Г=>©1 в\Г=>0

(в правилах г и s - произвольные индуктивно определенные (по гипотезе индукции) индикаторы, вводимые по посылкам правил; ограничения на у и с, указанные в [20], естественно сохраняются). Построение теории КЧГ закончено.

Исчисление, в котором все М-формулы дедуктивной части являются оснащенными, будем называть оснащенным исчислением. Аналогично КЧГ можно строить после известных результатов Г. Генцена 1934 г. оснащенные секвенциальные исчисления логики предикатов 1-го порядка.

VI. Теорема Cut и непротиворечивость теории Кантора -Чёрча - Генцена

Формулировка Теоремы Cut

Если в КЧГ выводимы секвенции (А => Л, А^г ) и (А^г, Г=> 0), то в КЧГ существует вывод секвенции (А, Г=>Л, 0), где А есть М-формула с индикатором г; А, Г, Л. ©суть наборы оснащенных М-формул.