 where F, as above, contains only finitistically acceptable means. In his 1943 paper Gentzen also showed that this result is best possible, as PA proves transfinite induction up to any \(\alpha&lt;\varepsilon_0\). So one might argue that the non-finitist part of PA is encapsulated in PR-TI\((\varepsilon_0)\) and therefore “measured” by \(\varepsilon_0\). \(\varepsilon_0\) is also the proof-theoretic ordinal of PA as specified in  Definition 3.4.  Gentzen hoped that results of this character could also be obtained for stronger mathematical theories, in particular for analysis. Hilbert’s famous second problem asked for a direct consistency proof of that mathematical theory. Gentzen wrote in 1938 that