  Reductive proof theory in this sense has followed two traditions: the first, mainly carried out by proof theorists following Gentzen and Schütte, has pursued a program of what is called ordinal analysis, and is exemplified by Gentzen’s first consistency proof of \(\PA\) by induction up to \(\varepsilon_0 . \varepsilon_0\) is a certain transfinite (though countable) ordinal, however, “induction up to \(\varepsilon_0\)” in the sense used here is not a genuinely transfinite procedure. Ordinal analysis does not operate with infinite ordinal numbers, but rather with ordinal notation systems which themselves can be formalized in very weak (essentially, finitary) systems. An ordinal analysis of a system \(T\) is given if: (a) one can produce an ordinal notation system which mimics the ordinals less than some ordinal \(\alpha_T\) so that (b) it can be proved finitarily that the formalization \(TI(\alpha_T)\) of the principle of induction up to \(\alpha_T\) implies the consistency of \(T\) (i.e., \(S \vdash TI(\alpha_T)\rightarrow Con_T)\) and (c) \(T\) proves \(TI(\beta)\) for all \(\beta \lt \alpha_T\) (\(S\) is a theory formalizing finitary metamathematics and is generally a weak sub-theory of \(T)\). To have any foundational significance it is also required that one can give a constructive argument for transfinite induction up to \(\alpha_T\). As mentioned above, this was done for by Gentzen and Takeuti for \(\varepsilon_0\), the proof theoretic ordinal of \(\PA\), but becomes more difficult and of progressively questionable philosophical significance for stronger theories.