Category:Axioms/Von Neumann-Bernays-Gödel Axioms

From ProofWiki
Jump to navigation Jump to search

This category contains axioms related to Von Neumann-Bernays-Gödel Axioms.


The Axiom of Extension

Let $A$ and $B$ be classes.

Then:

$\forall x: \paren {x \in A \iff x \in B} \iff A = B$


The Axiom of Pairing

For any two sets, there exists a set to which only those two sets are elements:

$\forall a: \forall b: \exists c: \forall z: \paren {z = a \lor z = b \iff z \in c}$


The Axioms of Class Existence

\((\text B 1)\)   $:$   \(\ds \exists X: \forall u, v: \tuple {u, v} \in X \iff u \in v \)      $\in$-relation
\((\text B 2)\)   $:$   \(\ds \forall X, Y: \exists Z: \forall u: u \in Z \iff u \in X \land u \in Y \)      intersection
\((\text B 3)\)   $:$   \(\ds \forall X: \exists Z: \forall u: u \in Z \iff u \notin X \)      complement
\((\text B 4)\)   $:$   \(\ds \forall X: \exists Z: \forall u: u \in Z \iff \exists v: \tuple {u, v} \in X \)      domain
\((\text B 5)\)   $:$   \(\ds \forall X: \exists Z: \forall u, v: \tuple {u, v} \in Z \iff u \in X \)      
\((\text B 6)\)   $:$   \(\ds \forall X: \exists Z: \forall u, v, w: \tuple {\tuple {u, v}, w} \in Z \iff \tuple {\tuple {v, w}, u} \in X \)      
\((\text B 7)\)   $:$   \(\ds \forall X: \exists Z: \forall u, v, w: \tuple {\tuple {u, v}, w} \in Z \iff \tuple {\tuple {u, w}, v} \in X \)      


The Axiom of Unions

For every set of sets $A$, there exists a set $x$ (the union set) that contains all and only those elements that belong to at least one of the sets in the $A$:

$\forall A: \exists x: \forall y: \paren {y \in x \iff \exists z: \paren {z \in A \land y \in z} }$


The Axiom of Powers

For every set, there exists a set of sets whose elements are all the subsets of the given set.

$\forall x: \exists y: \paren {\forall z: \paren {z \in y \iff \paren {w \in z \implies w \in x} } }$


The Axiom of Replacement

For every mapping $f$ and set $x$ in the domain of $f$, the image $f \sqbrk x$ is a set.


Symbolically:

$\forall Y: \map {\text{Fnc}} Y \implies \forall x: \exists y: \forall u: u \in y \iff \exists v: \tuple {v, u} \in Y \land v \in x$

where:

$\map {\text{Fnc}} X := \forall x, y, z: \tuple {x, y} \in X \land \tuple {x, z} \in X \implies y = z$

and the notation $\tuple {\cdot, \cdot}$ is understood to represent Kuratowski's formalization of ordered pairs.


The Axiom of Infinity

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


The Axiom of Foundation

For any non-empty class, there is an element of the class that shares no element with the class.

$\forall X: X \ne \O \implies \exists y: y \in X \land y \cap X = \O$


The Axiom of Global Choice

There exists a mapping $f : V \setminus \set \O \to V$, where $V$ is the universal class, such that:

$\forall x \in V: \map f x \in x$

Symbolically:

$\exists A: \map {\text{Fnc}} A \land \forall x: x \ne \O \implies \exists y: y \in x \land \tuple {x, y} \in A$