Can we avoid talking about proper classes by talking about models?

Intuitively, we can define the ordinal numbers $\mathsf{On}$ as the closure of $\{0\}$ with respect to successorship $x \mapsto x \cup \{x\}$ and (set-sized) unions. Arguably the most natural way to implement this idea is to write $\mathsf{On} = \bigcap \mathcal{A},$ where $\mathcal{A}$ is the collection of all classes that include $\{0\}$ and which are closed with respect to the aforementioned operations. However, this approach cannot work within ZFC, as there are no proper classes, let alone collections thereof. This issue isn't specifically an issue with the definition of the ordinals; it also occurs when defining the Surreal numbers, for example.

There's at least two standard solutions to this problem.

1. Work in a more expressive set theory.
2. Define the ordinals (surreals etc.) in a different way.

Suppose neither solution appeals to us. Well if television and fantasy books have taught me nothing else (and they haven't), its that there's always a third way. So my question is:

Can we work around the problem by talking about models of ZFC?

For instance, I was thinking we could define a new function symbol $\mathsf{On}$ such that if a set $M$ is a standard model of second-order ZFC, then $\mathsf{On}^M$ are the ordinals of $M.$ From this point of view, we can define $\mathsf{On}^M$ using the approach via closure described in the preceding paragraph, since $M$ is a set. Furthermore, I think that we can introduce such a function symbol $\mathsf{On}$ without even knowing whether or not ZFC has any models.

Now suppose we want to prove something about the ordinals. Like, we wish to show that every non-empty subclass of the ordinals has a minimum element. I imagine that we can instead prove that for all standard models $M$ of second order ZFC, we have that every non-empty subset of $\mathsf{On}^M$ has a minimum element. From this, I imagine that we may deduce the metatheorem that given a definable unary predicate in the language of ZFC such that at least one ordinal satisfies that predicate, there exists a least ordinal satisfying that predicate. I think this approach works even though we can't prove that a standard model $M$ of second order ZFC actually exists.

Does this sort of thing actually work, or is there a subtlety that I'm missing?

Edit. As Andreas Blass explains in his answer, taking $M$ to be a standard model of second-order ZFC doesn't work, because it prevents the completeness theorem from applying. But, can we solve this by allowing M to be an arbitrary model of first-order ZFC? More generally, is the idea salvageable?

• Just a remark on notation, it's usually common to denote the ordinals of $M$ by $\sf Ord^\it M$, or $\sf On^\it M$. Jul 10 '13 at 7:48
• @AsafKaragila, thanks, I changed it. Just out of curiosity, what's the usual notation for the cardinals of $M$? Jul 10 '13 at 7:50
• I've seen $\sf Card^\it M$, and I've seen $\Gamma(M)$, and I've seen more. I don't recall seeing a standard notation for that. The first is the most likely candidate to b one, though. Jul 10 '13 at 9:00
• @AsafKaragila, thanks. Please let me know if there's anything I can do to improve the question, as it doesn't seem to have generated much interest so far. Jul 10 '13 at 9:04

If you prove that some statement is true in all standard models of second-order ZFC, you cannot infer that it (or a reformulation using definable predicates instead of classes) is provable in ZFC. The first counterexample that comes to mind is the statement that ZFC is consistent; it's true in all standard models of second-order ZFC and in fact even in all standard models of first-order ZFC, but it's not provable in ZFC. Another example to keep in mind is "there is a standard model of first-order ZFC", which is true in all standard models of second-order ZFC but not in all standard models (let alone in all models) of (fisrst-order) ZFC. Also, if you really want to confine attention to statements "about ordinals", then use the equivalent formulation of my second example as "there is an ordinal $\alpha$ such that $L_\alpha$, the constructible hierarchy up to stage $\alpha$, satisfies first-order ZFC."
• @user18921: If ZFC has no models then there is a proof of the number theoretical statement $\neg$Con(ZFC). That cannot be encoded by a standard integer, so if a model has only standard integers it must agree that ZFC is consistent, and much more. Jul 10 '13 at 7:27