# Gentzen's consistency proof

That said, there are other, more powerful 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.

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.

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

Another proofs of consistency of Arithmetic were published by S. Artemov (in 2019). In the Artemov's paper it has been stated that the proof published there, is formalizable in Peano Arithmetic.

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