「自由クラス理論」非標準集合論コミュのクラス論の分類

　［　クラス理論の分類　］


　１．　準備

　クラス理論をＯｂｊとＳｅｔの関係のあり方によって、４つのＴｙｐｅに分類します。

　まず始めによく使われる公理や集まりについて解説します。

　Ａ．Ａｔ　　¬Ａｔ　Ｂ　⇒　（∀　ｂ　ｂ∈Ｂ　⇒　¬Ｏｂｊ　ｂ）
　　　　「¬Ａｔ」とはＯｂｊではない要素が存在することですが、この公理はＯｂｊと¬Ｏｂｊな要素が混在することはないことを言っています。
　　　　要素の「純粋性」の公理です。　　　　

　Ａ．Ｃｌ　　Ｃｌ　ｋ　⇒　（∀Ｂ　Ｂ　ｍａ　ｋ　⇒　Ａｔ　Ｂ）
　　　　「Ｃｌ」なクラスはＡｔな集まりだけから作られる。
　　　　集まりの「純粋性」の公理です。　　　　

　Ａ．｛　｝　　¬Ｓｅｔ　ｙ　∧　｛ｙ｝　ｍａ　ｋ　⇒　¬Ｓｅｔ　ｋ　
　　　　「¬Ｓｅｔ」は全クラスｕやラッセルのクラスｒが持っている性質ですから、「大きい」というニュアンスがあると考えてよいでしょう。
　　　　「大きい」クラス１個を要素とする集まりの作るクラスは「大きい」という公理。　　　　

　　　　Ｒ　　Ｄｆ．　　∀ｂ　ｂ∈Ｒ　⇔　Ｓｅｔ　ｂ
　　　　　　　　　　　　自分を要素としないクラス全ての集まり

　　　　Ｕ　　Ｄｆ．　　∀ｂ　ｂ∈Ｕ　⇔　Ｏｂｊ　ｂ
　　　　　　　　　　　　理論の対象となるクラス全ての集まり

　　　　ｒ　　Ｄｆ．　　Ｒ　ｍａ　ｒ
　　　　　　　　　　　　Ｒの作るクラス

　　　　ｕ　　Ｄｆ．　　Ｕ　ｍａ　ｕ
　　　　　　　　　　　　Ｕの作るクラス

　普通は集まりを表す定数には、「Ｒ_0」、「Ｕ_1」など添え字のついた文字を使いますが、間違うおそれのない場合は添え字なしの「Ｒ」、「Ｕ」などを使います。

　　　　Ｓｅｔ　ｂ　　Ｄｆ．　　¬（∃Ｂ　ｂ∈Ｂ　∧　Ｂ　ｍａ　ｂ）
　　　　「自分を要素としない」というのは大抵のクラスの持つ性質ですから、「Ｓｅｔ」＝「普通の」という感じです。　　　
　　　　正確に書くと「自分を要素としない集まりに作られない」となります。

　　　　Ｓｅｔ_ob　ｂ　　Ｄｆ．　　¬（∃Ｂ　Ａｔ　Ｂ　∧　ｂ∈Ｂ　∧　Ｂ　ｍａ　ｂ）
　　　　Ｏｂｊに対して相対的なＳｅｔのことです。
　　　　Ｏｂｊが定義されていなければ定まりません。
　　　　とうぜん次の定理がなりたちます。

　　　　Ｔ．Ｓｅｔ_ob　　∀ｂ　Ｓｅｔ　ｂ　⇒　Ｓｅｔ_ob　ｂ　

　　　　Ｒ_ob　　Ｄｆ．　　∀ｂ　ｂ∈Ｒ_ob　⇔　Ｓｅｔ_ob　ｂ
　　　　　　　　　自分を要素とするＡｔな集まりに作られないクラス全ての集まり
　


　２．　分類

　［　Type.1　］
　　　　Ｕ　⊂　Ｒ
　　　　∀ｘ　Ｏｂｊ　ｘ　⇒　Ｓｅｔ　ｘ　
　
　　　　
　［　Type.1　］
　　　　Ｕ　⊂　Ｒ
　　　　∀ｘ　Ｏｂｊ　ｘ　⇒　Ｓｅｔ　ｘ　

　［　Type.２　］
　　　　Ｒ　⊂　Ｕ
　　　　∀ｘ　Ｓｅｔ　ｘ　⇒　Ｏｂｊ　ｘ　

　［　Type.３　］
　　　　¬（Ｕ　⊂　Ｒ）　∧　¬（Ｒ　⊂　Ｕ）　∧　¬（Ｕ　∩　Ｒ　＝φ）　
　　　　（∃ｘ　Ｏｂｊ　ｘ　∧　¬Ｓｅｔ　ｘ）　∧　（∃ｙ　Ｓｅｔ　ｙ　∧　¬Ｏｂｊ　ｙ）　∧　（∃ｂ　Ｏｂｊ　ｂ　∧　Ｓｅｔ　ｂ）

