Alphabeta Math
Pipeline-generated
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.

Well-Founded Relations, Rank, and the Cumulative Hierarchy

1 · Prerequisites

2 · Summary

The development starts with supplied well-founded setlike relations, builds predecessor cones and compatible recursion attempts, and derives rank and Mostowski collapse. These constructions do not need ambient Foundation. Hierarchy stages use Power Set at successors and Replacement and Union at limits; Foundation enters when membership on all sets is declared well-founded. Its equivalence with hierarchy exhaustion is proved using stage heights.

Transitive closure means the least transitive superset. Hereditary size uses injections of the root-inclusive closure into an ordinal below the given infinite initial ordinal. This makes the sethood and transitivity of H_kappa choice-free. Choice appears only where stated: a supplied choice function in the descending-sequence converse, and AC in hereditary-size exhaustion. Universe closure is defined without claiming large-cardinal existence. Class notation is always eliminable first-order shorthand.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Well-founded and setlike relations

Definition

Let X be a definable class and R a definable binary relation on X, with fixed set parameters. Write pred⁡R(x)={y∈X:yRx}. The relation is setlike if this predecessor collection is a set for every x∈X. It is well-founded if every nonempty set A⊆X has an R-minimal member x, meaning pred⁡R(x)∩A=∅.

These are schemes in first-order set theory: a class is notation for a defining formula. No transitivity or totality of R is required. Every relation on a set is setlike. An ordinal carries a well-founded membership relation by its definition; ambient Foundation does not make every arbitrary relation well-founded. All results concerning a supplied well-founded setlike relation are valid in ZF without Foundation unless stated otherwise.

Conventions and prerequisites: Ordinal (von Neumann).

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Accessible pointed membership graphs

Definition

An accessible pointed graph consists of a set X of nodes, a root r∈X, and a relation R⊆X2. Draw an arrow x→y precisely when yRx. Accessibility means that for every x∈X there are n∈ω and a function p:n+1→X with p(0)=r, p(n)=x, and p(i+1)Rp(i) for i<n. The path of length zero reaches the root.

A decoration is a set function d on X such that d(x)={d(y):yRx} for each node. A well-founded graph means that R has the minimal-element property, not an unqualified no-infinite-path characterization. Extensionality is not part of the graph definition. No axiom of anti-foundation is assumed.

Conventions and prerequisites: Well-founded and setlike relations.

LemmaStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Finite predecessor closures are sets

Statement

For every setlike relation R on a definable class X and x∈X, there is a least predecessor-closed set C(x)⊆X containing x. It consists exactly of nodes reachable from x by a finite sequence of predecessor steps. Well-foundedness is not needed.

Facts & Assumptions

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

[F1]

Let X be a definable class and R a definable binary relation on X, with fixed set parameters. Write pred⁡R(x)={y∈X:yRx}. The relation is setlike if this predecessor collection is a set for every x∈X. It is well-founded if every nonempty set A⊆X has an R-minimal member x, meaning pred⁡R(x)∩A=∅. These are schemes in first-order set theory: a class is notation for a defining formula. No transitivity or totality of R is required. Every relation on a set is setlike. An ordinal carries a well-founded membership relation by its definition; ambient Foundation does not make every arbitrary relation well-founded. All results concerning a supplied well-founded setlike relation are valid in ZF without Foundation unless stated otherwise. Conventions and prerequisites: def-ordinal. (Well-founded and setlike relations)

[F2]

Let (W,<) be a well-order (def-well-order) and let G be a class function: a rule, given by a formula in the language of set theory, that assigns a set G(h) to every function h whose domain is a proper initial segment of W (def-initial-segment). Then there is exactly one function F with domain W such that F(a)=G(F↾W<a)for every a∈W. Here F↾W<a is the restriction of F to the initial segment determined by a, so the value of F at a is prescribed in terms of all its earlier values at once. Because G is a class function rather than a set, this is a theorem schema of ZF: one theorem for each formula defining G. It uses Replacement, and it uses no form of the Axiom of Choice. (Transfinite recursion)

Proof

1.1F1F2

Put C0={x} and Cn+1=Cn∪⋃{pred⁡R(y):y∈Cn}. At each step Replacement collects the predecessor sets and Union forms the next set. Apply the set well-order recursion schema on ω, whose rule reads the last value at successors and gives {x} at zero; totalize on malformed histories by returning ∅. This produces a set sequence.

2.1step 1.1

Let C(x)=⋃n∈ωCn, a set by Replacement and Union. It contains x and is predecessor-closed: if y∈Cn and zRy, then z∈Cn+1. Conversely any predecessor-closed set containing x contains every Cn by natural induction, hence contains C(x).

3.1step 1.1step 2.1∎

Induction on n says Cn consists exactly of the nodes reached in at most n steps: the successor construction either keeps a node or appends one predecessor edge. Taking the union proves the finite-path description.

TheoremStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Induction on well-founded setlike relations

Statement

Let R be well-founded and setlike on a definable class X. If a definable property P is progressive, meaning that for every x∈X, [∀yRx P(y)]⇒P(x), then P(x) holds for all x∈X. Set parameters in P are allowed. This holds without Foundation.

Facts & Assumptions

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

[F1]

