nLab unordered pair

Idea

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

Definition

In structural set theory and material set theory with ordered pairing structure, given a set $A$, the set of unordered pairs of elements of $A$ is the quotient set $A \times A / \sim$, where $\sim$ is a binary relation on $A \times A$ where $(x, y) \sim (y, x)$ for all elements $x \in A$ and $y \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 $A$ be an h-set. Then the type of unordered pairs of elements in $A$ is a higher inductive type $\mathrm{UnorderedPairs}(A)$ generated by the constructors

• $\{-,-\}:A \times A \to \mathrm{UnorderedPairs}(A)$
• $a:A, b:A \vdash \mathrm{eq}_{\{-,-\}}(a, b):\{a,b\} =_{\mathrm{UnorderedPairs}(A)} \{b,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\}$ should not be confused with the ordered pair $(x,y)$. In particular, $\{x,y\} = \{y,x\}$, while $(x,y) \neq (y,x)$ (if $x \neq y$).

In material set theory, $\{x,y\}$ has a direct definition, but $(x,y)$ must be coded in a complicated way (traditionally as $\big\{\{x\}, \{x,y\}\big\}$). In structural set theory, $(x, y)$ has a direct definition, and $\{x,y\}$ must be coded in a complicated way (traditionally as an element of the quotient set $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 $\big(\!\big({A \atop 2}\big)\!\big)$ of unordered pairs of elements of $A$ may be constructed as a quotient set of the set $A^2$ of ordered pairs of elements of $A$ (by the equivalence relation generated by declaring that $(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 $n$Lab usually refers to ordered pairs.

 See also

• pair set
• axiom of pairing