Теперь определим индикаторы как (конечные, возможно, пустые) слова в однобуквенном алфавите | (буква «палочка»). Для пустого индикатора введем обозначение 0.
Если а есть индикатор, то а | называем индикатором.
Для индикатора | используем обозначение 1 («единица»). Соответственно, для индикатора | | используем обозначение 2 («два») и так далее. Так, к примеру, 5 есть индикатор | | 11 |. Таким образом, все (натуральные) числа в работе воспринимаем как индикаторы.
По индукции доказываем, что конкатенация а[3 индикаторов а и /3 является индикатором (иногда вместо аД пишем а+Д).
Ниже равенство слов в алфавите | означает совпадение слов.
Считается, что индикатор s не равен индикатору г, если существует непустой индикатор t такой, что или s = rt, или г = st.
Аналогично вводится неравенство г < s и другие знаки для индикаторов.
Определим далее новые слова, называемые М-формулами с индикаторами следующим образом:
Если А есть М-формула и г - индикатор, то конкатенация Аг называется М-формулой с индикатором г, иногда пишем ind (А) = г.
Наконец, М-формулы с индикаторами будем называть оснащенными М-формулами.
Далее большими греческими буквами будем обозначать конечные (возможно пустые) упорядоченные наборы (списки) оснащенных М-формул. Слово (Г => А) называем дедуктивной секвенцией (ср. [20]), в отличие от [20] в дедуктивных секвенциях наборы состоят из оснащенных М-формул, пустой набор иногда обозначается ®.
V. Построение теории Кантора - Чёрча - Генцена (КЧГ)
Как известно, в схеме аксиом - основной секвенции Генцена (А => А) - секвенциального формализма логики предикатов, не уменьшая общности, можно ограничиться только случаем атомарной формулы А.
Этот результат естественно распространить на построение исчисления КЧГ по исчислению М из [20] следующим образом.
Первый ярус исчисления М в КЧГ сохраняется без изменений; во 2-ом ярусе вместо правила подъема 115 из [20], не уменьшая общности, возьмем схему аксиом
(/'): (А0 => А0), где А - атомарная формула (но в М, с термами и М-термами), имеющая по определению индикатор 0, то есть А является оснащенной атомарной М-формулой с индикатором 0;
правила К115 - 115А из [20] сохраняются, только в них все дедуктивные секвенции состоят из оснащенных М-формул; при этом правила П115 - 115А определяют индуктивно по построению выводов соответствующие индикаторы главных членов (что отражает в КЧГ известное определение рангов (по Генцену 1934 г.) формул логики предикатов), правила П115 - 115А имеют следующий вид.
П115: Г=>0. (avf- ; 115П: (acf. Г=>0 ;
Г=>0, (Пд)г~ (Ш)Г|,Г^0
Р115: d. Г=>0.d ; Г=>0, (Рае)"
1115: d. Г=>0 Г=>0,(Ь)г|
*Р: (А=>А d) (d Г^01 ; (Pae)rs',A, Г=>А, 0
А,115: (А=>А. d) (а—н:)
А^А,ег
(в—>а) (d. Г=>©1 в\ Г=>0
(в правилах г и s - произвольные индуктивно определенные (по гипотезе индукции) индикаторы, вводимые по посылкам правил; ограничения на у и с, указанные в [20], естественно сохраняются). Построение теории КЧГ закончено.
Исчисление, в котором все М-формулы дедуктивной части являются оснащенными, будем называть оснащенным исчислением. Аналогично КЧГ можно строить после известных результатов Г. Генцена 1934 г. оснащенные секвенциальные исчисления логики предикатов 1-го порядка.
VI. Теорема Cut и непротиворечивость теории Кантора -Чёрча - Генцена
Формулировка Теоремы Cut
Если в КЧГ выводимы секвенции (А => Л, Аг ) и (Аг, Г=> 0), то в КЧГ существует вывод секвенции (А, Г=>Л, 0), где А есть М-формула с индикатором г; А, Г, Л. ©суть наборы оснащенных М-формул.