For every setlike relation R on a definable class X and x∈X, there is a least predecessor-closed set C(x)⊆X containing x. It consists exactly of nodes reachable from x by a finite sequence of predecessor steps. Well-foundedness is not needed. (Finite predecessor closures are sets)

Proof

1.1F1given

If there is a counterexample x, take its predecessor-closed set C(x) and separate the nonempty set B={y∈C(x):¬P(y)}. Well-foundedness gives a minimal b∈B.

2.1step 1.1given∎

Every predecessor of b belongs to C(x), and none belongs to B by minimality. Hence all satisfy P. Progressiveness gives P(b), contrary to b∈B. Therefore no counterexample exists.

LemmaStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Compatible recursion attempts

Statement

Let R be well-founded and setlike on X, and let a definable rule G(x,h) assign a unique set whenever x∈X and h is a set function on pred⁡R(x). An attempt is a set function f on a predecessor-closed set D⊆X satisfying f(z)=G(z,f↾pred⁡R(z)) for every z∈D.

Any two attempts agree on the intersection of their domains. If for every yRx an attempt exists on the canonical cone C(y), there is a unique attempt on C(x).

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 a definable class X. If a definable property P is progressive, meaning that for every x∈X, [∀yRx P(y)]⇒P(x), then P(x) holds for all x∈X. Set parameters in P are allowed. This holds without Foundation. (Induction on well-founded setlike relations)

[F2]

For every setlike relation R on a definable class X and x∈X, there is a least predecessor-closed set C(x)⊆X containing x. It consists exactly of nodes reachable from x by a finite sequence of predecessor steps. Well-foundedness is not needed. (Finite predecessor closures are sets)

Proof

1.1F1

The intersection of two attempt domains is predecessor-closed. At a point of the intersection, agreement at all predecessors makes their restricted functions equal; functionality of G then makes their values equal. Well-founded induction on this intersection proves agreement throughout.

2.1F2step 1.1

For each yRx, the attempt on C(y) is unique by step 1.1. Since the predecessor set is a set, Replacement collects these uniquely specified attempts. Their union h is a function on D=⋃yRxC(y) by agreement on overlaps. Its domain is predecessor-closed and it satisfies the attempt equation, because each point and all its predecessors lie in a constituent cone.

3.1F2step 1.1step 2.1given∎

There is no finite R-cycle: the finitely many nodes of such a cycle would form a nonempty set with no minimal member. Thus x∉D. The finite-path description gives C(x)=D∪{x}. Extend h by the single pair (x,G(x,h↾pred⁡R(x))). The extension obeys the rule at x, and it does not alter any predecessor restriction of a point in D. It is an attempt on C(x), unique by step 1.1. If the predecessor set is empty, the same construction starts with h=∅.

TheoremStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

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∈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∈X and h is a set function on pred⁡R(x). An attempt is a set function f on a predecessor-closed set D⊆X satisfying f(z)=G(z,f↾pred⁡R(z)) for every z∈D. Any two attempts agree on the intersection of their domains. If for every yRx an attempt exists on the canonical cone C(y), there is a unique attempt on C(x). (Compatible recursion attempts)

Proof

1.1F1

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.1F1step 1.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⊆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.

3.1F1step 2.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.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Transitive closure of a set

Definition

For a set a, form a0=a and an+1=an∪⋃an by recursion on ω. Set

TC⁡(a)=⋃n∈ωan.

This is a set by the same recursion, Replacement and Union construction as finite predecessor closure, now starting from a rather than a singleton and using membership as the setlike relation. The convention is the least transitive superset of a; to include a itself as an element, use TC⁡({a}). This construction does not assume Foundation.

Conventions and prerequisites: Finite predecessor closures are sets.

PropositionStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Minimality and closure laws of TC

Statement

For every set a, TC⁡(a) is transitive, contains a as a subset, and is contained in every transitive set T with a⊆T. Moreover a⊆b implies TC⁡(a)⊆TC⁡(b), and TC⁡(TC⁡(a))=TC⁡(a). In particular a∈TC⁡({a}).

Facts & Assumptions

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

[F1]

For a set a, form a0=a and an+1=an∪⋃an by recursion on ω. Set TC⁡(a)=⋃n∈ωan. This is a set by the same recursion, Replacement and Union construction as finite predecessor closure, now starting from a rather than a singleton and using membership as the setlike relation. The convention is the least transitive superset of a; to include a itself as an element, use TC⁡({a}). This construction does not assume Foundation. Conventions and prerequisites: lem-finite-predecessor-closure-is-a-set. (Transitive closure of a set)

Proof

1.1F1

The stage zero inclusion gives a⊆TC⁡(a). If z∈y∈TC⁡(a), choose n with y∈an; then z∈⋃an⊆an+1. Thus the union is transitive. Equivalently, transitivity of a set T is the elementary condition ⋃T⊆T.

2.1F1step 1.1

If a⊆T and T is transitive, induction gives an⊆T: the successor follows from ⋃an⊆⋃T⊆T. Union over n proves minimality.

3.1step 1.1step 2.1∎

For a⊆b, the transitive set TC⁡(b) contains a, so minimality proves monotonicity. Applying minimality with T=TC⁡(a) gives one idempotence inclusion and step 1.1 gives the other. Finally a∈{a}⊆TC⁡({a}).

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Ordinal rank of a well-founded relation

Definition

For a well-founded setlike relation R on X, its ordinal rank is the definable function determined by

