$\newcommand{\omegaoneck}{\omega_1^{\text{CK}}}$ Pardon the extremely basic question - this isn't quite my area - but I'm confused about the definition of proof theoretic ordinals.

The proof theoretic ordinal of a theory is defined to be the smallest ordinal that the theory cannot prove is well founded. In other words, it gives us a measure of how much transfinite induction the theory allows us to do. There is a countable ordinal $\omegaoneck$ such that every recursive theory has a proof theoretic ordinal $\alpha\in\omegaoneck$.

This seems fine, except that there exist recursive theories (such as ZFC) in which we can prove transfinite induction over all ordinals. My first thought was that perhaps ZFC can't prove the existence of ordinals larger than its own proof-theoretic ordinal $\omega_{ZFC}$, so 'induction over all ordinals' is the same as 'induction up to $\omega_{ZFC}$', within ZFC. But that can't be true: ZFC can prove Hartogs' Lemma, which gives us arbitrarily large ordinals (and they can be shown to be arbitrarily large within ZFC).

One possibility might be that ZFC can't reason about its own proof-theoretic ordinal, and can't show that it's less than any given ordinal. But that seems rather strange, given that ZFC can construct ordinals such as $\omega_1$ that are far far larger than even $\omegaoneck$, even in cardinality.

recursiveordinal the theory cannot prove well-founded. ZFC thinks it can prove the well-foundedness of crazy huge ordinals, but it does not know how to represent them by recursive relations on the integers. $\endgroup$ – Emil Jeřábek Jan 27 '16 at 12:00thenask if the theory proves it well-founded (which, for ZFC, might involve unwinding the recursive definition into the von Neumann representation that ZFC internally uses for ordinals). One reason for this is to have a comparison across theories: say, ZFC has an ordinal it calls $\omega_3$, and a fancy theory X (that does not look at all like set theory) has an ordinal it calls PSM9. Are they the same? Which one is longer? These would be meaningless questions, ... $\endgroup$ – Emil Jeřábek Jan 27 '16 at 12:19canask about the same ordinal in two different theories. $\endgroup$ – Emil Jeřábek Jan 27 '16 at 12:20