ordered pair

Given any things $a$ and $b$, the **ordered pair** of $a$ and $b$ is a thing, usually written $(a,b)$, sometimes $[a,b]$ or $\langle{a,b}\rangle$. The important property is

(1)$(a,b) = (c,d) \;\Leftrightarrow\; a = c,\; b = d .$

The things $a$ and $b$ are called the **components** of the ordered pair $(a,b)$. Given any two sets $X$ and $Y$, their Cartesian product is a set $X \times Y$ whose elements are precisely the ordered pairs whose components are respectively elements of $X$ and elements of $Y$.

Note that nothing is **ordered** in an ordered pair other than how it is written out, so sometimes just the word **pair** is used for this concept. The concept of “pair” meaning a set containing just one or two members as in the axiom of pairing of Zermelo–Frankel Set Theory is now usually distinguished as an **unordered pair**. A pair in which the components are ordered is basically an arrow between the components, which is sometimes called or analyzed as an interval within a larger context.

One may wish to declare ordered pairs to exist by fiat, which was done, for example, by both Bourbaki and Bill Lawvere. In Bourbaki's foundational set theory, $\langle{-,-}\rangle$ is a fundamental binary operation on mathematical objects satisfying two axioms: (1) and the existence (as a set) of the Cartesian product of any two sets. In Lawvere's foundational set theory, ETCS, one axiom is the existence of products in the category of sets; when applied to global elements, this gives their ordered pair (with the product itself being the Cartesian product), and (1) can be proved. Other structural set theories should contain an axiom similar to Lawvere's axiom of products.

I need to check that I remembered Bourbaki correctly; it varies with the edition. —Toby

Instead, one may construct ordered pairs out of some more basic operation. In a material set theory, one may use Kuratowski's definition

$(a,b) \coloneqq \big\{\,\{a\},\{a,b\}\,\big\} ;$

it is straightforward (using the axiom of extensionality) to prove that (1) holds. Sometimes one sees the alternative

$(a,b) \coloneqq \big\{a, \{a,b\}\,\big\} ;$

but now the axiom of foundation is also needed to prove (1), so the first form is usually preferred. To prove that the cartesian product of two sets is a set, one may use the axiom of separation (bounded separation) is enough to construct $X \times Y$ as a subset of the power set of the power set of the union of $X$ and $Y$, or else use the axiom of replacement (restricted replacement? is enough) to construct it directly, since its elements are indexed by the sets $X$ and $Y$.

In a foundational type theory, ordered pairs are usually also given by fiat, but (1) may not hold, depending on the type theory used. Now Bourbaki's binary operation of pairing becomes a typed operation; given $a$ of type $X$ and $b$ of type $Y$, the ordered pair $(x,y)$ has type $A \times B$. There are also two typed operations (either basic or definable, depending on the style of type theory used) $\pi\colon X \times Y \to X$ and $\rho\colon X \times Y \to Y$, satisfying the beta-rules $\pi(x,y) = x$ and $\rho(x,y) = y$. Then we can either add the eta-rule $z = (\pi z,\rho z)$, which will allow (1) to be proved, or else take (1) as the *definition* of equality on the product type $X \times Y$ (which will then allow the eta-rule to be proved).

… tuples …

… families …

… pairings …

… dependent sums …

Revised on September 5, 2011 16:25:30
by Toby Bartels
(75.88.82.16)