ρR(x)=sup⁡{ρR(y)+1:yRx}=⋃{ρR(y)∪{ρR(y)}:yRx}.

To justify the definition, apply well-founded recursion to the total rule which returns this union if every value of its input function is an ordinal and returns 0 otherwise. Well-founded induction shows that every actual value is an ordinal: predecessor values are ordinals by the induction hypothesis, their successors are ordinals, Replacement collects them, and their union is an ordinal, including the empty union 0. Thus the default case never occurs. For yRx the rank equation gives ρR(y)<ρR(x). The definition requires no ambient Foundation for a supplied well-founded R.

Conventions and prerequisites: Recursion on well-founded setlike relations, Basic closure properties of ordinals.

PropositionStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Ordinal rankings characterize well-foundedness

Statement

A definable setlike relation R on X is well-founded if and only if there is a definable ordinal-valued function r on X with yRx⇒r(y)<r(x). For well-founded R, its rank ρR is pointwise least among such functions. No choice or Foundation is needed.

Facts & Assumptions

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

[F1]

For a well-founded setlike relation R on X, its ordinal rank is the definable function determined by ρR(x)=sup⁡{ρR(y)+1:yRx}=⋃{ρR(y)∪{ρR(y)}:yRx}. To justify the definition, apply well-founded recursion to the total rule which returns this union if every value of its input function is an ordinal and returns 0 otherwise. Well-founded induction shows that every actual value is an ordinal: predecessor values are ordinals by the induction hypothesis, their successors are ordinals, Replacement collects them, and their union is an ordinal, including the empty union 0. Thus the default case never occurs. For yRx the rank equation gives ρR(y)<ρR(x). The definition requires no ambient Foundation for a supplied well-founded R. Conventions and prerequisites: thm-recursion-on-well-founded-setlike-relations, lem-ordinal-basics. (Ordinal rank of a well-founded relation)

Proof

1.1F1

For well-founded R, its recursively defined ordinal rank exists and strictly increases along each predecessor edge, providing a ranking.

1.2given

Conversely, for a nonempty set A⊆X, Replacement makes r[A] a nonempty set of ordinals. It has a least element: choose one value α and minimize within the set of values at most α, using the well-order of α+1. A preimage a∈A of that least value has no predecessor in A, since a predecessor would have smaller rank.

2.1F1step 1.2∎

Finally well-founded induction gives ρR(x)≤r(x). If it holds at all yRx, then ρR(y)+1≤r(y)+1≤r(x) for all such y, and taking the ordinal supremum gives the desired bound at x. The empty supremum is zero.

PropositionStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Descending sequences and the choice hypothesis

Statement

A well-founded relation R on a definable class X admits no sequence f:ω→X with f(n+1)Rf(n) for every n. Conversely, if X is a set supplied with a choice function c on all its nonempty subsets, absence of such a sequence implies well-foundedness. The converse is asserted with this extra hypothesis, not in bare ZF.

Facts & Assumptions

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

[F1]

Let (W,<) be a well-order (def-well-order) and let G be a class function: a rule, given by a formula in the language of set theory, that assigns a set G(h) to every function h whose domain is a proper initial segment of W (def-initial-segment). Then there is exactly one function F with domain W such that F(a)=G(F↾W<a)for every a∈W. Here F↾W<a is the restriction of F to the initial segment determined by a, so the value of F at a is prescribed in terms of all its earlier values at once. Because G is a class function rather than a set, this is a theorem schema of ZF: one theorem for each formula defining G. It uses Replacement, and it uses no form of the Axiom of Choice. (Transfinite recursion)

Proof

1.1given

The range of any descending sequence is a nonempty set. A minimal element of that range, say f(n), still has predecessor f(n+1) in the range, a contradiction. This uses exactly the minimal-element definition of well-foundedness.

1.2F1given

For the converse, if a nonempty A⊆X has no minimal member, every A∩pred⁡R(a) for a∈A is nonempty. Begin with f(0)=c(A) and recurse by f(n+1)=c(A∩pred⁡R(f(n))). The supplied choice function makes this a uniquely specified recursion on the set well-order ω; malformed histories can be assigned c(A).

2.1step 1.2∎

Induction keeps every value in A and ensures f(n+1)Rf(n) at each step, contradicting the assumed absence. Thus every nonempty subset has a minimal element. For X=∅ well-foundedness is vacuous and there is no sequence into X.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

The cumulative hierarchy

Definition

In ZF without Foundation define the cumulative hierarchy by

V0=∅,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 ∅; 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α:α∈Ord⁡⟩ denotes a definable class function, not a set sequence.

Conventions and prerequisites: Transfinite recursion, Basic closure properties of ordinals, Successor and limit ordinals.

PropositionStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Transitivity and growth of hierarchy stages

Statement

In ZF without Foundation, every Vα is transitive and α≤β implies Vα⊆Vβ. Also Vα∩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 V0=∅,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 ∅; 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α:α∈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⊆W satisfy the following: for every a∈W, if W<a⊆S then a∈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∈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.1F1F2

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⊆P(T) and P(T) is transitive: z∈y⊆T implies z∈T and thus z⊆T. A union of transitive sets is transitive. These observations establish transitivity and, simultaneously, nesting at successors and limits.

2.1F1F2step 1.1

