Editing Ordered pair (section)

===Kuratowski's definition===
In 1921 [[Kazimierz Kuratowski]] offered the now-accepted definition<ref>cf introduction to Wiener's paper in van Heijenoort 1967:224. van Heijenoort observes that the resulting set that represents the ordered pair "has a type higher by 2 than the elements (when they are of the same type)"; he offers references that show how, under certain circumstances, the type can be reduced to 1 or 0.</ref><ref>{{cite journal | title=Sur la notion de l'ordre dans la Théorie des Ensembles | first=Casimir|last=Kuratowski| author-link=Kazimierz Kuratowski| year=1921| journal=[[Fundamenta Mathematicae]] | pages=161–171| volume=2 | number=1 | doi=10.4064/fm-2-1-161-171|doi-access = free}}</ref>
of the ordered pair (''a'', ''b''):
<math display="block">(a, \ b)_K \; := \  \{ \{ a \}, \ \{ a, \ b \} \}.</math>
When the first and the second coordinates are identical, the definition obtains:
<math display="block">(x,\ x)_K = \{\{x\},\{x, \ x\}\} = \{\{x\},\ \{x\}\} = \{\{x\}\}</math>

Given some ordered pair ''p'', the property "''x'' is the first coordinate of ''p''" can be formulated as:
<math display="block">\forall Y\in p:x\in Y.</math>
The property "''x'' is the second coordinate of ''p''" can be formulated as:
<math display="block">(\exist Y\in p:x\in Y) \land(\forall Y_1,Y_2\in p: (x \in Y_1 \land x \in Y_2) \rarr Y_1 = Y_2).</math>
In the case that the left and right coordinates are identical, the right [[Logical conjunction|conjunct]] <math>(\forall Y_1,Y_2\in p: (x \in Y_1 \land x \in Y_2) \rarr Y_1 = Y_2)</math> is trivially true, since <math>Y_1 = Y_2</math> is the case.

If <math>p=(x,y)=\{\{x\},\{x,y\}\}</math> then:
: <math>\bigcap p = \bigcap \bigg\{\{x\}, \{x, y\}\bigg\} = \{x\} \cap \{x, y\} = \{x\},</math>
: <math>\bigcup p = \bigcup \bigg\{\{x\}, \{x, y\}\bigg\} = \{x\} \cup \{x, y\} = \{x, y\}.</math>

