クワイン–ロッサーの定義
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/05/05 18:06 UTC 版)
J. Barkley Rosser (1953) はウィラード・ヴァン・オーマン・クワインに負うところよる自然数のア・プリオリな定義を必要とする順序対の定義を採用している。N を自然数全体の成す集合とし、函数 φ ( x ) = ( x ∖ N ) ∪ { n + 1 : n ∈ ( x ∩ N ) } {\displaystyle \varphi (x)=(x\smallsetminus \mathbb {N} )\cup \{n+1:n\in (x\cap \mathbb {N} )\}} を定義する。この函数を適用するには、ただ x に属するどの自然数も 1 増やせばいい。とくに、φ(x) は最小の自然数である 0 を含まないので、任意の集合 x, y に対し φ ( x ) ≠ { 0 } ∪ φ ( y ) {\displaystyle \varphi (x)\neq \{0\}\cup \varphi (y)} が成立する。これを用いて順序対 (A, B) を ( A , B ) = { φ ( a ) : a ∈ A } ∪ { φ ( b ) ∪ { 0 } : b ∈ B } {\displaystyle (A,B)=\{\varphi (a):a\in A\}\cup \{\varphi (b)\cup \{0\}:b\in B\}} と定義する。この対から 0 を含まない元をすべて取り出して、φ の適用を取り消せば A が得られる。同様に、0 を含む元を考えれば B を復元することができる。 型理論および公理的集合論 NF のような副産物において、クワイン-ロッサー対は、対とその成分とが同じ型を持つため、「型レベル」("type-level") の順序対と呼ばれる。その意味でこの定義は、順序対として定義される写像が、その引数よりも 1 だけ高い階の型を持つことを許すという点で有利である。この定義は、自然数全体の成す集合が無限集合である場合にのみうまくいく。これは NF ではそうなっているが、型理論や NFU においてはそうではない。ロッサーはそのような型レベルの順序対（あるいは「型が 1 だけ上がる」順序対）の存在性が無限公理を含意することを示した。クワイン集合論の文脈での順序対の広範な議論は Holmes (1998) を参照せよ。
※この「クワイン–ロッサーの定義」の解説は、「順序対」の解説の一部です。
「クワイン–ロッサーの定義」を含む「順序対」の記事については、「順序対」の概要を参照ください。
- クワイン–ロッサーの定義のページへのリンク
