Normalization proof for Peano Arithmetic

摘要

A proof of normalization for a classical system of Peano Arithmetic formulated in natural deduction is given. The classical rule of the system is the rule for indirect proof restricted to atomic formulas. This rule does not, due to the restriction, interfere with the standard detour conversions. The convertible detours, numerical inductions and instances of indirect proof concluding falsity are reduced in a way that decreases a vector assigned to the derivation. By interpreting the expressions of the vectors as ordinals each derivation is assigned an ordinal less than E > (0). The vector assignment, which proves termination of the procedure, originates in a normalization proof for Godel's T by Howard (Intuitionism and proof theory. North-Holland, Amsterdam, 1970).