順序対

B math 順序対

順序対の定義として
0. = {{x}, {x, y}}
1. = {x, {x, y}}
の二つがあるように思われるが
1の定義をするとよろしくないことが起きる気がする。

というのも1では正則性公理なしに
= -> a = a' & b = b'
の証明が出来ないように思われるから。そうすると、正則性公理の相対的無矛盾性を示す際に嵌められたり、BG公理系では類の中の順序対の値域が類になるという公理が悲鳴を上げたりする気がする。

Th.
\Large \{x, \{x, y\}\} = \{x', \{x', y'\}\} \wedge x \not = x' \quad \Rightarrow \quad \bot
Prf.
\Large x \in \{x', \{x', y'\}\}
\Large x \not = x' ならば
\Large x = \{x', y'\}となる。(0)

\Large x = \{x, y\}ならば、\Large \{x, \{x, y\}\}が正則性公理に違反するので \Large x \not = \{x, y\}
同様に \Large x' \not = \{x', y'\}
(0)とここから
\Large \{x, y\} \in \{x', \{x', y'\}\}を使って、\Large x' = \{x, y\} (1)

\Large \{x, x'\} を考えると(0) (1) からこれが正則性公理に反していることが分かる。
Q.E.D.

1 の定義も何度か見たことがある気がするから、1 の方がブルバキあたりの古い流儀で、0 の方がこれじゃまずいことがあると決められた新興な流儀なのかな。