nLab unordered pair

Unordered pairs

Unordered pairs


The unordered pair of xx and yy, denoted {x,y}\{x,y\}, has the property that {x 1,y 1}={x 2,y 2}\{x_1,y_1\} = \{x_2,y_2\} if and only if x 1=x 2x_1 = x_2 and y 1=y 2y_1 = y_2 or x 1=y 2x_1 = y_2 and y 1=x 2y_1 = x_2. In other words, the unordered pair {x,y}\{x,y\} is the same as the ordered pair (x,y)(x,y), except that presentation order does not matter.


In structural set theory and material set theory with ordered pairing structure, given a set AA, the set of unordered pairs of elements of AA is the quotient set A×A/A \times A / \sim, where \sim is a binary relation on A×AA \times A where (x,y)(y,x)(x, y) \sim (y, x) for all elements xAx \in A and yAy \in A. An unordered pair is just an element of said quotient set.

In material set theory without ordered pairing structure, an unordered pair is usually just defined as a pair set.

 In type theory

In dependent type theory, let AA be an h-set. Then the type of unordered pairs of elements in AA is a higher inductive type UnorderedPairs(A)\mathrm{UnorderedPairs}(A) generated by the constructors

  • {,}:A×AUnorderedPairs(A)\{-,-\}:A \times A \to \mathrm{UnorderedPairs}(A)
  • a:A,b:Aeq {,}(a,b):{a,b}= UnorderedPairs(A){b,a}a:A, b:A \vdash \mathrm{eq}_{\{-,-\}}(a, b):\{a,b\} =_{\mathrm{UnorderedPairs}(A)} \{b,a\}
  • a:A,c(a):{a,a}= UnorderedPairs(A){a,a}K(a):eq {,}(a,a)= {a,a}= UnorderedPairs(A){a,a}c(a)a:A, c(a):\{a,a\} =_{\mathrm{UnorderedPairs}(A)} \{a,a\} \vdash K(a):\mathrm{eq}_{\{-,-\}}(a, a) =_{\{a,a\} =_{\mathrm{UnorderedPairs}(A)} \{a,a\}} c(a)

Relation to ordered pairs

The unordered pair {x,y}\{x,y\} should not be confused with the ordered pair (x,y)(x,y). In particular, {x,y}={y,x}\{x,y\} = \{y,x\}, while (x,y)(y,x)(x,y) \neq (y,x) (if xyx \neq y).

In material set theory, {x,y}\{x,y\} has a direct definition, but (x,y)(x,y) must be coded in a complicated way (traditionally as {{x},{x,y}}\big\{\{x\}, \{x,y\}\big\}). In structural set theory, (x,y)(x, y) has a direct definition, and {x,y}\{x,y\} must be coded in a complicated way (traditionally as an element of the quotient set A×A/(x,y)(y,x)A \times A / (x, y) \sim (y, x)).

However, the two are somewhat related:

  • As just seen, the usual encoding of an ordered pair of pure sets as a pure set (due to Kuratowski) involves unordered pairs. Conversely, the set ((A2))\big(\!\big({A \atop 2}\big)\!\big) of unordered pairs of elements of AA may be constructed as a quotient set of the set A 2A^2 of ordered pairs of elements of AA (by the equivalence relation generated by declaring that (x,y)(y,x)(x,y) \sim (y,x)).
  • Just as unordered pairs (through the axiom of pairing) are needed to get anywhere in material set theory, so some axiom related to ordered pairs is needed to get anywhere in structural set theory. (In ETCS, this is the axiom of the (Cartesian) product; in SEAR, this is the axiom of tabulations.)

Despite the name of the axiom of pairing, the term ‘pairing’ in the nnLab usually refers to ordered pairs.

 See also

Last revised on December 12, 2022 at 12:31:05. See the history of this page for a list of all contributions to it.