I'm trying to get my head around how to prove that the axiom of choice implies Zorn's lemma using transfinite recursion:
Transfinite recursion I Let $G$ be a class function. Then there is class function $F$ from the class of ordinals so that for any ordinal $\alpha$ we have $F(\alpha) = G(F\restriction_\alpha)$.
Transfinite recursion II Let $G_1,G_2$ and $G_3$ be class functions. Then there is a class function $F$ from the class of ordinals that that
$F(0) = G_1(0)$,
for any ordinal $\alpha$, $F(\alpha + 1) = G_2(F(\alpha)),$
for any limit ordinal $\lambda$, $F(\lambda) = G_3(F\restriction_\lambda).$
Before telling that this is a duplicate, hear me out. Most of the references on the matter I found on this site and on the internet at large contain only informal proofs or sketches. In particular, this answer by Asaf Karagila
https://math.stackexchange.com/a/97315/229776
advises to build a transfinite sequence of elements of a partially ordered set $(X,\leq)$ to find a maximal element with a choice function $f$ of $X$ by setting.
The book by Hrbacek and Jech ("Introduction to set theory") also uses Hartog's number $h(X)$ (the least ordinal not equipotent to any subset of $X$) to construct an $h(X)$-sequence.
The problem is that I simply can't see at the moment how we can formally use transfinite recursion theorems to construction a desired sequence. Any help would be appreciated.
Best Answer
We can avoid the appeal to Hartogs numbers if we do an indirect proof instead. As a bonus, the transfinite recursion becomes a bit cleaner:
Assume that (a) $(P,\preceq)$ is a partially ordered set that satisfies the premises of Zorn's lemma, (b) $P$ has no maximal element, and (c) $C$ is a choice function on $P$. We then seek a contradiction.
Without loss of generality extend $C$ such that $C(\varnothing)=42$, no matter whether or not $42\in P$.
Apply Transfinite Recursion I to the class function $$ G(X) = C(\{y\in P\mid \forall z\in \operatorname{Rng}(X)\cap P: z\prec y\}) $$ This gives a class function $F$ such that for every ordinal $\alpha$, $$ F(\alpha) = C(\{y\in P \mid \forall \beta<\alpha : F(\beta)\in P \to F(\beta)\prec y\}) $$
Lemma. For all $\alpha$ it holds that $F(\alpha)\in P$ and $\forall \beta : F(\beta)\prec F(\alpha)$.
Proof. By transfinite induction on $\alpha$. The induction hypothesis tells us that $\{F(\beta)\mid \beta<\alpha\}$ is a chain in $P$ (note that it is a set in any case thanks to Replacement). The Zorn premises tells us that this chain has an upper bound; because there is no maximal element it even has a strict upper bound. In other words, $$\{y\in P \mid \forall \beta<\alpha : F(\beta)\in P \to F(\beta)\prec y\},$$ the set of all the strict upper bounds, is not empty, so $F(\alpha)$ is in $P$ and is greater than all the $F(\beta)$s.
The lemma tells us that $F$ is an order-preserving function from ON to $P$. Since $F$ preserves order, it is in particular injective. Therefore the formula $$ H(x)=\alpha \iff F(\alpha)=x \lor (\alpha=117 \land \forall\beta:F(\beta)\ne x) $$ is functional, and applying Replacement on $P$ and $H$ tells us that ON is a set. The Burali-Forti paradox now furnishes our desired contradiction.
Note that we never actually needed $C(\varnothing)=42$ except to make sure that $G$ was a class function so we could use the recursion theorem on it.
The proof structure here is typical: The definition by transfinite recursion is followed immediately by a transfinite induction that extracts useful facts from the recursion formula. This two-step approach is often necessary for using the general recursion machinery because we need to define $G$ in a defensive way such that we can prove that it is makes sense and is functional without depending on its argument being produced by recursion. This defensive scaffolding -- i.e., intersecting $\operatorname{Rng}(X)$ with $P$ so $z\prec y$ makes sense, and making sure that $C(\{x\in P\mid \cdots\})$ always means something even if the condition ends up filtering everything away -- is then cleaned away by the lemma once the recursive magic has done its job and we know the input to $G$ comes from a well-behaved recursion.
As an additional note, one might argue that this is not "morally" an indirect proof. The way I prefer to think about it is that I would like to assume just (a) and (c), and then in the middle of the proof of the lemma say
Claiming that "we're done" with the entire Zorn's Lemma when we were in the middle of an inner induction step is not really done in polite company, though. Phrasing the entire proof as an indirect proof will allow us to follow this intuition anyway, in simple yet formally acceptable way.
The part of the proof after the lemma is then just an argument that eventually we must hit one of the "we're done" conditions, because continuing forever would have absurd consequences.