axiom of pairing

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.

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

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\}$.

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**:

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

Again, we can prove the existence of specific $P$ such that $x_1, \ldots, x_n$ are the *only* members of $P$ and prove that this $P$ is unique; it is denoted $\{x_1, \ldots, x_n\}$ and is called the **finite set** consisting of $x_1, \ldots, 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.

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 \coloneqq x_1$ and $y \coloneqq x_1$ to construct $\{x_1\}$.
- For $n = 2$, we use the axiom of pairing with $x \coloneqq x_1$ and $y \coloneqq 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 $\big\{\{x_1, x_2\}, \{x_3\}\big\}$, then use the axiom of union to construct $\{x_1, x_2, x_3\}$.
- In general, once we have $\{x_1, \ldots, x_{n-1}\}$, we use pairing to construct $\{x_n\}$, use pairing again to construct $\big\{\{x_1, \ldots, x_{n-1}\}, \{x_n\}\big\}$, then use the axiom of union to construct $\{x_1, \ldots, x_n\}$. (A direct proof of a single statement for $n \gt 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.

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

category: foundational axiom