Proof-theoretic ordinal

Remarks

Example: for Peano arithmetic, $\abs{\mathrm{PA}} = \varepsilon_0$, the ordinal epsilon nought. Gentzen showed that PA proves transfinite induction along a standard notation system for each ordinal below $\varepsilon_0$, and not along the one for $\varepsilon_0$ itself. Non-example: the least uncountable ordinal $\omega_1$ is not the proof-theoretic ordinal of any such theory, because a computable well-order on $\N$ has countable order type. Suppose that every computable order that $T$ proves well-founded is in fact well-founded. Then $\abs{T}$ is below the Church–Kleene ordinal $\omega_1^{\mathrm{CK}}$, the least ordinal that is not the order type of a computable well-order. Several inequivalent definitions are in use, for example with primitive recursive in place of computable orders, or with $\Pi^0_2$ consequences in place of well-foundedness. For the usual theories they give the same ordinal.