TheoremStatement: 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.

Montague–Lévy reflection for a finite formula family

Statement

In ZF, for each fixed finite family $Φ$ and every ordinal $α$ , some $β > α$ makes $Φ$ absolute between $V_{β}$ and $V$ , for all tuples in $V_{β}$ . More generally the same holds between $W_{β}$ and $W$ for a definable increasing continuous hierarchy of sets exhausting a definable nonempty class $W$ . For an empty class, the relativization statement is interpreted as a scheme rather than satisfaction in an empty structure.

Facts & Assumptions

[F1]

Least witness ranks give choice-free bounds: 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_{α}$ .

[F2]

A finite witness criterion for reflection: Let $Φ$ be a finite family of membership formulas closed under subformulas, and let $\emptyset \neq C \subseteq D$ have actual restricted membership. All formulas of $Φ$ agree between $C, D$ iff whenever $\exists x ψ (x, \overset{ˉ}{a}) \in Φ$ is true in $D$ with $\overset{ˉ}{a} \in C$ , some $b \in C$ satisfies $ψ^{D} (b, \overset{ˉ}{a})$ . Definable-class versions are schemes.

[F3]

Transitivity and growth of hierarchy stages: In ZF without Foundation, every $V_{α}$ is transitive and $α \leq β$ implies $V_{α} \subseteq V_{β}$ . Also $V_{α} \cap Ord = α$ , and both $α$ and $V_{α}$ belong to $V_{α + 1} ∖ V_{α}$ .

[F4]

The cumulative hierarchy: In ZF without Foundation define the cumulative hierarchy by

$V_{0} = \emptyset, V_{α + 1} = P (V_{α}), V_{λ} = ⋃_{β < λ} V_{β} (λ a nonzero limit ordinal) .$

For each ordinal $θ$ , use the set well-order recursion schema on $θ + 1$ . On histories of domain $0$ return $\emptyset$ ; on domain $β + 1$ return the power set of the last value; on nonzero limit domains return the union of the range. Each is a unique set. Recursions on different ordinal intervals agree on overlaps by the uniqueness clause applied to the smaller interval. Hence the definition of $V_{α}$ as the value at $α$ is uniform and independent of the chosen interval. Power Set is used at successors and Replacement and Union at limits. The notation $⟨ V_{α} : α \in Ord ⟩$ denotes a definable class function, not a set sequence.

Conventions and prerequisites: thm-transfinite-recursion, lem-ordinal-basics, def-limit-ordinal.

Proof

Given: Ambient ZF, a fixed finite family, an ordinal bound, and the stated hierarchy hypotheses.

1.1

Expand abbreviations and close $Φ$ under subformulas; the resulting family is still finite. Take the definable witness bound $b$ from F1 for this family. Start $β_{0} > α$ , increasing it if necessary so that $W_{β_{0}}$ is nonempty in the general nonempty-class case. For $V$ , $β_{0} = α + 1$ suffices.

F1given

2.1

Define $β_{n + 1} = b (β_{n})$ and $β = \sup_{n \in ω} β_{n}$ . This definable class recursion yields a set sequence in ZF as follows: induction on $n$ gives a unique finite attempt of length $n + 1$ ; extending the attempt applies the definable function $b$ once. Uniqueness makes its endpoint a functional formula, so Replacement on $ω$ collects all endpoints. Union gives their supremum. Thus no fixed set containing all possible ordinals and no choice function is required. Strict increase implies $β > α$ and makes $β$ a nonzero limit ordinal.

F1step 1.1

3.1

Continuity and monotonicity give $W_{β} = ⋃_{n} W_{β_{n}}$ : any earlier index is below some $β_{n}$ . A finite tuple from this union is contained in one stage, by taking the maximum of finitely many indices; the empty tuple is in every stage. If an existential from the closed family is true in $W$ at that tuple, F1 gives a witness in $W_{β_{n + 1}} \subseteq W_{β}$ .

F1step 2.1

4.1

The finite witness criterion F2 therefore gives agreement for every member of the closed family, hence for $Φ$ . For $V$ , F3 supplies the increasing transitive hierarchy and its limit clause is F4; Foundation supplies exhaustion. Power Set constructs successor stages, Separation and Replacement construct the rank bounds, and Infinity, Replacement and Union supply step 2.1. For an empty $W$ every positive-arity tuple assertion is vacuous and closed-formula relativizations agree because both domains are empty. The entire construction is choice-free.

F2F3F4step 3.1∎

Depends on

Used by

Transitive models of fixed finite axiom fragments Corollary
Ordinal definability and HOD Definition
Reflecting a finite family with parameters Example
Finite reflection along constructible levels Lemma
Strong compactness and the product-measure extension interface Theorem

Dependency tree · two levels

16 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, complete proof pp10–11; Freiburg Theorem 3.5.10 pp53–54 (standard reference, not scraped)