対の公理(Pairing)

対の公理
\forall a \forall b \exists c \forall x(x \in c \leftrightarrow x=a \vee x=b)



任意の集合 a,b に対し, 要素が a であるか b であるかのいずれかであるような集合 c が存在すると言ってます.
外延性の公理から, そのような集合は一意に定まり, これを \{a,b\} と書くことにします.
ちなみに \{a,a\} なる集合は, 単に \{a\} と書き, これを単集合(singleton)と言います.
\{a,b\}=\{b,a\} ですが, a,b の順序も考慮した集合があると便利です.
そこで, 順序対(ordered pair) (a,b)
(a,b)=\{\{a\},\{a,b\}\}
で定義します.
すると上手いように
(a,b)=(c,d) \leftrightarrow (a=c) \wedge (b=d)
が成り立つことが確認できます.
ちなみに, このような原理を満たすようであれば, 順序対はどのように定義しても差し支えありません.
三つ以上の組についても同様に定義できます.