A normal form for arithmetical derivations implying the \(\omega\)-consistency of arithmetic (Q1375747)

A derivation in Peano Arithmetic PA is strongly irreducible (s.i.) if it does not contain redundant free variables, redundant inductions (induction term is closed), redundant cuts (no cut formula is obtained by induction) or \(\forall\)-antecedent with side formula derivable in PA. If an s.i. derivation of a sentence \(\neg \forall xA(x)\) is given, the lowermost \(\forall\)-antecedent inference has side formula \(A(n)\) underivable in PA. Hence the proposition SI stating that every derivable formula has an s.i. derivation implies \(\omega\)-consistency of PA. The author proves this proposition using induction up to \(\varepsilon_1\) by the method of Gentzen's second consistency proof. The proposition SI extends the reviewer's normal form theorem from Ann. Pure Appl. Log. 62, 65-79 (1993; Zbl 0786.03040). T. Arai noticed that SI can be extended from PA to any theory and even to any finite sequence of increasing theories. This extension has an easy model-theoretic proof using ideas of the reviewer's paper [loc. cit.].