Новая последовательность редукций для арифметики

Главный тип результатов теории доказательств, имеющих внешние приложения – это теоремы нормализации: любой вывод может быть приведен к нормальной форме с помощью конечного числа стандартных преобразований (редукций). Оценка сходимости процесса нормализации дает оценку роста доказуемо рекурсивных функций, нашедшую недавно приложение в финитной комбинаторике (J. Paris, L. Harrington, A mathematical incompleteness in Peano arithmetic. “Handhook of mathematical logic”, 1978, 1133–1142). Определение редукций для исчисления предикатов и арифметики принадлежат Генцену, который доказал теорему нормализации для выводов атомарных формул и дал оценку сходимости с помощью назначения выводам $d$ ординалов $0(d)<\varepsilon_0$ таким образом, что $0(d)>0(\bar d)$ для редукции $\bar d$ вывода $d$. Позднее сходимость была доказана для произвольных выводов, однако малая наглядность выбора $\bar d$ и доказательства убывания ординалов затрудняют понимание и изложение: как Такеути (Takeuti G. Proof Theory, North Holand, 1975),так и Шютте (РЖМат 1978.7A48K), ограничиваются выводами атомарных формул.
В реферируемой статье приводится более короткая и наглядная конструкция редукции $\bar d$ и назначения ординалов, позволяющая упростить также доказательство убывания ординалов. Источник всех упрощений – идейная связь с предложенным автором непрерывным оператором устранения сечения из бесконечных выводов. В частности, символ $0_k(d)$, в терминах которого, определяется $0(d)$, можно читать "ординальная высота вывода, получаемого после устранения сечений степени $\geq k$ из бесконечного вывода, в который стандартным образом перестраивается $d$". Рассматривается $L$-формулировка, где имеются правила введения связок в антецедент и сукцедент. Распространение на натуральную формулировку получается с помощью перевода по Правицу. Библ. –9 назв.