nLab
axiom of pairing

Idea

In material set theory as a foundation of mathematics, the axiom of pairing is an important axiom needed to get the foundations off the ground (to mix metaphors). It states that unordered pairs exist.

Statement

The axiom of pairing (or axiom of pairs) states the following:

Axiom (pairing)

If $x$ and $y$ are (material) sets, then there exists a set $P$ such that $x,y\in P$.

Using the axiom of separation (bounded separation is enough), we can prove the existence of a particular set $P$ such that $x$ and $y$ are the only members of $P$. Using the axiom of extensionality, we can then prove that this set $P$ is unique; it is usually denoted $\{x,y\}$ and called the unordered pair of $x$ and $y$. Note that $\{x,x\}$ may also be denoted simply $\{x\}$.

Generalisation

The axiom of pairing is the binary part of a binary/nullary pair whose nullary part is the axiom stating the existence of the empty set. We can use these axioms and the axiom of union to prove every instance of the following axiom (or rather theorem) schema of finite sets:

Theorem (finite sets)

If $x_1,\dots ,x_n$ are sets, then there exists a set $P$ such that $x_1,\dots ,x_n\in P$.

Again, we can prove the existence of specific $P$ such that $x_1,\dots ,x_n$ are the only members of $P$ and prove that this $P$ is unique; it is denoted $\{x_1,\dots ,x_n\}$ and is called the finite set consisting of $x_1,\dots ,x_n$.

Note that this is a schema, with one instance for every (metalogical) natural number. Within axiomatic set theory, this is very different from the single statement that begins with a universal quantification over the (internal) set of natural numbers. In particular, each instance of this schema can be stated and proved without the axiom of infinity.

Proof

Of course, there is one proof for each natural number.

• For $n=0$, this is simply the axiom of the empty set.
• For $n=1$, we use the axiom of pairing with $x≔x_1$ and $y≔x_1$ to construct $\{x_1\}$.
• For $n=2$, we use the axiom of pairing with $x≔x_1$ and $y≔x_2$ to construct $\{x_1,x_2\}$.
• For $n=3$, we first use the axiom of pairing twice to construct $\{x_1,x_2\}$ and $\{x_3\}$, then use pairing again to construct $\{\{x_1,x_2\},\{x_3\}\}$, then use the axiom of union to construct $\{x_1,x_2,x_3\}$.
• In general, once we have $\{x_1,\dots ,x_{n-1}\}$, we use pairing to construct $\{x_n\}$, use pairing again to construct $\{\{x_1,\dots ,x_{n-1}\},\{x_n\}\}$, then use the axiom of union to construct $\{x_1,\dots ,x_n\}$. (A direct proof of a single statement for $n>3$ can actually go faster than this; the length of the shortest proof is logarithmic in $n$ rather than linear in $n$.)

Note that these ‘finite sets’ are precisely the Kuratowski-finite sets in a constructive treatment.

Related notions

In the $n$Lab, the term ‘pairing’ usually refers to ordered pairs.

category: foundational axiom