Predicative definition and existence of ordinal numbers

Question

I was thinking about ordinal numbers recently, after I have read the wiki article about impredicativity. Now I have trouble to find a predicative definition of ordinal numbers, or even a "predicatively valid" ZFC-proof, that omega_1 (the first uncountable von Neumann ordinal) exists. Let me explain what I mean. By Gödels completeness theorem, every true ZFC statement can be syntactically proved from ZFC axioms using a proper deductive system (like the Hilbert calculus). The axiom of infinity "proves" the existence of omega_0. Using the axiom of pairing and the axiom of union, one can then prove the existence of omega_0 + 1, and so on. There are only countably many "and so ons", as any proof has finite length and uses finitely many symbols. So the description of omega_1 as "the set of all countable ordinals" is not a predicative definition, because we cannot prove the existence of every countable ordinal individually (since we believe that there are uncountably many), and then collect them into a new set.

So I was looking for another proof and read that hartogs lemma can prove the existence of omega_1. As I understand the proof of the lemma, it takes the class of ordinals as given. Essentially (for our special case of omega_1) it goes this way (from planetmath.org):

• Let alpha be the class of all countable ordinals:
  • Prove that alpha is a set.
  • Prove that alpha is an ordinal.
  • Prove that alpha is not countable.

From my point of view, this is not a predicatively valid proof of existence for two reasons:

1. One cannot assume that alpha exists in order to prove that it exists. Temporary naming that thing a class does not count.
2. ZFC does not talk about classes, so the proof of hartogs lemma seems to be metamathematical. Can the lemma be proved from ZFC axioms alone (in Gödels sense)?

So what am I missing and where am I wrong?

Edit 1:

Since I cannot comment with my reputation score, I will refine my question. I want to comment on Noah's fifth bullet point in the proof of hartogs lemma: The axiom of replacement needs three things:

• a set $A$
• A collection $C$ of sets.
• a class function $f:A\to C$

Then replacement states, that the image $f[A]$ is also a set. The collection $C$ comes from nowhere. Don't we need to prove that $C$ and $f$ exist? Does not seem so, but why not?

Wikipedia actually introduces the axiom via a relation $P$: "Suppose $P$ is a definable binary relation". Well, I can suppose, but in order to use it, I should be obligated to prove that it exists. And secondly: any definable relation? Not a relation that provably exists as a set in the universe, but any? Consider the following axiomatic system $\mathcal A$:

1. $\emptyset$ exists.
2. $\{\emptyset\}$ exists.
3. Axiom of replacement.

The universe $\left\{ \emptyset, \{\emptyset\} \right\}$ seems to be a model of $\mathcal A$, as well as $\left\{ \emptyset, \{\emptyset\}, 42 \right\}$. However, I shouldn't be able to prove the existence of 42 from $\mathcal A$. But let us define a binary relation $\left\{ (\emptyset, 42) \right\}$. Does replacement prove the existence of $\{42\}$?

EDIT 2:

This edit refers to Noahs Edit 1. Noah, thank you for pointing out my mistake with those 42-models and your patience. Let us look again at the upper axiomatic system $\mathcal A$. I won't try to construct a complete model any more, but want to discuss some sets that must exist in any model. Following your argument in your Edit 1, there must exist $\emptyset$, $\{ \emptyset \}$, $\{\{ \emptyset \} \}$, $\{\{\{ \emptyset \}\}\}$ ..., correct? If so, I am fine with that. Now I want to define a formula $\phi(x,y)$ which states that $y = \{ x, \{x\} \}$. I won't try to write down the actual FO formula, but I am confident that it exists, as ordered tuples are defined in a similar way. Can I use $\{\emptyset\}$ and $\phi$ within replacement to prove the existence of $\{ \emptyset, \{\emptyset \} \}$? I should not be able to, because I need its existence as a set in order to verify the axioms antecedent in the first place. So it boils down to the question: When I replace a set $S$ with a thing $T$, have I proved beforehand, that $T$ exists as a set?

Your proof which you have introduced with "Why is it that every $S \in \mathcal W$ has a corresponding $\alpha_S$?" apparently does exactly this. But as a layman, I am not sure if it does really. Your proof goes this way:

• If there is no corresponding ordinal to an $S$, you construct one (namely $A$) from other (apparently smaller) ordinals $\alpha_n$.
• Your construction of $A$ uses replacement with $\alpha_n$ as targets.

Is it possible to prove that every $\alpha_n$ exists as a set, beforehand? I would not doubt the existence of $\alpha_n$ and $A$ if an ordinal could be defined as the set of all smaller ordinals. However in the scope of this thread, I accept this definition only up to some large countable ordinal (probably Feferman-Schütte?).

The only safe definition I have found for ordinals is this one on Wikipedia:

A set $S$ is an ordinal if and only if $S$ is strictly well-ordered with respect to set membership and every element of $S$ is also a subset of $S$.

