Gentzen's theorem is concerned with first-order arithmetic: the theory of the natural numbers, including their addition and multiplication, axiomatized by the first-order Peano axioms. This is a "first-order" theory: the quantifiers extend over natural numbers, but not over sets or functions of natural numbers. The theory is strong enough to describe recursively defined integer functions such as exponentiation, factorials or the Fibonacci sequence.

Gentzen showed that the consistency of the first-order Peano axioms is provable over the base theory of primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal ε₀. Primitive recursive arithmetic is a much simplified form of arithmetic that is rather uncontroversial. The additional principle means, informally, that there is a well-ordering on the set of finite rooted trees. Formally, ε₀ is the first ordinal ${\displaystyle \alpha }$  such that ${\displaystyle \omega ^{\alpha }=\alpha }$ , i.e. the limit of the sequence

${\displaystyle \omega ,\ \omega ^{\omega },\ \omega ^{\omega ^{\omega }},\ \ldots }$ 

It is a countable ordinal much smaller than large countable ordinals. To express ordinals in the language of arithmetic, an ordinal notation is needed, i.e. a way to assign natural numbers to ordinals less than ε₀. This can be done in various ways, one example provided by Cantor's normal form theorem. Gentzen's proof is based on the following assumption: for any quantifier-free formula A(x), if there is an ordinal a< ε₀ for which A(a) is false, then there is a least such ordinal.

Gentzen defines a notion of "reduction procedure" for proofs in Peano arithmetic. For a given proof, such a procedure produces a tree of proofs, with the given one serving as the root of the tree, and the other proofs being, in a sense, "simpler" than the given one. This increasing simplicity is formalized by attaching an ordinal < ε₀ to every proof, and showing that, as one moves down the tree, these ordinals get smaller with every step. He then shows that if there were a proof of a contradiction, the reduction procedure would result in an infinite strictly descending sequence of ordinals smaller than ε₀ produced by a primitive recursive operation on proofs corresponding to a quantifier-free formula.^[1]

Gentzen's proof highlights one commonly missed aspect of Gödel's second incompleteness theorem. It is sometimes claimed that the consistency of a theory can only be proved in a stronger theory. Gentzen's theory obtained by adding quantifier-free transfinite induction to primitive recursive arithmetic proves the consistency of first-order Peano arithmetic (PA) but does not contain PA. For example, it does not prove ordinary mathematical induction for all formulae, whereas PA does (since all instances of induction are axioms of PA). Gentzen's theory is not contained in PA, either, however, since it can prove a number-theoretical fact—the consistency of PA—that PA cannot. Therefore, the two theories are, in one sense, incomparable.

That said, there are other, finer ways to compare the strength of theories, the most important of which is defined in terms of the notion of interpretability. It can be shown that, if one theory T is interpretable in another B, then T is consistent if B is. (Indeed, this is a large point of the notion of interpretability.) And, assuming that T is not extremely weak, T itself will be able to prove this very conditional: If B is consistent, then so is T. Hence, T cannot prove that B is consistent, by the second incompleteness theorem, whereas B may well be able to prove that T is consistent. This is what motivates the idea of using interpretability to compare theories, i.e., the thought that, if B interprets T, then B is at least as strong (in the sense of 'consistency strength') as T is.

A strong form of the second incompleteness theorem, proved by Pavel Pudlák,^[2] who was building on earlier work by Solomon Feferman,^[3] states that no consistent theory T that contains Robinson arithmetic, Q, can interpret Q plus Con(T), the statement that T is consistent. By contrast, Q+Con(T) does interpret T, by a strong form of the arithmetized completeness theorem. So Q+Con(T) is always stronger (in one good sense) than T is. But Gentzen's theory trivially interprets Q+Con(PA), since it contains Q and proves Con(PA), and so Gentzen's theory interprets PA. But, by Pudlák's result, PA cannot interpret Gentzen's theory, since Gentzen's theory (as just said) interprets Q+Con(PA), and interpretability is transitive. That is: If PA did interpret Gentzen's theory, then it would also interpret Q+Con(PA) and so would be inconsistent, by Pudlák's result. So, in the sense of consistency strength, as characterized by interpretability, Gentzen's theory is stronger than Peano arithmetic.

Hermann Weyl made the following comment in 1946 regarding the significance of Gentzen's consistency result following the devastating impact of Gödel's 1931 incompleteness result on Hilbert's plan to prove the consistency of mathematics.^[4]

It is likely that all mathematicians ultimately would have accepted Hilbert's approach had he been able to carry it out successfully. The first steps were inspiring and promising. But then Gödel dealt it a terrific blow (1931), from which it has not yet recovered. Gödel enumerated the symbols, formulas, and sequences of formulas in Hilbert's formalism in a certain way, and thus transformed the assertion of consistency into an arithmetic proposition. He could show that this proposition can neither be proved nor disproved within the formalism. This can mean only two things: either the reasoning by which a proof of consistency is given must contain some argument that has no formal counterpart within the system, i.e., we have not succeeded in completely formalizing the procedure of mathematical induction; or hope for a strictly "finitistic" proof of consistency must be given up altogether. When G. Gentzen finally succeeded in proving the consistency of arithmetic he trespassed those limits indeed by claiming as evident a type of reasoning that penetrates into Cantor's "second class of ordinal numbers."

Kleene (2009, p. 479) made the following comment in 1952 on the significance of Gentzen's result, particularly in the context of the formalist program which was initiated by Hilbert.

