 Gentzen did not deal explicitly with infinite proof trees in his second published proof of the consistency of PA (Gentzen 1938b). However, in the unpublished first consistency proof of Gentzen 1974 he aims at showing that a proof of a sequent in first-order arithmetic gives rise to a a well-founded reduction tree; that tree can be identified with a cut-free proof in the sequent calculus with the \(\omega\)-rule. The infinitary version of PA with the \(\omega\)-rule was investigated by Schütte (1950). There remained the puzzle, how Gentzen’s work that used an ingenious method of assigning ordinals to purported proofs of the empty sequent relates to the infinitary approach. Much later work by Buchholz (1997) and others revealed an intrinsic connection between Gentzen’s assignment of ordinals to deductions in PA and the standard one to infinite deductions in \(\PA_{\omega}\). In the 1950s infinitary proof theory flourished in the hands of Schütte. He extended his approach to PA to systems of ramified analysis to be discussed below in  section 5.2.