Extended normal form theorems for logical proofs from axioms (Q1575930)

The authors (and others) have been working on refinements of cut elimination and their implications. The main theorem of this paper states: if a sequent \(A_0,\dots, A_n\to A_{n+1}\) is provable (in predicate calculus), then it has an irreducible proof with respect to \(A_0,\dots,A_n\). Here, the \(A\)'s are sets of closed formulas, and a proof is said to be irreducible if it is cut-free, free variables in it are eigen-variables or occur in the endsequent, and the main formula of an inference has a descendent in \(A_{i+1}\), \(i\leq n\), and it is not provable or refutable from \(A_0,\dots,A_i\), according as the formula is in the antecedent or in the succedent. A consequence of this theorem is the \(\omega\)-consistency of PA. Another consequence of a proof -- which is in the fashion of Gentzen's second consistency proof -- is the provable equivalence (over PRA) of the theorem itself with the 2-consistency \(\text{RFN}_{\Sigma_2} (C_{n+1})\), for recursive \(A_0,\dots,A_n\). Here, `RFN' stands for `reflection scheme', and \(C_n\) is obtained successively from \(\text{PA}\) \((=C_1)\) by \(C_{n+1}: =\text{qf-Ind}+ C_n+\text{RFN}(C_n)\).