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

Transitivity and growth of hierarchy stages

Statement

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_{α}$ .

Facts & Assumptions

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

[F1]

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. (The cumulative hierarchy)

[F2]

Let $(W, <)$ be a well-order (def-well-order) and let $S \subseteq W$ satisfy the following: for every $a \in W$ , if $W_{< a} \subseteq S$ then $a \in S$ (def-initial-segment). Then $S = W$ . In property form: if a property $P$ of elements of $W$ satisfies "whenever $P (x)$ holds for every $x < a$ , it holds at $a$ ", then $P (a)$ holds for every $a \in W$ . This is a theorem of ZF. No form of the Axiom of Choice is used. Choice is perfectly available at this point in the library, since Zorn's lemma is proved from it on the previous page; the claim made here is about this proof, which never invokes it. (Transfinite induction)

Proof

1.1

Induct on ordinal stages, applying set transfinite induction on each sufficiently long ordinal interval. The empty stage is transitive. If $T$ is transitive then $T \subseteq P (T)$ and $P (T)$ is transitive: $z \in y \subseteq T$ implies $z \in T$ and thus $z \subseteq T$ . A union of transitive sets is transitive. These observations establish transitivity and, simultaneously, nesting at successors and limits.

F1F2

2.1

A second induction gives $V_{α} \cap Ord = α$ . At zero both are empty. An ordinal $γ$ lies in $V_{β + 1}$ iff $γ \subseteq V_{β}$ , iff all its ordinal members belong to $β$ , iff $γ \leq β$ ; thus the intersection is $β + 1$ . At a nonzero limit the intersection is the union of the earlier ordinal intersections, namely the limit itself.

F1F2step 1.1

3.1

Consequently $α \subseteq V_{α}$ but $α \notin V_{α}$ , and hence $α \in V_{α + 1}$ . Also $V_{α} \subseteq V_{α}$ gives $V_{α} \in V_{α + 1}$ . To exclude $V_{α} \in V_{α}$ , observe that any $u \in V_{α}$ is a subset of some $V_{β}$ with $β < α$ : this holds at successors directly, at limits by passing to an earlier stage, and at zero vacuously. If $u = V_{α}$ , then $α \subseteq V_{α} \subseteq V_{β}$ , making $α \in V_{β + 1} \subseteq V_{α}$ , a contradiction.

F1step 1.1step 2.1∎

Depends on

Used by

A bounded hierarchy for the multiple-choice argument Lemma
Ranks of ordinals and hierarchy stages Proposition
Equivalent forms of Foundation Theorem
Rank characterizes hierarchy membership 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

Marks, Set Theory, Berkeley edition — 7.2 p.34. (standard reference, not scraped)