A second induction gives Vα∩Ord⁡=α. At zero both are empty. An ordinal γ lies in Vβ+1 iff γ⊆Vβ, iff all its ordinal members belong to β, iff γ≤β; thus the intersection is β+1. At a nonzero limit the intersection is the union of the earlier ordinal intersections, namely the limit itself.

3.1F1step 1.1step 2.1∎

Consequently α⊆Vα but α∉Vα, and hence α∈Vα+1. Also Vα⊆Vα gives Vα∈Vα+1. To exclude Vα∈Vα, observe that any u∈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 α⊆Vα⊆Vβ, making α∈Vβ+1⊆Vα, a contradiction.

TheoremStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Equivalent forms of Foundation

Statement

Over ZF without Foundation the following are equivalent: (i) every nonempty set a has a member disjoint from a (Foundation); (ii) the membership induction schema, that every definable progressive property holds of every set; (iii) every set belongs to some cumulative-hierarchy stage. All schemas allow set parameters.

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, every Vα is transitive and α≤β implies Vα⊆Vβ. Also Vα∩Ord⁡=α, and both α and Vα belong to Vα+1∖Vα. (Transitivity and growth of hierarchy stages)

[F2]

For every set a, TC⁡(a) is transitive, contains a as a subset, and is contained in every transitive set T with a⊆T. Moreover a⊆b implies TC⁡(a)⊆TC⁡(b), and TC⁡(TC⁡(a))=TC⁡(a). In particular a∈TC⁡({a}). (Minimality and closure laws of TC)

[F3]

Let R be well-founded and setlike on a definable class X. If a definable property P is progressive, meaning that for every x∈X, [∀yRx P(y)]⇒P(x), then P(x) holds for all x∈X. Set parameters in P are allowed. This holds without Foundation. (Induction on well-founded setlike relations)

Proof

1.1F2F3

Assume Foundation. Membership on the universe is setlike and has the minimal-element property, so well-founded induction proves (ii). Equivalently the counterexamples inside the transitive set TC⁡({x}) have a minimal member, contradicting progressiveness.

1.2given

Assume (ii). If a nonempty set a had no member disjoint from a, the property P(x) meaning x∉a would be progressive: if all y∈x were outside a and x∈a, the no-minimal-member assumption would supply y∈x∩a, a contradiction. Membership induction gives x∉a for all x, impossible since a is nonempty.

1.3F1

Under (ii), prove (iii) by membership induction. If each y∈x lies in a stage, it has a unique least stage index h(y), found by minimizing below any witness. Replacement collects these indices; let β=sup⁡{h(y):y∈x}. Nesting puts every y∈x in Vβ, so x∈Vβ+1. For x=∅ the supremum is zero and the same conclusion holds.

2.1F1∎

Assume (iii) and let a be nonempty. The least stage index h(x) exists for each x∈a; it is a successor β+1, since zero is empty and a limit is a union. If y∈x, then x∈Vβ+1 implies y∈Vβ, hence h(y)≤β<h(x). Minimize h on the set a using Replacement. A member x of least height has x∩a=∅, proving Foundation. These heights were defined from stages alone, without membership rank.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Membership rank under Foundation

Definition

Now assume ZF, including Foundation. Membership on the universe is well-founded and setlike, so its ordinal rank is defined for every set. Write

rank⁡(x)=sup⁡{rank⁡(y)+1:y∈x}.

The empty supremum is 0, so rank⁡(∅)=0. If y∈x, then rank⁡(y)<rank⁡(x). This is the Foundation-dependent special case of relation rank. The earlier construction of Vα did not require Foundation.

Conventions and prerequisites: Ordinal rank of a well-founded relation, Equivalent forms of Foundation.

TheoremStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Rank characterizes hierarchy membership

Statement

In ZF, for every set x and ordinal α,

x∈Vα  ⟺  rank⁡(x)<α,x⊆Vα  ⟺  rank⁡(x)≤α.

Thus rank⁡(x) is the least α with x⊆Vα, and rank⁡(x)=α iff x∈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]

Now assume ZF, including Foundation. Membership on the universe is well-founded and setlike, so its ordinal rank is defined for every set. Write rank⁡(x)=sup⁡{rank⁡(y)+1:y∈x}. The empty supremum is 0, so rank⁡(∅)=0. If y∈x, then rank⁡(y)<rank⁡(x). This is the Foundation-dependent special case of relation rank. The earlier construction of Vα did not require Foundation. Conventions and prerequisites: def-rank-of-a-well-founded-relation, thm-foundation-equivalent-to-hierarchy-exhaustion. (Membership rank under Foundation)

[F2]

In ZF without Foundation, every Vα is transitive and α≤β implies Vα⊆Vβ. Also Vα∩Ord⁡=α, and both α and Vα belong to Vα+1∖Vα. (Transitivity and growth of hierarchy stages)

Proof

1.1F1F2

Induct on α for the membership equivalence, for all sets x at once. At zero neither membership in the empty stage nor rank below zero holds. At a successor β+1, x∈Vβ+1 iff every y∈x lies in Vβ, iff every rank⁡(y)<β, iff sup⁡y∈x(rank⁡(y)+1)≤β, iff rank⁡(x)<β+1. All equivalences include the empty supremum case.

2.1F1F2step 1.1

At a nonzero limit λ, membership means membership in some Vβ with β<λ. By induction this implies rank below λ. Conversely if ρ=rank⁡(x)<λ, then ρ+1<λ and induction puts x in Vρ+1, hence in Vλ.

