LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Transfinite recursion along the ordinals: a class rule determines exactly one operation defined at every ordinal

Statement

Let $G$ be a class function: a rule, given by a formula in the language of set theory, that assigns a set $G (h)$ to every function $h$ whose domain is an ordinal (Ordinal (von Neumann)). Then there is a class function $F$ , given by a formula and defined at every ordinal, such that

$F (β) = G (F ↾ β) for every ordinal β,$

and $F$ is the only one: any class function $F^{'}$ defined at every ordinal and satisfying $F^{'} (β) = G (F^{'} ↾ β)$ for every ordinal $β$ agrees with $F$ at every ordinal. Here $F ↾ β$ is the restriction of $F$ to the set $β$ of ordinals below $β$ , which is a set even though $F$ is not.

Like Transfinite recursion, this is a theorem schema of ZF: one theorem for each formula defining $G$ . It uses Replacement, inherited from that theorem, and it uses no form of the Axiom of Choice.

Why the published theorem does not already say this. Transfinite recursion is stated for a well-order $(W, <)$ , that is for a set, and it delivers one function whose domain is that set. An operation such as $α + β$ has to be defined at every ordinal $β$ , and the ordinals are not a set (Burali-Forti: there is no set of all ordinals), so no single instance of the published theorem defines it. What is proved below is exactly the bridge: the instances at the individual ordinals cohere, and the coherence is supplied by the published theorem's own uniqueness clause. No new recursion principle is introduced.

Facts & Assumptions

Given: A class function $G$ as in the statement, and the axioms of ZF. No choice principle is assumed. For an ordinal $γ$ we write $(γ, \in)$ for $γ$ carrying the membership relation.

[A1]

$G (h)$ is a well-determined set for every function $h$ whose domain is an ordinal, and the rule is given by a formula.

[L1]

Transfinite recursion on a set: for a well-order $(W, <)$ (Well-order and well-ordered set) and a class function $G$ defined on functions whose domains are proper initial segments of $W$ , there is exactly one function $F$ with domain $W$ such that $F (a) = G (F ↾ W_{< a})$ for every $a \in W$ (Transfinite recursion).

[L2]

An ordinal is a transitive set on which $\in$ is a strict well-order (Ordinal (von Neumann)).

[L3]

$W_{< a} = {x \in W : x < a}$ , and every proper initial segment of a well-order is $W_{< a}$ for exactly one $a$ (Initial segment of a well-order).

[L4]

Every element of an ordinal is an ordinal, $α^{+} = α \cup {α}$ is an ordinal, and $α \subseteq β$ if and only if $α \in β$ or $α = β$ (claims (a), (c), (f) of Basic closure properties of ordinals).

[L5]

Every nonempty set of ordinals has an $\in$ -least element (Trichotomy and well-ordering of the ordinals).

Proof

technique · direct

1.1

For every ordinal $γ$ the pair $(γ, \in)$ is a well-order, by clause 2 of the definition of an ordinal.

1.2

For $β \in γ$ the initial segment of $(γ, \in)$ determined by $β$ is $γ_{< β} = {x \in γ : x \in β} = β$ , because $β \subseteq γ$ by transitivity of $γ$ ; so by [L3] the proper initial segments of $(γ, \in)$ are exactly the ordinals $β \in γ$ , and a function whose domain is one of them is a function whose domain is an ordinal, to which $G$ applies.

L2L3A1

1.3

If $ξ \in β$ then $ξ^{+} \in β^{+}$ : transitivity of $β$ gives $ξ \subseteq β$ , and $ξ \in β$ gives ${ξ} \subseteq β$ , so $ξ^{+} \subseteq β$ , whence $ξ^{+} \in β$ or $ξ^{+} = β$ by [L4], and either way $ξ^{+} \in β \cup {β} = β^{+}$ .

L2L4

2.1

Applying [L1] to the well-order $(γ, \in)$ and to $G$ yields, for each ordinal $γ$ , exactly one function $F_{γ}$ with domain $γ$ satisfying $F_{γ} (β) = G (F_{γ} ↾ β)$ for every $β \in γ$ .

step 1.1step 1.2L1A1

3.1

Coherence: for $δ \in γ$ put $u = F_{γ} ↾ δ$ , a function with domain $δ$ ; for $β \in δ$ transitivity of $δ$ gives $β \subseteq δ$ , so $u ↾ β = F_{γ} ↾ β$ and $u (β) = F_{γ} (β) = G (F_{γ} ↾ β) = G (u ↾ β)$ , so $u$ satisfies the recursion on $δ$ and the uniqueness half of [L1] applied to $(δ, \in)$ gives $F_{γ} ↾ δ = F_{δ}$ .

step 2.1L1L2

3.2

Define $F (β) : = F_{β^{+}} (β)$ , which makes sense because $β^{+}$ is an ordinal by [L4] and $β \in β^{+}$ ; the defining condition is a formula in $β$ , so $F$ is a class function defined at every ordinal.

step 2.1L4construct

4.1

For every ordinal $β$ and every $ξ \in β$ we have $ξ^{+} \in β^{+}$ , hence $F_{β^{+}} ↾ ξ^{+} = F_{ξ^{+}}$ and therefore $F_{β^{+}} (ξ) = F_{ξ^{+}} (ξ) = F (ξ)$ ; so $F ↾ β = F_{β^{+}} ↾ β$ , which is a set because $F_{β^{+}}$ is.

step 1.3step 3.1step 3.2

5.1

Consequently $F (β) = F_{β^{+}} (β) = G (F_{β^{+}} ↾ β) = G (F ↾ β)$ for every ordinal $β$ , which is the required recursion equation.

step 4.1step 3.2

6.1

For uniqueness, let $F^{'}$ be a class function defined at every ordinal with $F^{'} (β) = G (F^{'} ↾ β)$ for every $β$ , and suppose $F (β_{0}) \neq F^{'} (β_{0})$ for some ordinal $β_{0}$ ; then $D = {ξ \in β_{0}^{+} : F (ξ) \neq F^{'} (ξ)}$ is a set by Separation, it is a set of ordinals by [L4], and it is nonempty because $β_{0} \in D$ , so it has an $\in$ -least element $μ$ by [L5].

step 5.1L4L5

7.1

Every $ξ \in μ$ lies in $β_{0}^{+}$ , because $μ \in β_{0}^{+}$ gives $μ \subseteq β_{0}^{+}$ , and $ξ \notin D$ by minimality of $μ$ , so $F (ξ) = F^{'} (ξ)$ ; hence $F ↾ μ = F^{'} ↾ μ$ and $F (μ) = G (F ↾ μ) = G (F^{'} ↾ μ) = F^{'} (μ)$ , contradicting $μ \in D$ .

step 6.1step 5.1L4

8.1

No such $β_{0}$ exists, so $F$ and $F^{'}$ agree at every ordinal, and $F$ is the unique class function on the ordinals satisfying $F (β) = G (F ↾ β)$ .

step 7.1step 6.1step 5.1∎

Remarks

What is spent. Replacement, through Transfinite recursion, and Separation, at step 6.1. No choice principle appears anywhere, for the same reason as in the published theorem: at every stage the object used is the unique function with a given domain, never one selected from many.

Three cases, not two. The lemma says nothing about how $G$ is given. In practice $G$ is defined by the three-way split of Successor and limit ordinals — a value at $0$ , a rule at a successor, a rule at a limit — and that split is exhaustive and exclusive for every ordinal. Writing "successor or limit" and forgetting $0$ is the standard way to define an operation that is undefined at $0$ .

Why the restriction is a set. Step 4.1 is not bookkeeping. $F$ is a proper class, so " $F ↾ β$ " needs an argument, and the argument is that it coincides with the restriction of the set function $F_{β^{+}}$ . Without it, $G (F ↾ β)$ would not even be an application of $G$ to a set.

The naming. Some texts state this as "transfinite recursion on the class of ordinals" and prove it directly by a least-counterexample argument. The route taken here spends nothing new: it reuses the published theorem at each ordinal and glues, and the glue is that theorem's uniqueness clause.

Depends on

Used by

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Transfinite induction (Wikipedia) (standard reference, not scraped)
Ordinal number (Wikipedia) (standard reference, not scraped)
T. Jech, Set Theory, 3rd millennium ed., Ch. 2 (Ordinal numbers) (standard reference, not scraped)
R. Moosa, Set Theory course notes (standard reference, not scraped)
Open Logic Project, Open Logic Text (standard reference, not scraped)