ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

The finite von Neumann ordinals, and $ω$ as the least limit ordinal

Example

With $0 = \emptyset$ and $σ (n) = n \cup {n}$ (The natural numbers $N$ (von Neumann)) and the ordinals of Ordinal (von Neumann):

(i) $0, 1, 2, 3$ are ordinals, $1 = {0}$ , $2 = {0, 1}$ , $3 = {0, 1, 2} = 2 \cup {2} = 2^{+}$ , and for each $k \leq 3$ the set $k$ is exactly the set of ordinals below $k$ , so $k = {ξ : ξ < k}$ ;

(ii) $ω = N$ is an ordinal, $ω$ is a limit ordinal, the union of the members of $ω$ is $ω$ itself, and every element of $ω$ is either $0$ or a successor, so no element of $ω$ is a limit ordinal (Successor and limit ordinals, $ω$ is the least limit ordinal);

(iii) $ω$ is the least limit ordinal: $ω \leq γ$ for every limit ordinal $γ$ .

No choice principle is used.

Facts & Assumptions

Given: The von Neumann naturals $N = ω$ with $0 = \emptyset$ and $σ (n) = n \cup {n}$ , and the ordinal notation of Ordinal (von Neumann): a set $α$ is an ordinal when it is transitive and $\in$ strictly well-orders it, with $α < β$ meaning $α \in β$ and $α^{+} = α \cup {α}$ .

[F1]

An ordinal is a transitive set on which $\in$ is a strict well-order, $0 : = \emptyset$ is an ordinal, $α^{+} = α \cup {α}$ , and for ordinals $α < β$ means $α \in β$ while $α \leq β$ means $α \in β$ or $α = β$ (Ordinal (von Neumann)).

[F2]

For every ordinal $α$ : every element of $α$ is an ordinal, and $α^{+}$ is an ordinal (Basic closure properties of ordinals).

[F3]

$N = ω$ is the smallest inductive set, with $0 = \emptyset$ , $σ (n) = n \cup {n}$ , $1 = {0}$ , $2 = {0, 1}$ , $3 = {0, 1, 2}$ and in general $n = {0, 1, \dots, n - 1}$ ; $ω$ is inductive, so $0 \in ω$ and $n \in ω$ implies $σ (n) \in ω$ (The natural numbers $N$ (von Neumann)).

[F4]

Every natural number is an ordinal, and $ω$ is an ordinal; $ω$ is a limit ordinal; every ordinal $α \in ω$ is $0$ or a successor ordinal; and $ω \subseteq γ$ for every limit ordinal $γ$ ( $ω$ is the least limit ordinal).

[F5]

An ordinal $α$ is a successor ordinal when $α = β^{+}$ for some ordinal $β$ , and a limit ordinal when $α \neq 0$ and $α$ is not a successor (Successor and limit ordinals).

[F6]

Every natural number is a transitive set and satisfies $n \notin n$ (Every natural number is a transitive set and is not a member of itself).

Verification

technique · direct

1.1F1F2F3F4

Claim (i): $0 = \emptyset$ is an ordinal by [F1]; $1 = 0^{+} = {0}$ , $2 = 1^{+} = {0, 1}$ and $3 = 2^{+} = {0, 1, 2}$ by [F3], and each is an ordinal by the successor clause of [F2], so $3 = 2 \cup {2} = 2^{+}$ as displayed. For $k \leq 3$ : every element $ξ$ of $k$ is a natural number, hence an ordinal by [F4], and conversely every ordinal $ξ$ with $ξ < k$ satisfies $ξ \in k$ by [F1]; the two sides of $k = {ξ : ξ < k}$ therefore have the same members, since the elements of $k$ are among the ordinals below $k$ and every ordinal below $k$ is an element of $k$ .

1.2F1F3F4F5F6

Claim (ii): $ω$ is an ordinal by [F4] and is a limit ordinal by [F4], and since $ω \neq 0$ by [F3] we may compute the union of its members. First $⋃ ω \subseteq ω$ : a member of $⋃ ω$ is a member of some $n \in ω$ , and $n \subseteq ω$ because $ω$ is transitive as an ordinal while $n \in ω$ , so that member lies in $ω$ as well. Conversely $ω \subseteq ⋃ ω$ : for $n \in ω$ the successor $σ (n) = n \cup {n}$ again lies in $ω$ by inductivity, and $n \in σ (n)$ , so every member of $ω$ lies in a member of $ω$ . Hence $⋃ ω = ω$ by extensionality. Finally every element of $ω$ is $0$ or a successor by [F4], and a limit ordinal is nonzero and not a successor by [F5], so no element of $ω$ is a limit ordinal.

1.3F1F4

Claim (iii): [F4] states that $ω \subseteq γ$ , that is $ω \leq γ$ in the ordinal order of [F1], for every limit ordinal $γ$ ; with $ω$ itself a limit ordinal by [F4], this says $ω$ is the least limit ordinal.

2.1step 1.1step 1.2step 1.3∎

Claims (i) to (iii) are established: the finite levels $0, 1, 2, 3$ are ordinals with $k = {ξ : ξ < k}$ by step 1.1, the ordinal $ω$ is a limit ordinal, equals the union of its members, and has no limit ordinal among its elements by step 1.2, and it is least among limit ordinals by step 1.3. Every ingredient is a theorem of ZF applied to the given sets, and nothing is selected from a family of sets, so no choice principle is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

A. Marks, Set Theory (Berkeley lecture notes, 2026) (standard reference, not scraped)
J. T. Moore, MATH 6870: Set Theory (Cornell lecture notes) (standard reference, not scraped)

The finite von Neumann ordinals, and ωω as the least limit ordinal