TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Recursion on well-founded setlike relations

Statement

In ZF without Foundation, let $R$ be a well-founded setlike relation on a definable class $X$ . For any definable rule assigning a unique set $G (x, h)$ to every $x \in X$ and every set function $h$ on ${pred}_{R} (x)$ , there is a unique definable function $F$ on $X$ satisfying

$F (x) = G (x, F ↾ {pred}_{R} (x)) .$

Every restriction of $F$ to a set subset of $X$ is a set function. Parameters in $R, X, G$ are allowed; the assertion is a schema, not quantification over class objects.

Facts & Assumptions

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

[F1]

Let $R$ be well-founded and setlike on $X$ , and let a definable rule $G (x, h)$ assign a unique set whenever $x \in X$ and $h$ is a set function on ${pred}_{R} (x)$ . An attempt is a set function $f$ on a predecessor-closed set $D \subseteq X$ satisfying $f (z) = G (z, f ↾ {pred}_{R} (z))$ for every $z \in D$ . Any two attempts agree on the intersection of their domains. If for every $y R x$ an attempt exists on the canonical cone $C (y)$ , there is a unique attempt on $C (x)$ . (Compatible recursion attempts)

Proof

1.1

Use well-founded induction to prove existence of an attempt on each canonical cone $C (x)$ . If attempts exist for all predecessors, the assembly assertion gives the attempt on $C (x)$ , including the empty-predecessor case. Thus the property is progressive.

2.1

Define $F (x) = u$ if some set-domain attempt contains $(x, u)$ . Existence follows from step 1.1 and uniqueness from compatibility of attempts. For each set $A \subseteq X$ , Replacement applied to this functional definition makes $F ↾ A$ a set. A cone attempt agrees with $F$ at $x$ and all its predecessors, proving the recursion equation.

F1step 1.1

3.1

Any rival definable function obeying the equation agrees with $F$ at a point whenever it agrees at all predecessors. Well-founded induction proves equality everywhere. Every definition just used quantifies over set attempts, so it is a first-order definition with the original parameters.

F1step 2.1∎

Depends on

Compatible recursion attempts

Used by

Extensional relations and collapse maps Definition
Ordinal rank of a well-founded relation Definition

Dependency tree · two levels

3 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

Marks, Set Theory, Berkeley edition — Theorem 6.6 p.31. (standard reference, not scraped)