3.1F1step 1.1step 2.1∎

Now x⊆Vα iff each y∈x has rank below α, iff the supremum of their successor ranks is at most α. This proves the subset equivalence. Taking α=rank⁡(x) gives the least-stage assertion; applying membership at α+1 and at α gives the successor-shell assertion.

CorollaryStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

The universe is the class union of its stages

Statement

In ZF every set x belongs to Vrank⁡(x)+1. Consequently V=⋃α∈Ord⁡Vα in the class sense: every set lies in a stage. This is not a union indexed by a set of all ordinals.

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, for every set x and ordinal α, x∈Vα  ⟺  rank⁡(x)<α,x⊆Vα  ⟺  rank⁡(x)≤α. Thus rank⁡(x) is the least α with x⊆Vα, and rank⁡(x)=α iff x∈Vα+1∖Vα. (Rank characterizes hierarchy membership)

Proof

1.1F1

For ρ=rank⁡(x), the ordinal inequality ρ<ρ+1 and the membership characterization give x∈Vρ+1.

2.1step 1.1∎

Every member of a stage is a set, and step 1.1 gives a stage containing every set. Thus the two class descriptions agree. Neither statement asserts that their collection is a set.

PropositionStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Ranks of ordinals and hierarchy stages

Statement

In ZF, for every ordinal α, rank⁡(α)=α and rank⁡(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, for every set x and ordinal α, x∈Vα  ⟺  rank⁡(x)<α,x⊆Vα  ⟺  rank⁡(x)≤α. Thus rank⁡(x) is the least α with x⊆Vα, and rank⁡(x)=α iff x∈Vα+1∖Vα. (Rank characterizes hierarchy membership)

[F2]

In ZF without Foundation, every Vα is transitive and α≤β implies Vα⊆Vβ. Also Vα∩Ord⁡=α, and both α and Vα belong to Vα+1∖Vα. (Transitivity and growth of hierarchy stages)

Proof

1.1F1F2

By F2, α∈Vα+1∖Vα. The final equivalence in F1 therefore gives rank⁡(α)=α, including α=0.

2.1F1F2∎

By F2, Vα∈Vα+1∖Vα. Applying the same equivalence in F1 gives rank⁡(Vα)=α, including V0=∅.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Extensional relations and collapse maps

Definition

A setlike relation R on X is extensional when pred⁡R(x)=pred⁡R(y) implies x=y for x,y∈X. If R is also well-founded, its collapse map is the unique definable function

π(x)={π(y):yRx}.

Existence and uniqueness follow from well-founded recursion with G(x,h)=ran⁡(h), a set by Replacement. A collapse map is defined even without extensionality; injectivity is a further conclusion requiring extensionality. The construction for a supplied well-founded relation uses no ambient Foundation.

Conventions and prerequisites: Recursion on well-founded setlike relations.

LemmaStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

An extensional collapse is injective

Statement

For a well-founded setlike extensional relation R on a definable class X, its collapse map π is injective.

Facts & Assumptions

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

[F1]

A setlike relation R on X is extensional when pred⁡R(x)=pred⁡R(y) implies x=y for x,y∈X. If R is also well-founded, its collapse map is the unique definable function π(x)={π(y):yRx}. Existence and uniqueness follow from well-founded recursion with G(x,h)=ran⁡(h), a set by Replacement. A collapse map is defined even without extensionality; injectivity is a further conclusion requiring extensionality. The construction for a supplied well-founded relation uses no ambient Foundation. Conventions and prerequisites: thm-recursion-on-well-founded-setlike-relations. (Extensional relations and collapse maps)

[F2]

For a well-founded setlike relation R on X, its ordinal rank is the definable function determined by ρR(x)=sup⁡{ρR(y)+1:yRx}=⋃{ρR(y)∪{ρR(y)}:yRx}. To justify the definition, apply well-founded recursion to the total rule which returns this union if every value of its input function is an ordinal and returns 0 otherwise. Well-founded induction shows that every actual value is an ordinal: predecessor values are ordinals by the induction hypothesis, their successors are ordinals, Replacement collects them, and their union is an ordinal, including the empty union 0. Thus the default case never occurs. For yRx the rank equation gives ρR(y)<ρR(x). The definition requires no ambient Foundation for a supplied well-founded R. Conventions and prerequisites: thm-recursion-on-well-founded-setlike-relations, lem-ordinal-basics. (Ordinal rank of a well-founded relation)

Proof

1.1F1F2

Prove by transfinite induction on α that any x,y with max⁡(ρR(x),ρR(y))=α and π(x)=π(y) are equal. For any uRx, the collapse equation supplies vRy with π(u)=π(v). Both predecessor ranks are smaller than their respective parent ranks, so their maximum is strictly below α. The induction hypothesis gives u=v.

2.1F1F2step 1.1∎

It follows that every predecessor of x is a predecessor of y. Interchanging x,y proves the reverse inclusion; extensionality gives x=y. At rank zero both predecessor sets are empty and the same extensionality step applies without invoking an induction hypothesis. Every pair of ranks has an ordinal maximum, so the induction covers all pairs.

TheoremStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Mostowski collapse for extensional relations

Statement

Every well-founded setlike extensional relation R on a definable class X is isomorphic to membership on a unique transitive definable class Y, by a unique definable isomorphism π:X→Y. For a set domain X, the isomorphism and its image are sets. This holds without ambient Foundation.

Facts & Assumptions

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

[F1]

For a well-founded setlike extensional relation R on a definable class X, its collapse map π is injective. (An extensional collapse is injective)

[F2]

For a well-founded setlike relation R on X, the collapse map is the unique definable function satisfying π(x)={π(y):yRx}. Its existence and uniqueness follow from well-founded recursion. (Extensional relations and collapse maps)

Proof

1.1F1F2

Use the collapse map and let Y={π(x):x∈X}. It is injective by the extensional-collapse lemma and surjective onto this range by definition. If z∈π(x), its defining equation gives z=π(y) for some yRx; hence z∈Y. Thus Y is transitive.

2.1F1F2step 1.1

If yRx then π(y)∈π(x). Conversely, if π(y)∈π(x), the collapse equation gives zRx with π(z)=π(y); injectivity gives z=y. This proves preservation and reflection of the relation.

3.1F2step 2.1∎

For any other isomorphism j onto a transitive class Z, each member of j(x) lies in Z and so is j(y) for a unique y∈X. Relation reflection then says exactly yRx. Consequently j(x)={j(y):yRx}, the same recursion as π. Uniqueness of the collapse map gives j=π, and thus Z=Y. When X is a set, Replacement forms both its graph and image.

CorollaryStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Well-founded pointed graphs have unique decorations

Statement

Every well-founded accessible pointed graph (X,R,r) has a unique decoration d. Its range is TC⁡({d(r)}). If R is extensional, d is the unique isomorphism from (X,R) onto membership on that transitive set.

Facts & Assumptions

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

[F1]

An accessible pointed graph consists of a set X of nodes, a root r∈X, and a relation R⊆X2. Draw an arrow x→y precisely when yRx. Accessibility means that for every x∈X there are n∈ω and a function p:n+1→X with p(0)=r, p(n)=x, and p(i+1)Rp(i) for i<n. The path of length zero reaches the root. A decoration is a set function d on X such that d(x)={d(y):yRx} for each node. A well-founded graph means that R has the minimal-element property, not an unqualified no-infinite-path characterization. Extensionality is not part of the graph definition. No axiom of anti-foundation is assumed. Conventions and prerequisites: def-well-founded-setlike-relations. (Accessible pointed membership graphs)

[F2]

A setlike relation R on X is extensional when pred⁡R(x)=pred⁡R(y) implies x=y for x,y∈X. If R is also well-founded, its collapse map is the unique definable function π(x)={π(y):yRx}. Existence and uniqueness follow from well-founded recursion with G(x,h)=ran⁡(h), a set by Replacement. A collapse map is defined even without extensionality; injectivity is a further conclusion requiring extensionality. The construction for a supplied well-founded relation uses no ambient Foundation. Conventions and prerequisites: thm-recursion-on-well-founded-setlike-relations. (Extensional relations and collapse maps)

[F3]

For every set a, TC⁡(a) is transitive, contains a as a subset, and is contained in every transitive set T with a⊆T. Moreover a⊆b implies TC⁡(a)⊆TC⁡(b), and TC⁡(TC⁡(a))=TC⁡(a). In particular a∈TC⁡({a}). (Minimality and closure laws of TC)

[F4]

Every well-founded setlike extensional relation R on a definable class X is isomorphic to membership on a unique transitive definable class Y, by a unique definable isomorphism π:X→Y. For a set domain X, the isomorphism and its image are sets. This holds without ambient Foundation. (Mostowski collapse for extensional relations)

Proof

1.1F2F3

The collapse recursion, which does not require extensionality for existence, supplies a unique decoration on the set X. Its range D is transitive by the recursion equation and contains d(r) as an element, so minimality gives TC⁡({d(r)})⊆D.

2.1F1F3step 1.1

Every node x is reached from r by a finite predecessor path. Along this path the decoration of each next node is a member of the decoration of the preceding node. Transitivity therefore puts d(x) in TC⁡({d(r)}), starting with the root itself at path length zero. This gives the reverse inclusion.

3.1F4step 2.1∎

When R is extensional, Mostowski collapse makes the same decoration an isomorphism, unique among isomorphisms onto transitive targets. Step 2.1 identifies that target explicitly.

PropositionStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Minimum-rank selection and Collection

Statement

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

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, for every set x and ordinal α, x∈Vα  ⟺  rank⁡(x)<α,x⊆Vα  ⟺  rank⁡(x)≤α. Thus rank⁡(x) is the least α with x⊆Vα, and rank⁡(x)=α iff x∈Vα+1∖Vα. (Rank characterizes hierarchy membership)

Proof

1.1F1

Instantiate one c∈C and minimize the ranks attained in C among ordinals at most rank⁡(c). Separation on rank⁡(c)+1 and ordinal well-ordering yield a least such α, which is globally least. All members of rank α lie in Vα+1, so Separation inside that stage forms the asserted nonempty set.

2.1F1step 1.1

Given the Collection premise, for each x∈a the class of witnesses has a unique least rank αx by step 1.1. Replacement collects these ordinals; set γ=sup⁡{αx+1:x∈a}. The stage Vγ contains at least one witness for each x, because the witnesses of its minimum rank lie in Vαx+1⊆Vγ. Thus b=Vγ suffices. For a=∅, take γ=0.

3.1given∎

Conversely assume Separation and Collection, and let ϕ be functional on the set a. Collection supplies a set b containing a witness for each x∈a. Separation gives {y∈b:∃x∈a ϕ(x,y)}. Uniqueness ensures every value of ϕ occurs in this set and that every member is such a value, which is the Replacement conclusion. This direction does not use rank or a prior application of Replacement.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Hereditary size and H_kappa

Definition

Let κ be an infinite initial ordinal. In ZF set

Hκ={x:∃λ<κ ∃j (j:TC⁡({x})↪λ)}.

This initially defines a class. Its root-inclusive transitive closure contains x as an element. When TC⁡({x}) is well-orderable its hereditary cardinality means the least ordinal equinumerous with it; under Choice this exists for every set. The injection formulation above is used without Choice.

For infinite κ, replacing TC⁡({x}) by TC⁡(x) gives the same class. Indeed TC⁡({x})={x}∪TC⁡(x) by the finite-stage formula. Adding one point to a set injecting into finite λ gives an injection into λ+1<κ; for infinite λ, keep indices at least ω, shift natural indices by one, and use index zero for the added point, obtaining an injection into λ. Restriction gives the converse. We retain the root-inclusive convention throughout.

Conventions and prerequisites: Minimality and closure laws of TC, Cardinal (initial ordinal) and cardinality.

LemmaStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

A small transitive set bounds its ranks

Statement

In ZF, if a transitive set T injects into an ordinal λ<κ, where κ is an infinite initial ordinal, then rank⁡(t)<κ for every t∈T. No regularity or Choice is assumed.

Facts & Assumptions

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

[F1]

Let κ be an infinite initial ordinal. In ZF set Hκ={x:∃λ<κ ∃j (j:TC⁡({x})↪λ)}. This initially defines a class. Its root-inclusive transitive closure contains x as an element. When TC⁡({x}) is well-orderable its hereditary cardinality means the least ordinal equinumerous with it; under Choice this exists for every set. The injection formulation above is used without Choice. For infinite κ, replacing TC⁡({x}) by TC⁡(x) gives the same class. Indeed TC⁡({x})={x}∪TC⁡(x) by the finite-stage formula. Adding one point to a set injecting into finite λ gives an injection into λ+1<κ; for infinite λ, keep indices at least ω, shift natural indices by one, and use index zero for the added point, obtaining an injection into λ. Restriction gives the converse. We retain the root-inclusive convention throughout. Conventions and prerequisites: prop-transitive-closure-minimality, def-cardinal. (Hereditary size and H_kappa)

[F2]

Now assume ZF, including Foundation. Membership on the universe is well-founded and setlike, so its ordinal rank is defined for every set. Write rank⁡(x)=sup⁡{rank⁡(y)+1:y∈x}. The empty supremum is 0, so rank⁡(∅)=0. If y∈x, then rank⁡(y)<rank⁡(x). This is the Foundation-dependent special case of relation rank. The earlier construction of Vα did not require Foundation. Conventions and prerequisites: def-rank-of-a-well-founded-relation, thm-foundation-equivalent-to-hierarchy-exhaustion. (Membership rank under Foundation)

Proof

1.1F2

By Replacement, A={rank⁡(t):t∈T} is a set of ordinals. It is downward closed. To see this, suppose β<α∈A but β∉A, and choose the least attained rank γ>β. Take t∈T of rank γ. Every u∈t lies in T by transitivity, has rank below γ, and cannot have rank equal to β or strictly between β and γ. Thus all have rank below β, making rank⁡(t)≤β, a contradiction. Consequently A is an ordinal.

2.1F1step 1.1

A supplied injection j:T↪λ well-orders T by its image order. For each rank in A, take the preimage having least j-value. Replacement produces this uniquely specified section, so A injects into λ. Necessarily A<κ: otherwise restricting this injection to κ⊆A would inject κ into λ<κ. The image, ordered as a subset of λ, has order type at most λ, and its bijection with κ would contradict initiality. The order-type bound follows by induction along the enumeration of that subset: its element at position ξ is at least ξ.

3.1step 1.1step 2.1∎

For t∈T its rank belongs to the ordinal A<κ, so it is below κ. If T is empty then A=0 and the conclusion about its members is vacuous. No supremum of fewer-than-κ arbitrary ordinals was assumed to be below κ; the bound came from the injection.

TheoremStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

H_kappa is a transitive subset of V_kappa

Statement

In ZF, for every infinite initial ordinal κ, Hκ is a transitive set and Hκ⊆Vκ. For infinite initial ordinals κ≤μ, one has Hκ⊆Hμ.

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, if a transitive set T injects into an ordinal λ<κ, where κ is an infinite initial ordinal, then rank⁡(t)<κ for every t∈T. No regularity or Choice is assumed. (A small transitive set bounds its ranks)

[F2]

In ZF, for every set x and ordinal α, x∈Vα  ⟺  rank⁡(x)<α,x⊆Vα  ⟺  rank⁡(x)≤α. Thus rank⁡(x) is the least α with x⊆Vα, and rank⁡(x)=α iff x∈Vα+1∖Vα. (Rank characterizes hierarchy membership)

Proof

1.1F1F2

For x∈Hκ, let T=TC⁡({x}) and use its witnessing injection into λ<κ. This is a transitive set containing x as an element, so the small-ranks lemma gives rank⁡(x)<κ. Rank characterization puts x∈Vκ. Separation inside Vκ now proves that Hκ is a set.

2.1F1step 1.1

If y∈x∈Hκ, the transitive set TC⁡({x}) contains y, and hence contains TC⁡({y}) by minimality. Restrict the same witnessing injection to this smaller closure. Thus y∈Hκ, proving transitivity.

3.1F1∎

If κ≤μ, any witnessing ordinal λ<κ also satisfies λ<μ. The same injection proves x∈Hμ.

CorollaryStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Hereditary size exhausts V under Choice

Statement

Assume ZFC. For every set x there is an infinite initial ordinal κ with x∈Hκ. Hence the hereditary-size stages exhaust the universe in the class sense under Choice.

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, for every infinite initial ordinal κ, Hκ is a transitive set and Hκ⊆Vκ. For infinite initial ordinals κ≤μ, one has Hκ⊆Hμ. (H_kappa is a transitive subset of V_kappa)

[F2]

Assume the Axiom of Choice (def-axiom-of-choice). Then every set X can be well ordered: there is a relation on X making it a well-ordered set (def-well-order). The Axiom of Choice is used only inside thm-zorn, and nowhere else in the argument below. (The well-ordering theorem)

[F3]

For every set A there is an ordinal (def-ordinal) that does not inject into A, that is, admits no injective function into A. The least such ordinal is the Hartogs number ℵ(A), and it is exactly ℵ(A)={ot(S,R):S⊆A and R well-orders S}, the set of order types (thm-mostowski-collapse) of the well-ordered subsets of A. The proof is choice free. That is the whole point of the theorem: in ZF alone, with no assumption that A can be well ordered, one still gets an ordinal too long to be laid inside A. (Hartogs: an ordinal that does not inject into a given set)

Proof

1.1F1F2

Let T=TC⁡({x}). By the well-ordering theorem and AC, T is well-orderable and has an ordinal order type α. Set δ=α∪ω, an infinite ordinal into which T injects.

2.1F1F3step 1.1∎

Let κ be the Hartogs number of δ. It is initial: a bijection with any smaller ordinal would combine with an injection of that smaller ordinal into δ to contradict its defining noninjection. Also δ<κ, since every ordinal at most δ injects into δ. Thus κ is infinite and the injection T↪δ<κ witnesses x∈Hκ.

PropositionStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

H_omega equals V_omega

Statement

In ZF, Hω=Vω. These are exactly the sets whose root-inclusive transitive closure is finite, called hereditarily finite sets.

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, for every infinite initial ordinal κ, Hκ is a transitive set and Hκ⊆Vκ. For infinite initial ordinals κ≤μ, one has Hκ⊆Hμ. (H_kappa is a transitive subset of V_kappa)

[F2]

In ZF without Foundation define the cumulative hierarchy by V0=∅,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 ∅; 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α:α∈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)

