ExampleConstruction: AI-adaptedVerification: 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.

Reflecting a finite family with parameters

Example

For fixed formulas $ϕ (x), ψ (x, y)$ and a set $a$ , there is $β$ with $a \in V_{β}$ such that both formulas are absolute on every tuple from $V_{β}$ . For instance take $a = {\emptyset}$ , $ϕ (x) \equiv \exists z (x \in z)$ and $ψ (x, y) \equiv \exists z (x \in z \land y \in z)$ .

Facts & Assumptions

[F1]

Montague–Lévy reflection for a finite formula family: 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.

[F2]

Transitive models of fixed finite axiom fragments: For each fixed external finite $Γ \subseteq Z F$ , ZF proves that some transitive $V_{β}$ satisfies $Γ$ , with $β$ above any prescribed ordinal bound. In ZFC the analogous scheme holds for fixed finite $Γ \subseteq Z F C$ . These are schemes indexed by external fragments, not a single internal assertion of models for all coded fragments.

Verification

Given: A fixed pair of formulas and a set parameter; the displayed instance uses von Neumann ranks.

1.1

In the instance, $rank (a) = 1$ and the witnesses for $ϕ (a)$ and $ψ (a, a)$ can both be ${a}$ . It has rank $2$ , so it lies in $V_{3}$ , while $a \in V_{2}$ . Thus the witness may require a later stage than the parameter.

givenalgebra

2.1

For the general pair, close both formulas under subformulas and apply F1 starting above $rank (a) + 1$ . The produced $β$ contains $a$ and reflects every formula of this finite closure. In particular it reflects the two original formulas at all tuples in $V_{β}$ , not merely at the named instance. Applying F2 is an additional option when the displayed formulas include a fixed axiom fragment.

F1F2step 1.1

3.1

Choosing only witnesses for the two formulas at $a$ would not cover their subformula instances at the new witnesses and at all other parameters in $V_{β}$ . The construction in F1 bounds every existential subformula at every tuple from each stage and iterates those bounds. That is why its conclusion supplies the required all-tuple agreement.

F1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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 pp10–11 (standard reference, not scraped)