Normalization proof for Peano arithmetic (Q892146): Difference between revisions

The main purpose of the paper is to prove normalization of Peano arithmetic formulated in a standard natural deduction with an ordinal assignment originating in Howard's normalization proof for Gödel's T. The result is a generalization of an argument found in an earlier paper by \textit{A. Kanckos} [Math. Log. Q. 56, No. 6, 611--624 (2010; Zbl 1219.03072)] where a consistency proof for Heyting arithmetic was given.