 Using the Hauptsatz and its Corollary, Gentzen was able to capture all of the consistency results that had been obtained prior to 1934 including Herbrand’s, that had been called by Gödel in his 1933 “the most far-reaching” result. They had been obtained at least in principle for fragments of elementary number theory; in practice, Gentzen did not include the quantifier-free induction principle. Having completed his dissertation, Gentzen went back to investigate natural deduction calculi and obtained in 1935 his first consistency proof for full first-order arithmetic. He formulated, however, the natural calculus now in “sequent form”: instead of indicating the assumptions on which a particular claim depended by the undischarged ones in its proof tree, they are attached now to every node of the tree. The “sequents” that are being proved are of the form \(\Gamma \Rightarrow A\), where all the logical inferences are carried out on the right hand side. This proof was published only in 1974; it was subsequently analyzed most carefully in Tait 2015 and Buchholz 2015. It was due to criticism of Bernays and Gödel that Gentzen modified his consistency proof quite dramatically; he made use of transfinite induction, as will be discussed in detail in the next section. Here we just mention that Bernays extensively discussed transfinite induction in Grundlagen der Mathematik II. The main issue for Bernays was the question, is it still a finitist principle?—Bernays did not discuss, however, two other aspects of Gentzen’s work, namely, the use of structural features of formal proofs for consistency proofs and the attempt of gaining a constructive, semantic understanding of intuitionist arithmetic. The former became crucial for proof theoretic investigations; the latter influenced Gödel and his functional interpretation via computable functionals of finite  type.[14]  The two aspects together opened a new era for proof theory and mathematical logic with the goal of proving the consistency of analysis. We will see, how far current techniques lead us and what foundational significance one can attribute to them.