# Why is Axiom of Pairing needed?

I'm learning ZFC set theory and I'm very confused about the Axiom of Pairing.

Axiom of Pairing: For any $a$ and $b$ there exists a set $\{a, b\}$ that contains exactly $a$ and $b$.

It seems that this axiom can be derived from other axioms in a lot of ways. For example, consider the powerset of the powerset of $\varnothing$, which is $\{\varnothing,\{\varnothing\}\}$, and then we apply the Axiom Schema of Replacement we can get $\{a,b\}$.

I looked for Wiki. It says the "non-independence" as well.

I'm confused why the Axiom of Pairing is important and independent. Also, why do we use "pair sets" instead of "singleton sets"? It seems equivalant that we use "singleton sets" axiom and the Axiom of Union to deduce the Axiom of Pairing?

• In the presence of Replacement, Pairing is indeed redundant. However, it's often interesting to study Z (or ZC), which is ZF (or ZFC) without replacement, and in this context Pairing is needed explicitly. Commented Jun 8, 2018 at 22:53
• How would singletons and Union give you Pairing? Commented Jun 8, 2018 at 22:55
• @EricWofsey From Tao's Analysis “Conversely, the pair set axiom will follow from the singleton set axiom and the pairwise union axiom below (see Lemma 3.1.13).” The pairwise union axiom can be deduced from the axiom of union. So I think if $a$ is an object, then there exists a set $\{a\}$, if $b$ is an object, then there exists a set $\{b\}$, then we can use the pairwise union axiom to get $\{a,b\}$. Is it right? Commented Jun 8, 2018 at 23:01
• How can the pairwise union axiom be deduced from the union axiom, without Pairing? Commented Jun 8, 2018 at 23:02
• @EricWofsey I got you! Thank you. I overlooked that I need Pairing to construct $\{\{a\},\{b\}\}$. Commented Jun 8, 2018 at 23:09

Note that Replacement cannot be philosophically justified non-circularly, so philosophically you would want to distinguish between theorems that rely on Replacement and theorems that do not. Pairing is in contrast rather innocuous, and is crucial in obtaining ordered pairs (meaning definable pairing and projection) in Zermelo set theory.

Also, even if one axiom implies another, it does not imply that the weaker one is unimportant. For example, the unrestricted comprehension axiom (schema) of naive set theory entails Pairing and Union and Powerset and Replacement, but also entails contradiction. What is important is what can be justified and not usually what can imply more things.

In the case of Pairing, it captures a relatively simple notion that given any two objects $a,b$ we can form a single collection whose members must each be either equal to $a$ or $b$. 'Clearly' we can form such a conceptual collection.

It is true that if ZFC is meaningful then Replacement can be considered more fundamental than Separation and Pairing, because it not only entails them but also itself corresponds to reification of definable functions on a set, meaning that for any formula $P$ such that $\forall x \in S\ \exists! y ( P(x,y) )$ ($P$ is a definable function) there is an object $f$ representing $P$, namely $\forall x \in S\ \exists! y ( (x,y) \in f )$. Note that unrestricted reification of definable functions on a set entails a contradiction, just as unrestricted reification of definable 1-place predicates (which is precisely unrestricted comprehension) entails a contradiction.

But to give an example showing that it is not philosophically sufficient to have mere consistency, consider that PA+¬Con(PA) proves everything that PA does, and is consistent, but most logicians reject it as meaningless to the real world, unlike PA+Con(PA), which most logicians accept as true (or a good approximation) of real-world 'natural numbers'.

In ZFC theory the Axiom of Pairing appears rather early, so its justification need not be too complicated. In the OP's example, where he asserted the existence of $$\{\emptyset,\{\emptyset\}\}$$, he already invoked the Axiom of Pairing. Now, you (and the OP himself) might argue that what was invoked was the Axiom of Powerset. However, the Axiom of Powerset is meant to be invoked to construct sets of infinite depth (having infinite nested brackets). The ZFC theory describes a universe where sets are constructed inductively. Like in all metamathematical inductive formulations, you need a basis, and you need an induction hypothesis. The basis and the induction hypothesis are two different things, and one does not replace the other. In the present case, the Axiom of Pairing plays the role of the basis, while the Axiom of the Powerset plays the role of the induction hypothesis. Thus, the very example used already demonstrated the necessity of the Axiom of Pairing, for without it $$\{\emptyset,\{\emptyset\}\}$$ can not be claimed to be a set.

As to the Axiom Schema of Replacement, it is meant to rein in what is meant by infinity. To see this, note that while a Russell class is infinite in size and is not a set, a powerset is infinite in size and is a set. The Axiom Schema of Replacement can then be invoked to construct sets of desired sizes, as shown by the OP. It is an important and integral part of ZFC theory. With it, you can quickly assert the existence of a set without having to build it from the ground up. This frees you from the worries of having sets that are infinite yet not "too large". Thus, both the Axiom of Pairing and the Axiom Schema of Replacement have their places. One does not make the other redundant.

• What you're saying is absolutely wrong. Pairing plays exactly zero part in the recursive construction of the universe; and just because the power set axiom is more pronounced in the infinite case does not mean that it has no benefits for the finite case. Indeed, the existence of $\{\varnothing,\{\varnothing\}\}$ follows entirely from Infinity and Extensionality. Pairing is entirely redundant if your goal is to study ZFC or ZF. It is useful, though, once you start removing axioms and you want to study weaker systems. Commented Oct 13, 2020 at 11:06
• @AsafKaragila So pairing being entirely redundant is necessary for studying ZFC? That's amazing logic. By saying that it is useful, you have contradicted yourself. I stand by what I wrote. Commented Oct 18, 2020 at 10:32
• I think you misread my comment. Try again, maybe with less anger. Commented Oct 18, 2020 at 10:34
• @AsafKaragila Well, a logic proof will have to end somewhere. Mine has ended. Commented Oct 18, 2020 at 10:38
• That a particular axiom is redundant means, in this context, that it is implied by the rest of the axioms (so it can be omitted and the theory proves exactly the same things). So for example, the axiom of pairing and the axiom schema of separation can be omitted from ZF or ZFC, because they follow from the axiom schema of replacement (together with the axiom of infinity, which requires the existence of an empty set). So why do the usual formulations of set theory include these axioms? For historical reasons, and for convenience. Commented Feb 12, 2021 at 17:17