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

3. Theorem

Theorem for the properties which Class Theory of each type has.


[ Theorem of Type.1 ]

　Ｔ．１−１　　¬Ｏｂｊ　ｕ　
　Ｔ．１−２　　Ｓｅｔ　ｕ　　［Ａ．Ｃｌ］
　Ｔ．１−３　　∀ｂ　Ｐｒｃｌ　ｂ　⇒　Ｓｅｔ　ｂ
　Ｔ．１−４　　∃ｋ　Ｉｎｄ　ｋ

　　　　Individual is able to exist.
　　　　Ａ．Ｐａｉｒ　 　We ashume this Axiom
　　　　Ｓｅｔ　ｕ Hence
　　　　｛ｕ｝　ｍａ　ｋ　 So
　　　　Ｓｅｔ　ｋ
　　　　Class k is Set, so it is possible to assume k is Obj
　　　　Ｏｂｊ　ｋ　　　　−＊−
　　　　From Ｔ．１−１　　
　　　　¬Ｏｂｊ　ｕ Hence
　　　　¬Ａｔ　｛ｕ｝ Hence
　　　　¬Ｃｌ　ｋ　　［Ａ．Ｃｌ］
　　　　 From *
　　　　Ｉｎｄ　ｋ

　　　　Where Class k which Atsumari {u} whose member is Universal class u
makes is able to be Individual

[ A.*** ] means the Axiom *** is asumed

　Ｔ．１−５　　∀ｙ　Ｓｅｔ_ob



In Class Theory of this type, Ind and Obcl and Prcl are all Set.
For example, Class r which is ¬Set has no relationship with it

Example of Class Theory of Type.1
ZF belongs to this type.

A.Reg arrives at the condition of Type.1


[ Theorem oof Type.2 ]

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


Example of Class Theory of Type.2
FC belongs in this Type.

If we defined that all Classes are Obj then it becomes a representation of "FC" on FC. Naturally　Ｒ⊂Ｕ

　　　　Ｏｂｊ　ｙ　　Ｄｆ．　　ｙ＝ｙ

In FC, all Classes are elements and all Classes are made by Atsumari so neither Indiviual nor Proper Class exist.


[ Theorem of Type.3 ]

　Ｔ．３−０　　　Ｓｅｔ_ob　ｒ　　　　　　　　　　　　　 　［Ａ．Ｃｌ］

　Ｔ．３−１　　¬Ｓｅｔ　ｕ　∧　Ｏｂｊ　ｕ　　　　　　　　［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．Ａｔ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ.｛　｝］

　Ｔ．３−２　　¬Ｓｅｔ_ob　u　　　　　　　　　　　　　　　［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．Ａｔ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ｛　｝］

　Ｔ．３−３　　¬Ｓｅｔ　ｒ_ob　∧　Ｓｅｔ_ｏｂ　ｒ_ob　　 ［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．｛　｝］


　Ｔ．３−４　　¬Ｓｅｔ　−ｒ　∧　Ｓｅｔ_ｏｂ　−ｒ　　　 ［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．｛　｝］


　Ｔ．３−５　　¬Ｓｅｔ　−ｕ　∧　¬Ｏｂｊ　−ｕ　　　　［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．Ａｔ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．｛　｝｝

　Ｔ．３−６　　¬Ｓｅｔ_ob　−ｒ_ob　　　　　　　　　　　［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．｛　｝］

　Ｔ．３−７　　∀ｙ　Ｐｒｃｌ　ｙ　⇒　Ｓｅｔ　ｙ　　　　［Ａ．Ｃｌ］

　Ｔ．３−８　　∀ｙ　Ｉｎｄ　ｙ　⇒　Ｓｅｔ　ｙ　　　　　［Ａ．Ａｔ］


Example of Class Theory of Type.3

Quine's ML is an example of this Type.

We consider about such Atsumari N and Class n

　　　　∀ｂ　ｂ∈Ｎ　⇔　ｂ＝ｍ　∧　Ｓｅｔ　ｍ　，　Ｎ　ｍａ　ｎ

"Set m" in the formula of N's condition is not able to be stratified so

¬Ｏｂｊ　ｎ

And with Ａ．Ｐａｉｒ , Ｓｅｔ　ｎ
　 Hence
　　　　Ｓｅｔ　ｎ　∧　¬Ｏｂｊ　ｎ　　−＊１−

And Universal Atsumari U is able be stratified so

Ｏｂｊ　ｕ

With Ａ．⊂ , ¬Ｓｅｔ　ｕ
Hence
　　　¬Ｓｅｔ　ｕ　∧　Ｏｂｊ　ｕ　　−＊２−

And
　　　Ｓｅｔ　０　∧　Ｏｂｊ　０　　−＊３−
Where φ　ｍａ　０

Formula ＊１∧＊２∧＊３ is the condition of Type.3


[ Theorem of Type.4 ]

　Ｔ．４−１　　∀ｙ　¬Ｓｅｔ_ob　ｙ　⇒　Ｏｂｊ　y

　Ｔ．４−２　　¬Ｏｂｊ　ｒ　　　　　　［Ａ．Ｃｌ］

　Ｔ．４−３　　¬Ｓｅｔ_ob　u　　　　　［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　［Ａ．｛　｝］

　Ｔ．４−４　　¬Ｓｅｔ_ob　−ｒ_ob　　［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　［Ａ．｛　｝］

　Ｔ．４−５　　¬Ｓｅｔ　−ｒ　∧　Ｓｅｔ_ob　−ｒ　　［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．｛　｝］

　Ｔ．４−６　　¬Ｓｅｔ　−ｕ　∧　¬Ｏｂｊ　−ｕ　　［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．Ａｔ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．｛　｝］

　Ｔ．４−７　　¬Ｓｅｔ　ｒ_ob　∧　¬Ｏｂｊ　ｒ_ob　　［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．Ａｔ］
　　　　　　　　　　　　　　　　　　　　　　　　　　　　［Ａ．｛　｝］

　Ｔ．４−８　　∀ｙ　¬Ｐｒｃ　ｙ　　［Ａ．Ｃｌ］
　　　　　　　　　　　　　　　　　　　［Ａ．｛　｝］

　Ｔ．４−９　　∀ｙ　¬Ｉｎｄ　ｙ　　　［Ａ．Ｃｌ］


No example of Class Theory of Type.4 exists in known Class Theories