The Axiom of Pairing: $\forall x\,\forall y\,\exists z\,\forall t\,(t \in z \leftrightarrow (t = x \vee t = y))$

The Axiom of Pairing is the sentence

$\forall x\,\forall y\,\exists z\,\forall t\,\bigl(t \in z \leftrightarrow (t = x \vee t = y)\bigr)$

of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations): for any $x$ and $y$ there is a set $z$ whose elements are exactly $x$ and $y$.

• The weak form is equivalent, given Separation. Several presentations assume only $\forall x\,\forall y\,\exists z\,(x \in z \wedge y \in z)$, a set containing $x$ and $y$ and possibly more, and then cut it down with 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)))$ applied to the formula $t = x \vee t = y$. The result is the set asserted here, so the two forms yield the same theorems. The same choice arises for The Axiom of Power Set: $\forall x\,\exists y\,\forall z\,(\forall t\,(t \in z \to t \in x) \to z \in y)$, where the weak form is the one assumed, so that the trimming step is visible in the ledger.

• Order and repetition are invisible. Taking $y := x$ gives a set whose only element is $x$. Because $t = x \vee t = y$ and $t = y \vee t = x$ are the same condition, the axiom does not distinguish the pair formed from $x$ then $y$ from the pair formed from $y$ then $x$; recovering an order from a set is the problem The Kuratowski ordered pair $(a,b) := \{\{a\},\{a,b\}\}$ solves.