Proof

1.1F1

The general bound gives Hω⊆Vω. The definition of Hω says its root closure injects into a finite ordinal, exactly finiteness: a subset of a finite ordinal can be enumerated in increasing order, and a finite set injects into its size.

1.2F2

Every Vn is finite by natural induction. V0 is empty. If Vn has m elements, membership bits relative to a finite enumeration biject its power set with the length-m binary words. Those form a finite set: for zero length there is one word, and appending either bit doubles the previous finite number. Thus Vn+1 is finite.

2.1F1F2step 1.2∎

If x∈Vω, choose n<ω with x∈Vn. The finite transitive set Vn contains x as an element, hence contains TC⁡({x}) by minimality. That closure is finite, so x∈Hω. Together with step 1.1 this proves equality.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Grothendieck universe closure convention

Definition

A Grothendieck universe, in the closure convention used here, is a nonempty transitive set U such that: if x,y∈U then {x,y}∈U; if x∈U then P(x)∈U; and if I∈U and f is any set function on I with f(i)∈U for every i∈I, then ⋃i∈If(i)∈U. The indexing function need not itself belong to U.

The additional condition ω∈U is imposed only when explicitly stated. This is a definition by closure conditions, not an assertion that a universe containing any prescribed set exists. Transitivity means that every member of a member of U is itself a member of U.

Conventions and prerequisites: Minimality and closure laws of TC.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Grothendieck universes and relative size

Remark

For a fixed universe U, “U-small” means being a member of U. It is relative to that specified set. Cardinal size alone does not determine it: a singleton can contain an ordinal of arbitrarily high rank, since rank⁡({α})=α+1 follows immediately from the rank equation and rank⁡(α)=α.

Our closure convention does not impose ω∈U. For example, Vω satisfies the closure conditions: its members lie in finite stages; pairs and power sets raise the stage by only finitely much; and a family indexed by one of its finite members has a finite bound on the stages of its values, so its union again lies in a finite stage. It is nonempty and transitive, but ω∉Vω by the ordinal-intersection formula. This explains why an uncountable-inaccessible characterization needs an additional infinity convention. Universe existence axioms and large-cardinal characterizations are not asserted here.

Conventions and prerequisites: Grothendieck universe closure convention, Ranks of ordinals and hierarchy stages.

5 · Examples, counterexamples and false statements

None yet.

Sources