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 (1