In post 13 I sketched proof by transfinite induction, and definition by transfinite recursion. Let’s take a closer look at that. By definition, < means ∈ for ordinals—treat that also as vernacular. Sometimes one symbol or the other makes the meaning clearer. We must keep in mind though that we have not shown that < is a well-ordering on Ω, or even a simple ordering.
Let Ω(x) be the formula for “x is an ordinal”, thus:
| (∀u,v)(u∈v∈x → u∈x) |
| ∧(∀u,v∈x)(u<v ∨ v<u ∨ u=v) |
| ∧(∀u∈x)(¬u<u) |
| ∧(∀u,v∈x)(¬(u<v ∧ v<u)) |
| ∧(∀u,v,w∈x)(u<v<w → u<w) |
| ∧(∀y⊆x)(y≠∅ → ∃u(u∈y ∧ ∀v(¬(v<u ∧ v∈y)))) |
The first line says x is transitive, the next four lines say that < simply-orders x, and the last line says that < is a well-ordering on x. (Quite a bit of vernacular, but by now you should know how to deal with “u∈v∈x’’, for example.)
The clauses are not as economical as possible: for example, Foundation implies the third and last line, and a transitive irreflexive relation is automatically asymmetric, so even without Foundation we don’t need the fourth line. For the moment, we proceed without using Foundation.
Within an ordinal, ∈ well-orders; we want to bootstrap this to all of Ω. First an easy observation. Given a formula φ(x), if any β∈α satisfy φ, then there is a least such β. We need only invoke Separation to provide us with the set of all β∈α satisfying φ, and then appeal to the last clause in the definition of an ordinal.
How about smallest elements over all of Ω? That is,
∃αφ(α)→∃α(φ(α) ∧ ∀β(¬(β<α∧φ(β))))
(By vernacular convention, α and β are ordinals. Formally one begins “∃x(Ω(x)∧φ(x))…’’.)
Suppose ∃γφ(γ). If none of γ’s predecessors satisfy φ, then we’re done. Otherwise suppose φ(α) with α∈γ. Because γ is well-ordered, there is is an element of γ—let’s still call it α—such that α is the smallest element of the set {β∈γ:φ(β)}. We need to know that there are no ordinals, period, that satisfy φ and precede α. But if β was such an ordinal, we’d have β∈α∈γ. Since γ is transitive, we’d have β∈γ, and we’ve already ruled that out.
The contrapositive is transfinite induction. Letting ψ be ¬φ,
∀α((∀β<α)ψ(β)→ψ(α)) → ∀αψ(α)
With transfinite induction, we can show that Ω is simply-ordered. Only trichotomy presents any wrinkles. We induct on the property, “α is comparable with every ordinal.” Suppose this is true for all β<α. Let γ be an arbitrary ordinal. If γ<β or γ=β for some β∈α, then γ<α, since α is transitive (and < means ∈). Suppose then that β∈γ for all β∈α. That is, α⊆γ. If α=γ, we’re done. Suppose α⊂γ. Let δ be the smallest element of γ∖α. We will now show that α=δ, proving α∈γ, i.e., α<γ.
The key point: both α and δ are subsets of γ, and within γ, ∈ is a simple ordering. Extensionality kicks in: we have to prove x∈α↔x∈δ, or turned around, x∉δ↔x∉α. Now, α is an initial segment of γ because α is transitive. Therefore δ>x for all x∈α because δ∉α. So x∉δ implies x≥δ implies x∉α. On the other hand, x∉α implies x>y for all y∈α, again because α is an initial segment. Since δ is the least element of γ∖α, it follows that x≥δ, i.e., ¬x<δ, i.e., x∉δ. We’re done.
So < is a well-ordering on Ω, and we can trust our intuition about it (mostly).
Next consider transfinite recursion. The discussion in post 13 applies, with a few remarks. As before, we have a “rule” ρ(α,f,s) that assigns a value s to an ordinal α given as input a function f:α→···. Our rule is a formula, and may even include parameters. Thus: ρ(α,f,s,p̄).
Suppose that for the parameter values p̄=c̄ this formula is “function-like”; then we’re in business. One proves in ZF that the following condition
∀α,f ∃s ρ(α,f,s,c̄)
∧ ∀α,f,s,t (ρ(α,f,s,c̄)∧ρ(α,f,t,c̄)→s=t)
implies, for all α, the existence of a unique function gα:α+1→··· “obeying the recursion”. The proof uses transfinite induction, of course; also the set-existence axioms, especially Replacement. I won’t comb out all the hair, but essentially: if we have an “obedient” gβ for all β<α, Replacement plus Union plus the uniqueness allow you to combine all these gβ’s into one fα with domain α. Then you use ρ to assign a value to α, extending fα to gα.
The conclusion, even leavened with vernacular, is more than I’m prepared to write. But you get a theorem—technically, a different theorem for each formula ρ. (So it’s a theorem schema.) It has the form ∀p̄(A→B), where A is the above condition and B asserts the existence of g.
We don’t need to prove that the condition holds; rather, the theorem says that whenever it holds (perhaps only for some values of the parameters), then the conclusion holds. The proof does not require Choice: the ordinals are already well-ordered. As before, we also have a formula G(α,c̄,s); if the condition holds for some c, then G(α,c̄,s) assigns a unique s to every ordinal—a “function-like” thingy with “domain” Ω.
As a bonus, we can rehabilitate Cantor’s “proof” of the Well-Ordering Theorem. Let M be a set, and let c be a choice function for M. Our rule ρ says that the s assigned to α is c(M∖{f(β):β<α}), provided that the difference set is not empty. Otherwise we assign M to α. (We choose M simply because it is not an element of M.) We define G by transfinite recursion; informally, we can write Ĝ(α) for the value assigned to α. (I have left the parameters M and c̄ implicit.) If we never have Ĝ(α)=M, that means that G defines an injection of Ω into M, and inverting this gives us a map from M onto Ω. Replacement then says that Ω is a set. The Largest Ordinal paradox however proves this is not so. (The formal statement: ¬∃S ∀x(Ω(x)↔x∈S).) Therefore for some α, gα maps α+1 1–1 onto M, and we’ve well-ordered M.
I’ve made a full meal of this argument. Typically, one would condense this discussion into a couple of sentences: “Given a choice function c, use it to define (by transfinite recursion) an injective function from an initial segment of Ω into M. As this function cannot be defined for all ordinals, it must map the ordinals less than some α onto M, and so M is well-orderable.”
While this proof resembles Cantor’s demonstration, it borrows essential features from Zermelo’s. Gone are the successive choices with their psychological aspect, replaced with a choice function. And the “union of partial well-orderings” in Zermelo’s 1904 proof lies buried inside the transfinite recursion.