Финитное исследование трансфинитных выводов

Рассматриваются $\omega$-выводы арифметических формул. В первой части строится примитивно рекурсивный оператор нормализации $E$. Он устраняет сечение не только из рекурсивно описанных выводов (то есть фундированных фигур), но также из произвольных (не обязательно фундированных) фигур, построенных из аксиом по правилам вывода. Это позволяет применить $E$ в теории моделей. Его применения в теории доказательств основаны на формализуемости основных свойств $E$ в примитивно рекурсивной арифметике.
Во второй части доказывается устранимость сечения в гейтинговской арифметике $HA^{\omega}+AC$ с аксиомой выбора для всех конечных типов. Формулировка, допускающая устранение сечения, использует термы, сопоставляемые выводам по методу Карри, Говарда,Жирара, Мартин–Лефа. Эти термы включаются в сами формулировки правил. В качестве одного из следствий получается консервативность $HA^{\omega}+AC$ над $HA$. Библ. – 11 назв.