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

The Axiom of Pairing is the sentence

$\mathrm{\forall }x\mathrm{\forall }y\mathrm{\exists }z\mathrm{\forall }t(t\in z\leftrightarrow (t=x\vee t=y))$

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 $\mathrm{\forall }x\mathrm{\forall }y\mathrm{\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 $\phi$, $\mathrm{\forall }\bar{p}\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(z\in y\leftrightarrow (z\in x\wedge \phi (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: $\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(\mathrm{\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.