　［　Type.４　］
　　　　¬（Ｕ　⊂　Ｒ）　∧　¬（Ｒ　⊂　Ｕ）　∧　　（Ｕ　∩　Ｒ　＝φ）　
　　　　（∃ｘ　Ｏｂｊ　ｘ　∧　¬Ｓｅｔ　ｘ）　∧　（∃ｙ　Ｓｅｔ　ｙ　∧　¬Ｏｂｊ　ｙ）　∧　¬（∃ｂ　Ｏｂｊ　ｂ　∧　Ｓｅｔ　ｂ）
　
　Ｔｙｐｅ．１とＴｙｐｅ．２はＵとＲの関係が反対です。
　Ｔｙｐｅ．３はＴｙｐｅ１．Ｔｙｐｅ．２のどちらでもなく、ＵとＲの重なりがある。
　Ｔｙｐｅ．４はＴｙｐｅ１．Ｔｙｐｅ．２のどちらでもなく、ＵとＲの重なりがない。

　「⊂」に「＝」がありません。
　なぜなら、Ｕ＝Ｒとすると矛盾が起こります。　　　　　　
　　　　∀ｂ　Ｏｂｊ　ｂ　⇔　Ｓｅｔ　ｂ　と仮定します
　　　　Ｕ　ｍａ　ｕ　とすると　Ａｔ　Ｕ　ゆえに
　　　　Ｃｌ　ｕ　　　　−＊
　　　　一方
　　　　Ｒ　ｍａ　ｒ　とすると　¬Ｓｅｔ　ｒ　、　ｕ＝ｒ　ゆえに
　　　　¬Ｓｅｔ　ｕ　仮定より　¬Ｏｂｊ　ｕ
　　　　また　∃Ｂ　ｕ∈Ｂ　∧　Ｂ　ｍａ　ｕ　だから
　　　　¬Ａｔ　Ｂ
　　　　［Ａｔ．Ｃｌ］と＊式から　　
　　　　　Ａｔ　Ｂ
　　　　矛盾
　　　　


　３．　定理

　それぞれの型のクラス理論がどのような性質を持っているかの定理を示します。

　Ｔｙｐｅ．１の定理

　Ｔ．１−１　　¬Ｏｂｊ　ｕ　
　Ｔ．１−２　　Ｓｅｔ　ｕ　　［Ａ．Ｃｌ］
　Ｔ．１−３　　∀ｂ　Ｐｒｃｌ　ｂ　⇒　Ｓｅｔ　ｂ
　Ｔ．１−４　　∃ｋ　Ｉｎｄ　ｋ
　　　　　　　　個体が存在しうる。
　　　　Ａ．Ｐａｉｒ　があるとする
　　　　Ｓｅｔ　ｕ　ゆえに
　　　　｛ｕ｝　ｍａ　ｋ　なら
　　　　Ｓｅｔ　ｋ
　　　　クラスｋはＳｅｔであるから、Ｏｂｊであるとしても矛盾はない　　　
　　　　Ｏｂｊ　ｋ　　　　−＊−
　　　　なお、Ｔ．１−１　　
　　　　¬Ｏｂｊ　ｕ　ゆえに
　　　　¬Ａｔ　｛ｕ｝　ゆえに
　　　　¬Ｃｌ　ｋ　　［Ａ．Ｃｌ］
　　　　＊式とあわせて
　　　　Ｉｎｄ　ｋ
　　　　全クラスｕ１個を要素とする集まり｛ｕ｝の作るクラスｋは個体でありえます

　Ｔ．１−５　　∀ｙ　Ｓｅｔ_ob

　この型のクラス理論のなかでは、ＩｎｄもＯｂｃｌもＰｒｃｌも皆Ｓｅｔです。
　たとえば、¬Ｓｅｔであるクラスｒなどは、この理論と関係のない存在です。

　Ｔｙｐｅ．１のクラス理論の例

　ＺＦはこの型に属します。
　Ａ．ＲｅｇはＴｙｐｅ．１の条件そのものです。

　Ｔｙｐｅ．２の定理

　Ｔ．２−１　　∀ｙ　¬Ｓｅｔ_ob　ｙ　⇒　Obj　ｙ　　−Ｒ_ob　⊂　Ｕ
　Ｔ．２−２　　¬Ｓｅｔ_ob　ｒ　　
　Ｔ．２−３　　¬Ｓｅｔ_ob　–ｒ_ob
　Ｔ．２−４　　¬∃ｙ　Ｉｎｄ　ｙ　　　　　［Ａ．｛　｝］
　Ｔ．２−５　　¬∃ｙ　Ｐｒｃｌ　ｙ　　　　［Ａ．Ｃｌ］　　　

　Ｔｙｐｅ．２のクラス理論の例

　ＦＣ自体がこの型に属します。
　全てのクラスがＯｂｊであると定義すれば、「ＦＣ」のＦＣの上への表現になりますが、当然　Ｒ　⊂　Ｕ　となります。
　　　　Ｏｂｊ　ｙ　　Ｄｆ．　　ｙ＝ｙ
　ＦＣでは全てのクラスが要素となり、クラスは皆集まりから作られるのですから、個体やプロパークラスが存在しないという定理も当然のことです。　　　　

