「自由クラス理論」非標準集合論コミュのクワインのＭＬの矛盾

　１．公理　

　ＦＣの上に表現するとＭＬの矛盾が容易く示されます。

　ただ「ラッセルのクラスの矛盾」を解消するのをみて分かるように、ＦＣの上には相当おかしな体系であっても「矛盾なく」表現することが可能です。
　＞「矛盾している」Ｎａｉｖｅな集合論も表現できる　　

　ここでＭＬが「矛盾」しているというのは、いくつかの「まともな」公理を仮定するとＭＬのＯｂｊの定め方が矛盾しているということです。
　　
　すなわち、「まともな」「普通の」公理と両立しない、あるいはＭＬの中ではそれら有用な公理が使えない、ということもできます。　　　　

　＞　まともな公理
　次の三つの公理は、「まとも」で「普通」と思えるでしょう。　　　　　　　　　

　Ａ．¬Ｓｅｔ　　¬Ｓｅｔ　ｘ　∧　｛ｘ｝　ｍａ　ｙ　⇒　¬Ｓｅｔ　ｙ

　「¬Ｓｅｔ」＝「自分を要素とする集まりによって作られる」という性質は、ラッセルのクラスｒや全クラスｕなど「大きい」クラスの持つ性質です。
　ですから、そのような大きなクラス１個からなる集まり｛ｘ｝の作るクラスｙは当然「大きい」と想像できます。　　　　
　また、この公理の対偶をとると、

　Ａ．¬Ｓｅｔ　　　Ｓｅｔ　ｙ　∧　｛ｘ｝　ｍａ　ｙ　⇒　Ｓｅｔ　ｘ

　ＺＦ風に略して言うと、「大きくない」クラスｙの要素ｘは「大きくない」ということを示しています。
　これは前に得られた結果「ＺＦには個体がない」という事実と整合性のある公理です。
　なぜなら、ＺＦのＯｂｊはすべてＳｅｔですが、Ａ．¬Ｓｅｔに反してその要素に¬Ｓｅｔなクラスが存在しうるとすると、それは¬Ｏｂｊとなり、ＣｌではないＯｂｊ＝Ｉｎｄ＝個体が存在しうることになり矛盾。　　　　　　
　
　Ａ．Ｉｎｄ　　Ｉｎｄ　ｘ　∧　｛ｘ｝　ｍａ　ｙ　⇒　Ｓｅｔ_ob　ｙ

　個体ｘ１個を要素とする集まり｛ｘ｝の作るクラスｙはＳｅｔであるということを表現しています。
　たしかにたとえば、りんご1個の集まりの作るクラスは「大きくない」。　　　　　
　そのようなありふれたクラスが「自分を要素とする集まりによって作られる」というおかしな性質を持つべきではないでしょう。
　　　　
　ただし、個体という概念はＯｂｊに対して相対的なものですから、ＳｅｔもＯｂｊに対して相対的なほうのＳｅｔ_obであるべきです。　　　

　Ａ．Ｃｌ　　∀ｘ∀Ｂ　Ｃｌ　ｘ　∧　Ｂ　ｍａ　ｘ　⇒　Ａｔ　Ｂ
　
　Ｃｌの定義はＡｔな集まりによって作られることですが、この公理はＣｌは「Ａｔな集まりだけ」によって作られることを表現しています。

　この３個の公理を仮定すると、ＭＬの矛盾が容易に示せます。


　２．クワインのＭＬ

　クワインのＭＬのＯｂｊはこのように定義されます。

　　　　Ｏｂｊ　ｙ　　Ｄｆ．　∃Ｂ　Ｂ　ｍａ　ｙ　∧　Ｓｔ　Ｂ
　　　　　　　　　　　＊「Ｓｔ」は「Ｓｔｒａｔｉｆｙ」の略

　クラスｙがＯｂｊであるとは、ある層別化された集まりＢによって作られること。

　さらに次のような公理を仮定します。

　　　　Ａ．Ｏｂｊ　　∀ｙ∀Ｂ　Ｂ　ｍａ　ｙ　∧　Ｏｂｊ　ｙ　⇒　Ｓｔ　Ｂ

　Ｏｂｊなクラスを作るのは、層別化された集まりだけという公理です。

　「層別化」の定義は次のとうりです。　　

　　　　Ｓｔ　Ｂ　　Ｄｆ．　Ｂの定義式に現れる全ての「∃Ｃ　ｘ∈Ｃ　∧　Ｃ　ｍａ　ｙ」という形の論理式に対して、ｆ（ｘ）＋１＝ｆ（ｙ）となるように、クラスの変数から整数への関数ｆが定められること

　＞例
　［層別化可能な式］
　（∃Ｃ　ｕ∈Ｃ　∧　Ｃ　ｍａ　ｚ）∧（∃Ｂ　ｚ∈Ｂ　∧　Ｂ　ｍａ　ｘ）∨（∃Ｃ　ｚ∈Ｃ　∧　Ｃ　ｍａ　ｙ）
　　　　　変数　　　　階層
　　　　　ｘ、ｙ　　　２
　　　　　ｚ　　　　　１
　　　　　ｕ　　　　　０
　とすればよい

　［層別化不可能な式］
（∃Ｃ　ｕ∈Ｃ　∧　Ｃ　ｍａ　ｚ）∧（∃Ｂ　ｚ∈Ｂ　∧　Ｂ　ｍａ　ｘ）∧（　∃Ｃ　ｕ∈Ｃ　∧　Ｃ　ｍａ　ｘ）

　∃Ｃ　ｚ∈Ｃ　∧　Ｃ　ｍａ　ｚ
　など


　３．矛盾　

　全集まりＵの定義は

　　　　∀ｘ　ｘ∈Ｕ　⇔　ｘ＝ｘ　　−１−

　この集まりＵが全クラスｕを作ります。

　　　　Ｕ　ｍａ　ｕ
　　　　
　　　　１式は層別化されているので

　　　　Ｓｔ　Ｕ
　　　　
　　　　ゆえに

　　　　Ｏｂｊ　ｕ

　　　　ＵにはＯｂｊではないクラスも要素として存在する
　　　　ゆえに

　　　　¬Ａｔ　Ｕ　　　　　
　　　　¬Ｃｌ　ｕ 　　　　［Ａ．Ｃｌ］

　　　　ゆえに

　　　　Ｉｎｄ　ｕ
　　　　Ｓｅｔ_ob　ｕ’　　［Ａ．Ｉｎｄ］　　−２−

　　　　ただし　｛ｕ｝ｍａ　ｕ’

　　　　Ａｔ　｛ｕ」
　　　　Ｃｌ　ｕ’
　一方
　　　　¬Ｓｅｔ　ｕ
　　　　¬Ｓｅｔ　ｕ’　　　［Ａ．¬Ｓｅｔ］　　−３−

　　　　２．３．式より　　

　　　　∃Ｂ　ｕ’∈Ｂ　∧　Ｂ　ｍａ　ｕ’　∧　¬Ａｔ　Ｂ
　　　　¬Ｃｌ　ｕ’　　　　［Ａ．Ｃｌ］　

　　　　矛盾