The original proposals of the formalists to make classical mathematics secure by a consistency proof did not contemplate that such a method as transfinite induction up to ε₀ would have to be used. To what extent the Gentzen proof can be accepted as securing classical number theory in the sense of that problem formulation is in the present state of affairs a matter for individual judgement, depending on how ready one is to accept induction up to ε₀ as a finitary method.

In contrast, Bernays (1967) commented on whether Hilbert's confinement to finitary methods was too restrictive:

It thus became apparent that the 'finite Standpunkt' is not the only alternative to classical ways of reasoning and is not necessarily implied by the idea of proof theory. An enlarging of the methods of proof theory was therefore suggested: instead of a reduction to finitist methods of reasoning, it was required only that the arguments be of a constructive character, allowing us to deal with more general forms of inference.

Gentzen's first version of his consistency proof was not published during his lifetime because Paul Bernays had objected to a method implicitly used in the proof. The modified proof, described above, was published in 1936 in the Annals. Gentzen went on to publish two more consistency proofs, one in 1938 and one in 1943. All of these are contained in (Gentzen & Szabo 1969).

Kurt Gödel reinterpreted Gentzen's 1936 proof in a lecture in 1938 in what came to be known as the no-counterexample interpretation. Both the original proof and the reformulation can be understood in game-theoretic terms. (Tait 2005).

In 1940 Wilhelm Ackermann published another consistency proof for Peano arithmetic, also using the ordinal ε₀.

Another proof of consistency of Arithmetic was published by I. N. Khlodovskii, in 1959.

Yet other proofs of consistency of Arithmetic were published by: T. J. Stępień and Ł. T. Stępień (in 2018) and by S. Artemov (in 2019). In the Stępieńs' paper it has been claimed that the proof of consistency (published there), of the Arithmetic System, is done within this System.^{[citation needed]}

In Artemov's paper it has been stated that the proof published there, is formalizable in Peano Arithmetic.^{[citation needed]}

Gentzen's proof is the first example of what is called proof-theoretic ordinal analysis. In ordinal analysis one gauges the strength of theories by measuring how large the (constructive) ordinals are that can be proven to be well-ordered, or equivalently for how large a (constructive) ordinal can transfinite induction be proven. A constructive ordinal is the order type of a recursive well-ordering of natural numbers.

In this language, Gentzen's work establishes that the proof-theoretic ordinal of first-order Peano arithmetic is ε₀.

Laurence Kirby and Jeff Paris proved in 1982 that Goodstein's theorem cannot be proven in Peano arithmetic. Their proof was based on Gentzen's theorem.

• Artemov, S. (2019), "The Provability of Consistency", arXiv:1902.07404 [math.LO]
• Edwards, Paul, ed. (1967). "Paul Bernays". Encyclopedia of Philosophy. Vol. 3. MacMillan and Free Press. p. 502.
• Feferman, Solomon (1960). "Arithmetization of metamathematics in a general setting". Fundamenta Mathematicae. 49 (1): 35–92. doi:10.4064/fm-49-1-35-92. ISSN 0016-2736.
• Gentzen, Gerhard (1936), "Die Widerspruchsfreiheit der reinen Zahlentheorie", Mathematische Annalen, 112: 493–565, doi:10.1007/BF01565428, S2CID 122719892 – Translated as "The consistency of arithmetic", in (Gentzen & Szabo 1969).
• Gentzen, Gerhard (1938), "Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie", Forschungen zur Logik und zur Grundlegung der Exakten Wissenschaften, 4: 19–44 – Translated as "New version of the consistency proof for elementary number theory", in (Gentzen & Szabo 1969).
• Gentzen, Gerhard (1969), Szabo, M. E. (ed.), Collected Papers of Gerhard Gentzen, Studies in logic and the foundations of mathematics (Hardcover ed.), Amsterdam: North-Holland, ISBN 978-0-7204-2254-2 - an English translation of papers.
• Gödel, K. (2001) [1938], "Lecture at Zilsel's", in Feferman, Solomon (ed.), Kurt Gödel: Collected Works, vol. III Unpublished Essays and Lectures (Paperback ed.), Oxford University Press Inc., pp. 87–113, ISBN 978-0-19-514722-3
• Jervell, Herman Ruge (1999), A course in proof theory (textbook draft ed.), archived from the original on 2011-06-07
• Khlodovskii, I. N. (1959), "A new proof of the consistency of arithmetic" (PDF), Uspekhi Mat. Nauk, 14 (6(90)): 105–140
• Kirby, L.; Paris, J. (1982), "Accessible independence results for Peano arithmetic" (PDF), Bull. London Math. Soc., 14 (4): 285–293, CiteSeerX 10.1.1.107.3303, doi:10.1112/blms/14.4.285, archived from the original (PDF) on 2014-09-12
• Kleene, Stephen Cole (2009) [1952]. Introduction to metamathematics. Ishi Press International. ISBN 978-0-923891-57-2.
• Pudlák, Pavel (1 June 1985). "Cuts, Consistency Statements and Interpretations". Journal of Symbolic Logic. 50 (2): 423–441. doi:10.2307/2274231. ISSN 0022-4812. JSTOR 2274231.
• Stępień, T. J.; Stępień, Ł. T. (2018), "On the Consistency of the Arithmetic System", arXiv:1803.11072 [math.LO]
• Tait, W. W. (2005), "Gödel's reformulation of Gentzen's first consistency proof for arithmetic: the no-counterexample interpretation" (PDF), The Bulletin of Symbolic Logic, 11 (2): 225–238, doi:10.2178/bsl/1120231632, ISSN 1079-8986, S2CID 9481361
• Weyl, Hermann (2012). Levels of infinity: Selected writings on mathematics and philosophy. New York: Dover Publications. ISBN 978-0-486-48903-2.