Ytukyg

My understanding is that there exist ordinals which ZFC cannot prove really are ordinals, i.e. that they are well-founded.

I don't understand how this can be. Doesn't the iterative von Neumann construction of ordinals eventually reach every ordinal? I'm referring to the proof that every well-ordered set has a bijection with a von Neumann ordinal.

Maybe it proofs that every well-ordered set is an ordinal, but it doesn't know the extension of "the well-ordered sets"?

There are several issues here.

An obvious one is that there are only so many proofs and many more ordinals, so there are ordinals that we cannot even refer to within the theory, so of course the theory cannot prove anything about them.

This is somewhat subtle, as there are models of set theory that are pointwise definable, so that any $x$ in the model is definable in the model. In particular, every ordinal of the model is definable. But we cannot quite express this in the language of set theory, so to simplify manners, assume here that our ambient metatheory is powerful enough that we can discuss definability in set theory. To illustrate why this is subtle, the fact that there is a formula $phi$ that in the model defines an ordinal (that is, the model $M$ satisfies that there is a unique $x$ such that $phi(x)$, and that $x$ is an ordinal) doesn't mean that $mathsf{ZFC}$ proves that $phi$ defines a unique object, and even if it does, it still doesn't mean that $mathsf{ZFC}$ proves that that object is an ordinal. To make things worse, the model does not even have to be well-founded, or even an $omega$-model.

But there is more: if that pointwise definable model is well-founded, then its height is an ordinal that surely we cannot even describe in $mathsf{ZFC}$ in a way that we can prove its existence (if we could, the model would see it!). On the other hand, if the model is ill-founded, then there is an ordinal $gamma$ that is a proper initial segment of the ordinals of the model and yet it is indescribable within the model ($gamma$ could even be $omega$, and yet what the model thinks is $omega$ would be something else).

What I think, however, is the real issue, is that what one really wants is to talk about fairly explicit well-orderings of (subsets of) the natural numbers that are, say, recursive. Being recursive is sufficiently robust that we can talk about it in the theory. We can discuss the well-ordering because we can discuss the Turing machine that lists it. The question is then whether $mathsf{ZFC}$ can prove the well-foundedness of any such well-ordering. Note that this is also a subtle issue, as we are not quite talking of well-orderings but rather of specific ways of representing them: The same well-ordering can be listed by many different Turing machines. Of some of them, $mathsf{ZFC}$ may be able to prove that the linear ordering it describes is well-founded. Of some others, $mathsf{ZFC}$ may not even be able to prove that what is being listed is a linear ordering. Even if we restrict ourselves to machines that $mathsf{ZFC}$ can prove list linear orderings, there are some that $mathsf{ZFC}$ won't prove form a well-founded ordering. This is just a consequence of the fact that $mathsf{ZFC}$ is subject to the incompleteness theorem: it is not an issue that we can solve even if we change the theory to something much stronger, even if we restrict our attention to machines that only list 0. To see this, think for instance of a machine that at each stage $n$ simply lists 0, unless there is some $mle n$ such that $m$ codes a proof of an inconsistency in your theory, in which case from that point on it proceeds to list an infinite decreasing chain ordered like the negative integers.

It may seem that this is somewhat unsatisfactory since we know that 0 is well-founded and we just chose the wrong machine to talk about it. That is a fair point, but it doesn't solve much. Trying to push these ideas and seeing how far they take us leads us into ordinal analysis, which is a topic I recommend you investigate to further clarify these issues. For example, Peano Arithmetic cannot prove that orderings of $omega$ of type $varepsilon_0$ are well-founded. Something similar happens with $mathsf{ZFC}$ and its proof-theoretic ordinal. But the truth is that we understand very little of ordinal analysis at this level of generality. What little we know is that, by an argument rather similar to the one at the end of the previous paragraph, there are total recursive functions whose totality is not provable within the system.

This is one of the reasons why we care about good systems of notation for ordinals: they would allow us to define a (long!) fast-growing hierarchy of total recursive functions $f_alpha!:omegatoomega$ such that any total recursive function whose totality is provable in $mathsf{ZFC}$ is eventually dominated by (i.e., grows slower than) one of the $f_alpha$. This gives us a way to measure ways in which $mathsf{ZFC}$ fails to describe an ordinal: it would be an index $alpha$ of a function $f_alpha$ not provably total in the theory. This is precisely what happens in Peano arithmetic with $varepsilon_0$. Again, some of this is speculative since current systems of notation stop well short of reaching the heights required here.

This is a subtle issue, and Noah Schweber will come soon enough to write way more than I could. But let me give you an abbreviated version.

Inside a model of ZFC we have some fixed collection of ordinals, and these ordinals all exist there, and they are well-founded. But models are semantics. They are about actual objects in a particular interpretation. And different models could have different ordinals, in fact some models could be entirely ill-founded!

But provability is about proofs. This is a syntactic question now, not about a particular model with particular collection of ordinals. Just on paper, what can you prove to be a well-ordering.

The point is that in a given meta-theory, we can ask what relations on $Bbb N$ can be proved to be well-founded. But since there are only countably many proofs, there are only countably many ordinals that are provably well-founded.

If you want to think about it, think about it like this: take a countable model of ZFC. How many ordinals does it know? How many ordinals can we define over that model? Still only countably many. How does that fit with the fact that the ordinals make a proper class?