This is how we can extract the first coordinate of a pair (using the [[Iterated binary operation#Notation|iterated-operation notation]] for [[Intersection (set theory)#Arbitrary intersections|arbitrary intersection]] and [[Union (set theory)#Arbitrary unions|arbitrary union]]):
<math display="block">\pi_1(p) = \bigcup\bigcap p = \bigcup \{x\} = x.</math>

This is how the second coordinate can be extracted:
<math display="block">\pi_2(p) = \bigcup\left\{\left. a \in \bigcup p\,\right|\,\bigcup p \neq \bigcap p \rarr a \notin \bigcap p \right\} = \bigcup\left\{\left. a \in \{x,y\}\,\right|\,\{x,y\} \neq \{x\} \rarr a \notin \{x\} \right\} = \bigcup \{y\} = y.</math>

(if <math>x \neq y</math>, then the set <math>\{y\}</math> could be obtained more simply: <math>\{y\}=\{\left. a \in \{x,y\}\,\right|\, a \notin \{x\}  \}</math>, but the previous formula also takes into account the case when <math>x=y</math>.)

Note that <math>\pi_1</math> and <math>\pi_2</math> are [[Function (mathematics)#In the foundations of mathematics|generalized functions]], in the sense that their domains and codomains are [[proper classes]].

====Variants====
The above Kuratowski definition of the ordered pair is "adequate" in that it satisfies the characteristic property that an ordered pair must satisfy, namely that <math>(a,b) = (x,y) \leftrightarrow (a=x) \land (b=y)</math>. In particular, it adequately expresses 'order', in that <math>(a,b) = (b,a)</math> is false unless <math>b = a</math>. There are other definitions, of similar or lesser complexity, that are equally  adequate:
* <math>( a, b )_{\text{reverse}} :=  \{ \{ b \}, \{a, b\}\};</math>
* <math>( a, b )_{\text{short}} :=  \{ a, \{a, b\}\};</math>
* <math>( a, b )_{\text{01}} := \{\{0, a \}, \{1, b \}\}.</math><ref>This differs from Hausdorff's definition in not requiring the two elements 0 and 1 to be distinct from ''a'' and ''b''.</ref>
The '''reverse''' definition is merely a trivial variant of the Kuratowski definition, and as such is of no independent interest. The definition '''short''' is so-called because it requires two rather than three pairs of [[braces (punctuation)|braces]]. Proving that '''short''' satisfies the characteristic property requires the [[Zermelo–Fraenkel set theory]] [[axiom of regularity]].<ref>Tourlakis, George (2003) ''Lectures in Logic and Set Theory. Vol. 2: Set Theory''. Cambridge Univ. Press. Proposition III.10.1.</ref> Moreover, if one uses [[Set-theoretic definition of natural numbers#Definition as von Neumann ordinals|von Neumann's set-theoretic construction of the natural numbers]], then 2 is defined as the set {0, 1} = {0, {0}}, which is indistinguishable from the pair (0, 0)<sub>short</sub>. Yet another disadvantage of the '''short''' pair is the fact that, even if ''a'' and ''b'' are of the same type, the elements of the '''short''' pair are not. (However, if ''a''&nbsp;=&nbsp;''b'' then the '''short''' version keeps having cardinality 2, which is something one might expect of any "pair", including any "ordered pair".)

====Proving that definitions satisfy the characteristic property====
Prove: (''a'', ''b'') = (''c'', ''d'') [[if and only if]] ''a'' = ''c'' and ''b'' = ''d''.

'''Kuratowski''':<br>
''If''. If ''a'' = ''c'' and ''b'' = ''d'', then {{''a''}, {''a'', ''b''}} = {{''c''}, {''c'', ''d''}}. Thus (''a, b'')<sub>K</sub> = (''c'', ''d'')<sub>K</sub>.

''Only if''. Two cases: ''a'' = ''b'', and ''a'' ≠ ''b''.

If ''a'' = ''b'':
:(''a, b'')<sub>K</sub> = {{''a''}, {''a'', ''b''}}  = {{''a''}, {''a'', ''a''}} = <nowiki>{{</nowiki>''a''}}.
:{{''c''}, {''c'', ''d''}} = (''c'', ''d'')<sub>K</sub> = (''a'', ''b'')<sub>K</sub> = <nowiki>{{</nowiki>''a''}}.
:Thus {''c''} = {''c'', ''d''} = {''a''}, which implies ''a'' = ''c'' and ''a'' = ''d''. By hypothesis, ''a'' = ''b''. Hence ''b'' = ''d''.

If ''a'' ≠ ''b'', then (''a'', ''b'')<sub>K</sub> = (''c'', ''d'')<sub>K</sub> implies {{''a''}, {''a'', ''b''}} = {{''c''}, {''c'', ''d''}}.

:Suppose {''c'', ''d''} = {''a''}. Then ''c'' = ''d'' = ''a'', and so {{''c''}, {''c'', ''d''}} = {{''a''}, {''a'', ''a''}} = {{''a''}, {''a''}} = <nowiki>{{</nowiki>''a''}}. But then {{''a''}, {''a, b''}} would also equal <nowiki>{{</nowiki>''a''}}, so that ''b'' = ''a'' which contradicts ''a'' ≠ ''b''.

:Suppose {''c''} = {''a'', ''b''}. Then ''a'' = ''b'' = ''c'', which also contradicts ''a'' ≠ ''b''.

:Therefore {''c''} = {''a''}, so that ''c = a'' and {''c'', ''d''} = {''a'', ''b''}.

:If ''d'' = ''a'' were true, then {''c'', ''d''} = {''a'', ''a''} = {''a''} ≠ {''a'', ''b''}, a contradiction. Thus ''d'' = ''b'' is the case, so that ''a'' = ''c'' and ''b'' = ''d''.

'''Reverse''':<br>
(''a, b'')<sub>reverse</sub> = {{''b''}, {''a, b''}} = {{''b''}, {''b, a''}} = (''b, a'')<sub>K</sub>.

''If''. If (''a, b'')<sub>reverse</sub> = (''c, d'')<sub>reverse</sub>,
(''b, a'')<sub>K</sub> = (''d, c'')<sub>K</sub>. Therefore, ''b = d'' and ''a = c''.

''Only if''. If ''a = c'' and ''b = d'', then {{''b''}, {''a, b''}} = {{''d''}, {''c, d''}}.
Thus (''a, b'')<sub>reverse</sub> = (''c, d'')<sub>reverse</sub>.

'''Short:'''<ref>For a formal [[Metamath]] proof of the adequacy of '''short''', see [http://us.metamath.org/mpegif/opthreg.html here (opthreg).] Also see Tourlakis (2003), Proposition III.10.1.</ref>

''If'': If ''a = c'' and ''b = d'', then {''a'', {''a, b''}} = {''c'', {''c, d''}}. Thus (''a, b'')<sub>short</sub> = (''c, d'')<sub>short</sub>.

''Only if'': Suppose {''a'', {''a, b''}} = {''c'', {''c, d''}}.
Then ''a'' is in the left hand side, and thus in the right hand side.
Because equal sets have equal elements, one of ''a = c'' or ''a'' = {''c, d''} must be the case.
:If ''a'' = {''c, d''}, then by similar reasoning as above, {''a, b''} is in the right hand side, so {''a, b''} = ''c'' or {''a, b''} = {''c, d''}.
::If {''a, b''} = ''c'' then ''c'' is in {''c, d''} = ''a'' and ''a'' is in ''c'', and this combination contradicts the axiom of regularity, as {''a, c''} has no minimal element under the relation "element of."
::If {''a, b''} = {''c, d''}, then ''a'' is an element of ''a'', from ''a'' = {''c, d''} = {''a, b''}, again contradicting regularity.
:Hence ''a = c'' must hold.

Again, we see that {''a, b''} = ''c'' or {''a, b''} = {''c, d''}.
:The option {''a, b''} = ''c'' and ''a = c'' implies that ''c'' is an element of ''c'', contradicting regularity.
:So we have ''a = c'' and {''a, b''} = {''c, d''}, and so: {''b''} = {''a, b''} \ {''a''} = {''c, d''} \ {''c''} = {''d''}, so ''b'' = ''d''.