That definition does not give us anything about existence, though. Wikipedia further states that

it can be shown by transfinite induction that every well-ordered set is order-isomorphic to exactly one of these ordinals".

For the scope of this thread, I would probably reject this proof because of two reasons:

• Transfinite induction and recursion rely on ordinals, so I cannot use them in order to prove their existence.
• Is transfinite induction actually a tool a Gödel-proof could use (i.e. no metamathematics)?

EDIT 3:

To revise my last two questions:

• Transfinite induction does not rely on ordinals, but on well-orders.
• It is not metamathematics but provable from the axioms.

So when TI is used on a well-ordered set, then I am fine with it. Noahs argument "Why is it that every $S \in \mathcal W$ has a corresponding $\alpha_S$?" actually mimics the proof-by-contradiction that shows the general validity of TI. This also answers my question in Edit 2:

• Is it possible to prove that every $\alpha_n$ exists as a set, beforehand?

$\rightarrow$ Yes, it exists by the induction hypothesis.

Answer 1

EDIT: The following addresses your edits.

You seem to misunderstand the axiom of Replacement. Replacement really does say that given any definable relation $R$, and any set $X$, if for all $x\in X$ there is exactly one $y$ such that $xRy$ (that is: $R$ is really a function), then the set $\{y: \exists x\in X(xRy)\}$ exists. Note that we don't need to talk about a "target class" $C$, either.

Specifically, Replacement is an axiom scheme: for every formula $\varphi$, there is an axiom $$R_\varphi:\quad \forall \overline{a}\forall X[\forall x\in X\exists!y(\varphi(x, y, \overline{a}))\implies \exists z\forall w(w\in z\iff \exists u\in X(\varphi(u, w, \overline{a})))].$$ (There are multiple ways of phrasing this; Collection e.g. is slightly different.) So you do not need to "prove that the function exists". Similarly, you don't need to prove that the target of the function exists.

The example you give is a misunderstanding of model theory. Neither of the sets $\{\emptyset, \{\emptyset\}\}$ and $\{\emptyset,\{\emptyset\}, \{42\}\}$ satisfy Replacement, but not because of the example you describe. In the former, you can't build $\{42\}$ though since the formula defining the function you want relies on having a parameter for $42$. That is, the issue with this relation isn't that it doesn't exist as a set in the first structure, but rather that it isn't even definable in the first structure!

The reason these structures don't satisfy Replacement is that Replacement implies that, as long as there is some set which is nonempty, then every set's singleton exists. Specifically, suppose $D$ satisfies replacement, and $x, y\in D$ with $a\in b$, and $c\in D$ is arbitrary. Then consider the formula $\varphi(x, y)\equiv$"$y=c$" (note that this formula uses a parameter in the structure, so that's fine). Applying Replacement to this formula, with starting set $b$, implies that $\{c\}$ exists.

---

The proof you've outlined isn't quite correct. Here's how it really goes:

• We have the set of natural numbers $\omega$.

• By the Powerset axiom and Separation, we can get the set $\mathcal{R}$ of (sets of ordered pairs of naturals).

• Again via Separation, we get the subset $\mathcal{W}$ of $\mathcal{R}$ consisting of elements of $\mathcal{R}$ which are well-orderings of a subset of $\omega$: that is, $\mathcal{W}=\{S\in\mathcal{R}$: $S$ is a transitive, antisymmetric, total relation on a subset of $\omega$ with no descending chain$\}$.

• Now we observe that for every $S\in\mathcal{W}$, there is exactly one ordinal $\alpha_S$ such that $S$ and $\alpha_S$ have the same order-type. (Note that this isn't obvious! I'll say more about it below, but for now I'll skip over it.)

• Apply Replacement! (This is crucial, and without Replacement $\omega_1$ might not exist - see e.g. my answer to this question.) We get a set $B$ such that $x\in B\iff \exists S\in\mathcal{W}(x=\alpha_S)$. It's now not hard to show that this $B$ is indeed exactly the set of countable ordinals.

---

Why is it that every $S\in\mathcal{W}$ has a corresponding $\alpha_S$? Well, suppose otherwise. Then we can find an $S$ such that for every $n\in dom(S)$, the strictly smaller order $S_n$ of elements less than $n$ (formally: $S_n$ has domain $dom(S_n)=\{m\in dom(S): m<_{S}n\}$, and ordering $\{(a, b)\in dom(S_n)^2: a<_{S}b\}$) is in order-preserving bijection with some ordinal $\alpha_n$. (This is a good exercise.)

OK, now applying Replacement to $\{S_n: n\in dom(S)\}$ we get a set of countable ordinals $A=\{\alpha_n: n\in dom(S)\}$. But it is easy to show that $A$ is in fact an ordinal, and is in order-preserving bijection with $S$; a contradiction.