How exactly do the ZFC axioms guarantee the existence of ordered pairs?

Question

How exactly do the ZFC axioms guarantee the existence of ordered pairs or exactly which axioms guarantee this and how? I've googled this question for 15 minutes but haven't found anything that remotely answers this. Thanks in advance.

Answer 1

It's a straightforward application of the pairing axiom.

Suppose I have two sets $a, b$. Then:

• $(i)$ The set $x=\{a, a\}=\{a\}$ exists by pairing. Note: the pairing axiom says $\forall x\forall y\exists z\forall w(w\in z\iff (w=x\vee w=y))$, and this nowhere requires $x\not=y$, so forming the pair $\{a, a\}$ is perfectly legal.

• $(ii)$ The set $y=\{a, b\}$ exists by pairing.

• $(iii)$ So the set $\{x, y\}$ exists by pairing. But this is just $\{\{a\}, \{a, b\}\}$, that is, $\langle a, b\rangle$.

---

This uses the Kuratowski definition of ordered pairs. There are other ways you can define ordered pairs (the ordered pair isn't a primitive concept in set theory), and if you want to use a different definition then the proof will be somewhat different. But for all the reasonable definitions of ordered pairs, it looks pretty much exactly the same as the above.

---

EDIT: As Asaf points out, the pairing axiom can easily be proved from the other ZFC axioms. I find it valuable to explicitly include it anyways, since I (and others) are frequently interested in subtheories of ZFC which contain the pairing axiom but don't contain the other axioms used to prove it.

Answer 2

This results from the axiom of pairing: an ordered pair is defined as $$(a,b)\stackrel{\text{def}}{=}\bigl\{\{a\},\{a,b\}\bigr\}.$$