LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

Least witness ranks give choice-free bounds

Statement

For a fixed finite family of formulas and each ordinal $α$ , there is a definable ordinal $b (α) > α$ such that every true existential instance with parameters in $V_{α}$ has a witness of rank below $b (α)$ . More generally, for a definable increasing exhaustive hierarchy of sets $W_{γ}$ with union $W$ , the witnesses in $W$ can be bounded by a single stage $W_{b (α)}$ for parameters in $W_{α}$ .

Facts & Assumptions

[F1]

Minimum-rank selection and Collection: In ZF every nonempty definable class $C$ has a least member-rank $α$ , and ${x \in C : rank (x) = α}$ is a nonempty set. Replacement yields the Collection schema: if $\forall x \in a \exists y ϕ (x, y)$ , a set $b$ exists with $\forall x \in a \exists y \in b ϕ (x, y)$ . Conversely, Separation and Collection yield Replacement for functional formulas.

[F2]

Rank characterizes hierarchy membership: In ZF, for every set $x$ and ordinal $α$ ,

$x \in V_{α} ⟺ rank (x) < α, x \subseteq V_{α} ⟺ rank (x) \leq α .$

Thus $rank (x)$ is the least $α$ with $x \subseteq V_{α}$ , and $rank (x) = α$ iff $x \in V_{α + 1} ∖ V_{α}$ .

Proof

Given: A fixed finite list of existential formulas in ambient ZF and a specified ordinal $α$ .

1.1

For each existential matrix $ψ_{i} (y, \overset{ˉ}{x})$ define $r_{i} (\overset{ˉ}{x}) = 0$ when no witness exists, and otherwise let it be the least rank of a witness. F1 supplies that least ordinal and a witness at that rank. Because the list of formulas is fixed externally, this is a separate definable function for each $i$ , with no appeal to truth for arbitrary formulas.

F1given

2.1

The union of the finitely many sets of parameter tuples from $V_{α}$ is a set, including a singleton empty tuple for a sentence. Replacement collects all $r_{i} (\overset{ˉ}{a})$ in a set $R_{α}$ . Put $b (α) = \sup (R_{α} \cup {α}) + 1$ . Then $b (α) > α$ and every required least-rank witness has rank below $b (α)$ ; by F2 it lies in $V_{b (α)}$ . No particular witness has been selected as a function of the tuple.

F2step 1.1

3.1

For $W$ , replace least witness rank by the least stage containing a witness in $W$ whose matrix holds relativized to $W$ . Exhaustion gives such a stage; it has a least value by the well-order of ordinals. Replacement over tuples in $W_{α}$ and the same successor-supremum formula give $b (α)$ . By monotonicity, for every true instance at least one witness lies in $W_{b (α)}$ ; witnesses of larger rank need not lie there. With no existential formulas or no true instances, the same formula still gives a bound above $α$ .

step 1.1step 2.1given∎

Depends on

Used by

Montague–Lévy reflection for a finite formula family Theorem

Dependency tree · two levels

7 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

Geschke, Models of Set Theory — Theorem 4.3 proof pp10–11 (standard reference, not scraped)