How can any theory prove well-foundedness of ordinals above $\omega_1^{\text{CK}}$? $\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.
 A: This is a difference between internal and external quantification.  Proof-theoretic ordinal analysis involves an external quantification over (external, recursive) ordinals.  What is provable in ZFC is an internal quantification over (internal) ordinals.
Skolem’s Paradox is the classic illustration of why one can’t generally expect internal and external interpretations of a statement to be equivalent.
A: Just slightly expanding the comment of Emil Jeřábek: on one hand, in ZFC we can define some objects we call ordinals and prove transfinite induction of each of them. This is not what we mean by the ordinal of ZFC. The latter is defined roughly as follows (although there are several nonequivalent definitions):


*

*You take some recursive relation, such that in the actual natural numbers, this relation is well-founded and you actually fix some algorithm which describes this relation (as a set of pairs). 

*Then you ask, whether the theory in question proves that the relation given by this algorithm is a well-founded one.
For instance, think of the following relation $R$: $R(m,n)$ iff $m<n$ and there is no proof of $0 \neq 0$ from the axiom of ZFC using less than  $m$ symbols or $m>n$ otherwise. This relation is easily verified to be a recursive linear order by even very weak theories but is  wellfounded (namely isomorphic to $\omega$) iff ZFC is consistent, so ZFC does not even prove that $\omega$ is well-founded under totally arbitrary presentation of $\omega$.
Notice that the above example could give an impression that no theory can have its prof-theoretic ordinal bigger than $\omega,$ therefore precise definition of this concept is a rather subtle issue and there are several nonequivalent definitions. But the rough idea, of what may go wrong is precisely this.      
