Axiom:Axiom of Infinity/Set Theory

Axiom

There exists a set containing:

$(1): \quad$ a set with no elements

$(2): \quad$ the successor of each of its elements.

That is:

$\exists x: \paren {\paren {\exists y: y \in x \land \forall z: \neg \paren {z \in y} } \land \forall u: u \in x \implies u^+ \in x}$

In this context, the successor of the set $u$, written $u^+$, is defined as $u^+ := u \cup \set u$.

The symbol $\cup$ represents set union and $\set u$ represents the singleton containing $u$.

In an axiomatization of set theory that includes the Axiom of the Empty Set, the above can be abbreviated to:

$\exists x: \O \in x \land \forall u: \paren {u \in x \implies u^+ \in x}$

Weisstein, Eric W. "Zermelo-Fraenkel Axioms." From MathWorld--A Wolfram Web Resource. https://mathworld.wolfram.com/Zermelo-FraenkelAxioms.html