LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 $\omega$ that is inductive (Inductive set) and is a subset of every inductive set; it is unique. This $\omega$ 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 $\varphi$ , $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar 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 $\varnothing \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 $\omega := \{x \in I_0 : x \in J \text{ for every inductive set } J\}$ is a set.

givenconstruct

2.1

$\omega$ is inductive: $\varnothing \in J$ for every inductive $J$ (so $\varnothing \in I_0$ and $\varnothing \in \omega$ ), and if $x \in \omega$ 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 \omega$ .

step 1.2

2.2

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

step 1.2

3.1

Uniqueness: if $\omega'$ is also inductive and contained in every inductive set, then $\omega \subseteq \omega'$ (as $\omega'$ is inductive) and $\omega' \subseteq \omega$ (as $\omega$ is inductive), so $\omega = \omega'$ 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 8 results over 4 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)