nLab
axiom of pairing

The 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 xx and yy are (material) sets, then there exists a set PP such that x,yPx, y \in P.

Using the axiom of separation (bounded separation is enough), we can prove the existence of a particular set PP such that xx and yy are the only members of PP. Using the axiom of extensionality, we can then prove that this set PP is unique; it is usually denoted {x,y}\{x,y\} and called the unordered pair of xx and yy. Note that {x,x}\{x,x\} may also be denoted simply {x}\{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,,x nx_1, \ldots, x_n are sets, then there exists a set PP such that x 1,,x nPx_1, \ldots, x_n \in P.

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

Proof

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

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

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

In the nnLab, the term ‘pairing’ usually refers to ordered pairs.

Revised on September 5, 2011 16:10:09 by Toby Bartels (75.88.82.16)