　Ｔｙｐｅ．３の定理

　Ｔ．３−０　　　Ｓｅｔ_ob　ｒ　　　　　　　　　　　　　　［Ａ．Ｃｌ］
　Ｔ．３−１　　¬Ｓｅｔ　ｕ　∧　Ｏｂｊ　ｕ　　　　　　　　［Ａ．Ｃｌ］　［Ａ．Ａｔ］　［A.｛　｝］
　Ｔ．３−２　　¬Ｓｅｔ_ob　u　　　　　　　　　　　　　　　［Ａ．Ｃｌ］　［Ａ．Ａｔ］　［A.｛　｝］
　Ｔ．３−３　　¬Ｓｅｔ　ｒ_ob　∧　Ｓｅｔ_ｏｂ　ｒ_ob　　［Ａ．Ｃｌ］　［A.｛　｝］
　Ｔ．３−４　　¬Ｓｅｔ　−ｒ　∧　Ｓｅｔ_ｏｂ　−ｒ　　　［Ａ．Ｃｌ］　［A.｛　｝］
　Ｔ．３−５　　¬Ｓｅｔ　−ｕ　∧　¬Ｏｂｊ　−ｕ　　　　［Ａ．Ｃｌ］　［Ａ．Ａｔ］　［A.｛　｝］
　Ｔ．３−６　　¬Ｓｅｔ_ob　−ｒ_ob　　　　　　　　　　　［Ａ．Ｃｌ］　［A.｛　｝］
　Ｔ．３−７　　∀ｙ　Ｐｒｃｌ　ｙ　⇒　Ｓｅｔ　ｙ　　　　［Ａ．Ｃｌ］
　Ｔ．３−８　　∀ｙ　Ｉｎｄ　ｙ　⇒　Ｓｅｔ　ｙ　　　　　［Ａ．Ａｔ］

　Ｔｙｐｅ．３のクラス理論の例

　クワインのＭＬがこの型の例です。

　このような集まりＮとクラスｎを考えます。
　　　　∀ｂ　ｂ∈Ｎ　⇔　ｂ＝ｍ　∧　Ｓｅｔ　ｍ　，　Ｎ　ｍａ　ｎ
　Ｎの条件の論理式の中の「Ｓｅｔ　ｍ」は層別化不可能ですから、¬Ｏｂｊ　ｎ
　また、Ａ．ＰａｉｒからＳｅｔ　ｎ
　ゆえに、
　　　　Ｓｅｔ　ｎ　∧　¬Ｏｂｊ　ｎ　　−＊１−

　また、全集まりＵは層別化可能ゆえに　Ｏｂｊ　ｕ
　Ｓｅｔの公理Ａ．⊂より、¬Ｓｅｔ　ｕ
　ゆえに、
　　　¬Ｓｅｔ　ｕ　∧　Ｏｂｊ　ｕ　　−＊２−

　また、
　　　Ｓｅｔ　０　∧　Ｏｂｊ　０　　−＊３−
　　　ただし、φ　ｍａ　０
　＊１、＊２、＊３式はＴｙｐｅ．３の条件です。

　Ｔｙｐｅ．４の定理

　Ｔ．４−１　　∀ｙ　¬Ｓｅｔ_ob　ｙ　⇒　Ｏｂｊ　y　
　Ｔ．４−２　　¬Ｏｂｊ　ｒ　　　　　　［Ａ．Ｃｌ］
　Ｔ．４−３　　¬Ｓｅｔ_ob　u　　　　　［Ａ．Ｃｌ］　［Ａ．｛　｝］
　Ｔ．４−４　　¬Ｓｅｔ_ob　−ｒ_ob　　［Ａ．Ｃｌ］　［Ａ．｛　｝］
　Ｔ．４−５　　¬Ｓｅｔ　−ｒ　∧　Ｓｅｔ_ob　−ｒ　　［Ａ．Ｃｌ］　［Ａ．｛　｝］
　Ｔ．４−６　　¬Ｓｅｔ　−ｕ　∧　¬Ｏｂｊ　−ｕ　　［Ａ．Ｃｌ］　［Ａ．Ａｔ］　［Ａ．｛　｝］
　Ｔ．４−７　　¬Ｓｅｔ　ｒ_ob　∧　¬Ｏｂｊ　ｒ_ob　　［Ａ．Ｃｌ］　［Ａ．Ａｔ］　［Ａ．｛　｝］
　Ｔ．４−８　　∀ｙ　¬Ｐｒｃｌ　ｙ　　［Ａ．Ｃｌ］　［Ａ．｛　｝］
　Ｔ．４−９　　∀ｙ　¬Ｉｎｄ　ｙ　　　［Ａ．Ｃｌ］

　Ｔｙｐｅ．４のクラス理論の例は、知られているクラス理論には存在しません。