Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-06 (claude-opus-5)
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.

There is exactly one set with no elements, written ∅

Statement

There is exactly one set with no elements: there is a set e such that ¬∃z (z∈e), and any two such sets are equal. That set is written ∅.

Facts & Assumptions

Given: the language of set theory, in which the domain of discourse is nonempty (The first-order language of set theory: ∈, =, formulas with parameters, and class abbreviations).

[L1]

For any parameters pˉ and any set x, there is a set y whose elements are exactly the elements z of x for which φ(z,pˉ) holds (The Axiom Schema of Separation: for each formula φ, ∀pˉ ∀x ∃y ∀z (z∈y↔(z∈x∧φ(z,pˉ)))).

[L2]

If every z satisfies z∈x if and only if z∈y, then x=y (The Axiom of Extensionality: ∀x ∀y (∀z (z∈x↔z∈y)→x=y)).

Proof

technique · direct
1.1

The domain of discourse is nonempty, so fix a set a.

givenchoose
2.1

Apply Separation to a with the formula φ(z):=¬(z=z): there is a set e such that, for every z, z∈e holds if and only if z∈a and ¬(z=z).

L1step 1.1
3.1

No z satisfies ¬(z=z), so no z satisfies z∈e; hence e is a set with no elements, which proves existence.

step 2.1
4.1

If e′ is also a set with no elements, then z∈e and z∈e′ both fail for every z, so z∈e holds if and only if z∈e′, and therefore e=e′; existence and uniqueness together give the statement, and ∅ denotes this set.

L2step 3.1∎

Remarks

  • Existence is derived, not assumed. Several presentations take "there is a set with no elements" as an axiom of its own. Here it is a theorem, because the nonemptiness of the domain of discourse is already a validity of first-order logic and Separation converts any set whatever into this one.

Depends on

Used by

Dependency tree · one level

3 results within one dependency step 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