Given any things and , the ordered pair of and is a thing, usually written , sometimes or . The important property is
The things and are called the components of the ordered pair . Given any two sets and , their Cartesian product is a set whose elements are precisely the ordered pairs whose components are respectively elements of and elements of .
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, 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
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 as a subset of the power set of the power set of the union of and , or else use the axiom of replacement (restricted replacement? is enough) to construct it directly, since its elements are indexed by the sets and .
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 of type and of type , the ordered pair has type . There are also two typed operations (either basic or definable, depending on the style of type theory used) and , satisfying the beta-rules and . Then we can either add the eta-rule , which will allow (1) to be proved, or else take (1) as the definition of equality on the product type (which will then allow the eta-rule to be proved).