careful exposition of transfinite recursion

Question

Given a well ordered set W and a family of sets X(w) indexed by the elements w of W, transfinite recursion allows one often to define a function f on W that takes values f(w) in X(w). (I distinguish this from transfinite induction, which establishes a family of propositions.) The recursive definition involves providing a formula for f(w) in terms of the values of f at elements of W smaller than w, but there may also be an auxiliary condition on the family of previous values. For example, in the proof of Zorn's lemma by transfinite recursion from the well ordering theorem of Zermelo, one needs to know that the previous values form a chain: the next value is then a strict upper bound for that chain.

Is there a good reference in the published literature that gives a careful abstract criterion for specifying what sort of auxiliary conditions "work", together with a proof?

(I'm not asking for an exposition here, just for references to the literature. The reason I ask is that I'm in the process of formalizing the method of transfinite recursion, and I wonder whether I'm following the best approach, whether this has been done before, and whether a careful expository paper would be worth disseminating.)

Answer 1

These auxiliary conditions are never crucial to the argument: we can always define our recursive procedure to "trivialize" if they fail, and then separately prove that they don't.

Let's look at the Zorn example you give. At an abstract level, what we have is:

• A well-ordering $(W, \prec)$, and

• A map $F$ from chains in $P$ to chains in $P$ (where $P$ is the poset we're looking at).

We want to define $I(w)$ for all $w\in W$, where $I$ is the "iterate"of $F$, but on the face of it we need to know that we never "stop being a chain" - that is, $I(w)$ needs to be a chain for us to define $I(w+1)=F(I(w))$.

We get around this by working with a modified version of $F$: for a subset $A$ of $P$, $G(A)$ is defined as follows:

• If $A$ is a chain, then $G(A)=F(A)$.

• Otherwise, $G(A)=A$.

Then we can use transfinite recursion as usual to define an iterate $J$ of $G$, without a problem. We then prove by transfinite induction that $J(w)$ is a chain for each $w$, so in fact $J$ is an iterate of $F$ as hoped.

So there's no real need to use these "auxiliary conditions."