Ordered pair

An ordered pair is a construction satisfying the fundamental property #m/def/set

(𝑎 1, 𝑏 1) = (𝑎 2, 𝑏 2) ⟺ [𝑎 1 = 𝑎 2] \land [𝑏 1 = 𝑏 2]

the set of all ordered pairs from a given pair of sets forms the cartesian product. One may then define an ordered $𝑛$ -tuple by $(𝑎, 𝑏, 𝑐) = ((𝑎, 𝑏), 𝑐)$ , &c. Compare this with the related universal property of the categorical product.

Construction

Kuratowski

Within $Z F$ the typical model, due to Kazimierz Kuratowski, is as follows

(𝑎, 𝑏) = 𝐾 {{𝑎}, {𝑎, 𝑏}}

which satisfies the fundamental property.

Type theory

In a type theory, it is more typical to define ordered pairs directly, so that if $𝑎 : 𝐴$ and $𝑏 : 𝐵$ , we can form $(𝑎, 𝑏) : 𝐴 \times 𝐵$ , and moreover if $𝑝 : 𝐴 \times 𝐵$ , then $p r 1 𝑝 : 𝐴$ and $p r 2 𝑝 : 𝐵$ . The interaction of these rules for introduction and elimination are then subject to further $𝜂$ -unicity and $𝛽$ -computation rules. See product type, or the more general dependent pair.

#state/develop | #lang/en | #SemBr