nLab axiom of pairing

The 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 pair sets exist.

Statement

Pairing

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

Axiom of pairing: If xx and yy are (material) sets, then there exists a set PP such that xPx \in P and yPy \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 pair set of xx and yy. Note that {x,x}\{x,x\} may also be denoted simply {x}\{x\}.

One could also assume that the material set theory has a primitive binary operation PP which takes of a material set xx and yy and returns a material set P(x,y)P(x, y). Then the axiom of pairing becomes

Axiom of pairing: If xx and yy are (material) sets, then xP(x,y)x \in P(x, y) and yP(x,y)y \in P(x, y).

Unordered pairing

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

Axiom of unordered pairing: If xx and yy are (material) sets, then there exists a set PP such that xPx \in P and yPy \in P and for all sets zz, zPz \in P implies that z=xz = x or z=yz = y.

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 pair set of xx and yy. Note that {x,x}\{x,x\} may also be denoted simply {x}\{x\}.

One could also assume that the material set theory has a primitive binary operation {,}\{-,-\} which takes of a material set xx and yy and returns a material set {x,y}\{x, y\}. Then the axiom of pairing becomes

Axiom of unordered pairing: If xx and yy are (material) sets, then x{x,y}x \in \{x, y\}, y{x,y}y \in \{x, y\}, and for all sets zz, z{x,y}z \in \{x, y\} implies that z=xz = x or z=yz = y.

Ordered pairing

Let us assume that the material set theory has a primitive binary operation (,)(-,-) which takes of a material set xx and yy and returns a material set (x,y)(x, y).

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

Axiom of ordered pairing: If xx and yy are (material) sets, then x(x,y)x \in (x, y), y(x,y)y \in (x, y), and for all sets aa and bb, (a,b)=(x,y)(a, b) = (x, y) if and only if a=xa = x and b=yb = y.

a.b.{a,b}={x,y}(a=xb=y)\forall a.\forall b.\{a, b\} = \{x, y\} \iff (a = x \wedge b = y)

With sets and elements different

In set theories where sets and elements are not the same thing, pairing becomes an operation on both the sets and the elements. One has to add a primitive ternary relation p(X,Y,P)p(X, Y, P) which says that PP is the Cartesian product of XX and YY, as well as primitive quaternary relations π 1(X,P,c,a)\pi_1(X, P, c, a) and π 2(Y,P,c,b)\pi_2(Y, P, c, b) which says that element aXa \in X is the left element of the pair cPc \in P and element bYb \in Y is the right element of the pair cPc \in P, and the following axiom:

Axiom of ordered pairing: If XX and YY are sets, then there exists a set PP such that p(X,Y,P)p(X, Y, P) and for every object aa and bb, aXa \in X and bYb \in Y implies that there exists an object cc such that cPc \in P, π 1(X,P,c,a)\pi_1(X, P, c, a), and π 2(Y,P,c,b)\pi_2(Y, P, c, b)

PP is usually denoted X×YX \times Y and called the Cartesian product of XX and YY, while cc is usually denoted (a,b)(a, b) and called the ordered pair of aa and bb.

In dependent type theory

In dependent type theory, it is possible to define a Tarski universe (V,)(V, \in) of pure sets which behaves as a material set theory. The universal type family of the Tarski universe is given by the type family x:V y:Vyxx:V \vdash \sum_{y:V} y \in x. The axiom of pairing is given by the following inference rule:

ΓctxΓpairing V: x:V y:V P:V(xP)×(yP)\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{pairing}_V:\prod_{x:V} \prod_{y:V} \sum_{P:V} (x \in P) \times (y \in P)}

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

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. 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.

References

For the axiom of ordered pairing see:

Last revised on February 28, 2024 at 03:14:48. See the history of this page for a list of all contributions to it.