Gentzen's consistency proof without heightlines (Q2377348)

A proof of the consistency of a sequent calculus for intuitionistic arithmetic is proposed. The proof is based on the Gentzen-style assignment of ordinals to the derivations but does not use the so-called heightline argument, which means that the ordinal assigned to a sequent depends on the height of the sequent. Instead, the techniques proposed by Howard for Gödel's system \(T\) [\textit{W. A. Howard}, in: Intuitionism Proof Theory, Proc. Summer Conf. Buffalo N.Y. 1968, 443--458 (1970; Zbl 0206.28202)] is used. Namely an expression is assigned to every sequent and a vector of expressions is assigned to a derivation. Further, the first expression in the vector is interpreted as an ordinal. The author describes a procedure of transforming derivations of the empty sequent which reduces that ordinal. This provides the consistency of the system.