LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

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 natural numbers exist: a smallest inductive set

Statement

There is a set $ω$ that is inductive (Inductive set) and is a subset of every inductive set; it is unique. This $ω$ is the set of natural numbers.

Facts & Assumptions

Given: ZFC; in particular the Axiom of Infinity (The Axiom of Infinity: there is a set containing a set with no elements and closed under $y \mapsto y \cup {y}$ ): there exists an inductive set; the Axiom Schema of Separation (The Axiom Schema of Separation: for each formula $φ$ , $\forall \overset{ˉ}{p} \forall x \exists y \forall z (z \in y \leftrightarrow (z \in x \land φ (z, \overset{ˉ}{p})))$ ); and Extensionality (The Axiom of Extensionality: $\forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \to x = y)$ ). Write $x^{+} : = x \cup {x}$ . Recall that $I$ inductive means $\emptyset \in I$ and ( $x \in I \Rightarrow x^{+} \in I$ ).

Proof

technique · direct

1.1

By the Axiom of Infinity fix an inductive set $I_{0}$ .

given

1.2

By Separation the collection $ω : = {x \in I_{0} : x \in J for every inductive set J}$ is a set.

givenconstruct

2.1

$ω$ is inductive: $\emptyset \in J$ for every inductive $J$ (so $\emptyset \in I_{0}$ and $\emptyset \in ω$ ), and if $x \in ω$ then $x \in J$ for every inductive $J$ , hence $x^{+} \in J$ for every inductive $J$ , and $x^{+} \in I_{0}$ since $x \in I_{0}$ and $I_{0}$ is inductive, so $x^{+} \in ω$ .

step 1.2

2.2

$ω \subseteq J$ for every inductive $J$ : any $x \in ω$ satisfies $x \in J$ by definition.

step 1.2

3.1

Uniqueness: if $ω^{'}$ is also inductive and contained in every inductive set, then $ω \subseteq ω^{'}$ (as $ω^{'}$ is inductive) and $ω^{'} \subseteq ω$ (as $ω$ is inductive), so $ω = ω^{'}$ by Extensionality.

step 2.1step 2.2∎

Depends on

Used by

The natural numbers ℕ (von Neumann) Definition
ω is the least limit ordinal Lemma
The principle of mathematical induction Theorem

Dependency tree · two levels

8 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

Axiom of infinity (Wikipedia) (standard reference, not scraped)
Set-theoretic definition of natural numbers (Wikipedia) (standard reference, not scraped)
B. Kaya, MATH 320 Set Theory (METU lecture notes) (standard reference, not scraped)