Axiom:Axiom of Infinity/Set Theory

From ProofWiki
Jump to navigation Jump to search


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}$

Also see