 One last remark about the use of ordinals: Gentzen showed that transfinite induction up to the ordinal \(\varepsilon_0\) suffices to prove the consistency of PA. Using the arithmetized formalization of the proof predicate (see above, after  Definition 1.3)  and taking k as the numeral denoting the Gödel number of the formula \(0=1\), we can express the consistency of PA, \(\Con (\PA)\), by the formula \(\forall x \,\neg\proof_{\PA}(x,k)\). To appreciate Gentzen’s result it is pivotal to note that he applied transfinite induction up to \(\varepsilon_0\) only for primitive recursive predicates (the latter principle was denoted above by PR-TI\((\varepsilon_0)\)). Otherwise, Gentzen’s proof used only finistist means. Hence, a more accurate formulation of Gentzen’s result is 