「自由クラス理論」非標準集合論コミュのFree Class Theory 4

[ Classification of Class Theory ]
1.Preparation

We classify Class Theories into four types by the reationship between Obj and Set.
First of all, I explain the axiom and the Atsumari which are often used

　Ａ．Ａｔ　　¬Ａｔ　Ｂ　⇒　（∀　ｂ　ｂ∈Ｂ　⇒　¬Ｏｂｊ　ｂ）

"¬At" means that an element which is not Obj exists,So this axiom says that Obj and ¬Obj are not mixed. It is Axiom of "Pureness" of element

　Ａ．Ｃｌ　　Ｃｌ　ｋ　⇒　（∀Ｂ　Ｂ　ｍａ　ｋ　⇒　Ａｔ　Ｂ）

"Cl"-Class is made only by "At"-Atsumari. It is Axiom of "Pureness" of Atsumari.

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

"¬Set" is a property which universal cllass u or Russel's class r have, so it means "Large". The axiom says that a Class which an Atsumari having one large Class makes is large

　　　　Ｒ　　Ｄｆ．　　∀ｂ　ｂ∈Ｒ　⇔　Ｓｅｔ　ｂ
　　　　　　　　　　　　Atsumari of Classes which don't have itself

　　　　Ｕ　　Ｄｆ．　　∀ｂ　ｂ∈Ｕ　⇔　Ｏｂｊ　ｂ
　　　　　　　　　　　　Atsumari of Classes which are object of the Class Theory

　　　　ｒ　　Ｄｆ．　　Ｒ　ｍａ　ｒ
　　　　　　　　　　　　Class which R makes

　　　　ｕ　　Ｄｆ．　　Ｕ　ｍａ　ｕ
　　　　　　　　　　　　Class which U makes

　Ordinary we use characters with suffix like "R_0" or "U_1" for constant of Atsumari, but if we don't mistake then we use characters without suffix like "R" or "U"

　　　　Ｓｅｔ　ｂ　　Ｄｆ．　　¬（∃Ｂ　ｂ∈Ｂ　∧　Ｂ　ｍａ　ｂ）

　　　　Normal Classes have the property "Non self membership" so "Set" means "Normal"

　　　　Ｓｅｔ_ob　ｂ　　Ｄｆ．　　¬（∃Ｂ　Ａｔ　Ｂ　∧　ｂ∈Ｂ　∧　Ｂ　ｍａ　ｂ）

　　　　Relatively Set based on Obj
　　　　Obj must be defined

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


　　　　Ｒ_ob　　Ｄｆ．　　∀ｂ　ｂ∈Ｒ_ob　⇔　Ｓｅｔ_ob　ｂ

　　　　The Atsumari of Classes which are not made by the At-Atsumari which has itself as a member


2. Classification
［　Type.1　］

　　　　Ｕ　⊂　Ｒ

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

　　　　Ｒ　⊂　Ｕ

　　　　∀ｘ　Ｓｅｔ　ｘ　⇒　Ｏｂｊ　ｘ　

［　Type.３　］

　　　　¬（Ｕ　⊂　Ｒ）　∧　¬（Ｒ　⊂　Ｕ）　∧　¬（Ｕ　∩　Ｒ　＝φ）　

　　　　（∃ｘ　Ｏｂｊ　ｘ　∧　¬Ｓｅｔ　ｘ）　∧　（∃ｙ　Ｓｅｔ　ｙ　∧　¬
Ｏｂｊ　ｙ）　∧　（∃ｂ　Ｏｂｊ　ｂ　∧　Ｓｅｔ　ｂ）


［　Type.４　］

　　　　¬（Ｕ　⊂　Ｒ）　∧　¬（Ｒ　⊂　Ｕ）　∧　　（Ｕ　∩　Ｒ　＝φ）　

　　　　（∃ｘ　Ｏｂｊ　ｘ　∧　¬Ｓｅｔ　ｘ）　∧　（∃ｙ　Ｓｅｔ　ｙ　∧　¬Ｏｂｊ　ｙ）　∧　¬（∃ｂ　Ｏｂｊ　ｂ　∧　Ｓｅｔ　ｂ）
　
The relationship of U and R of Type.1 and Type.2 is opposite
Type.3 is neither Type.1 nor Type .2 and U and R are overapped
Type.4 is neither Type.1 nor Type.2 and U and R are not overapped

"⊂" don't contain "="
Because if U=R is assumed then it becomes contradiction　　　　　　
If the following formula is assumed

　　　　∀ｂ　Ｏｂｊ　ｂ　⇔　Ｓｅｔ　ｂ

　　　　Ｕ　ｍａ　ｕ　and 　Ａｔ　Ｕ　Hence
　　　　Ｃｌ　ｕ　　　　−＊
The other hand
　　　　Ｒ　ｍａ　ｒ　and 　¬Ｓｅｔ　ｒ　、　ｕ＝ｒ　Hence
　　　　¬Ｓｅｔ　ｕ　From assumption　¬Ｏｂｊ　ｕ　
　　　　Also　∃Ｂ　ｕ∈Ｂ　∧　Ｂ　ｍａ　ｕ　Hence
　　　　¬Ａｔ　Ｂ
From Axiom "A.Cl" and the formula "*"
　　　　　Ａｔ　Ｂ
　　　 Contradiction