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

7. The definition of Ordinal Number.

　Ordinal class is defined as follows :

　Ord x　 Df. ∃ B Ord B ∧ B ma x

　 and Ordinal Atsumari is defined as follows :

　Ord A　 Df. Com A ∧ Con A ∧ Reg A

　Com A　 Df. ∀x　x∈A　⇒　∃!B B<A ∧ B ma x
　Con A　 Df. ∀x∀y　x∈A ∧ y∈A　⇒　x<y | A　V　y<x | A　V　x=y
　Reg A　 Df. ∀B (∃b b∈B) ∧ B<A　⇒　∃a a∈B ∧ (∀b b<a|A ⇒ ¬b∈B)

　x<y | A　 Df. ∃B (x∈B ∧ B ma y) ∧ B<A
　B<A　　 Df. (∀a (a∈B ⇒ a∈A)) ∧ ¬(A=B)

　a comment : Com, Con, Reg are abbreviations of complete, connected, regularity.
　　　　　　 Com corresponds transitive and Con + Reg corresponds well-ordering.
　　　　　　 B<A means B is a proper sub-Atsumari of A.


　It is possible to prove the following theorem.

　T.2 Ord N
　　　　　where,
　　　　　N　　Df. ∀a a∈N ⇔ ord a
　ex. See M5, 0, 1, 2, 3, n are ordinal numbers, so N=U={0,1,2,3,n} and it is Ordinal Atsumari.

　T.3 Ord n

　T.4 ¬Set n
　　　　　where, N ma n


　I have a proof of T.2. It is in Japanese, I am going to translate it in English.

[A part of a proof of T.2.]
　 We prove the followimg theorem.　

　T.C.1　　 ∀a a∈A ∧ Ord A ⇒ Ord a


　Ord A is assumed, so Com A, hense

　∀a a∈A ⇒ ∃!B B ma a ∧ B < A

　B exists only one, so we call it "B0", and we prove "Ord B0" as follows.

　T.C.1.1 Com B0

　　 ∀b b∈B0 ⇒ b∈A　, because B0 < A

　　 Com A , so

　　 ∃!C C < A ∧ C ma b

　 If we assumed the following proposotion.

　P.1 ∃c c∈C ∧ ¬ c∈B0

　　 if a = c , it means b < a | A ∧ a < b | A .

　　 concider the Atsumari {a,b}, it becomes ¬ Reg A.

　　 But, Ord A so Reg A. It is a contradiction.　　　

　　 Or, if ¬ a = c , note that Con A is assumed, so a < c | A V c < a | A .

　　 if a < c | A then b < a | A ∧ c < b | A ∧ a < c | A .

　　 concider the Atsumari {a,b,c} , it becomes ¬ Reg A.. It is a　conteradiction.　

　　 if c < a | A then ∃B' c∈B' ∧ B' m a ∧ B' < A

　　 But, Com A , so ∃! C C m a . It means that B0 = B'

　　 So,　it becomes c∈B0 , but P.1 says that ¬ c∈B0. It is a contradiction.

　　 Hence P.1 is not true.

　　 C ⊆ B0 is proved.

　　 and , ¬ b∈C , so ¬ B0 = C , hence C < B0

　　　because, if b∈C then b < b | A , concider about {b}, it becomes ¬ Reg A　

　　 ∀b b∈B0 ⇒ ∃!C C < B0 ∧ C m b　 is proved.

　　T.C.1.2 Con B0　　

　　 ∀b b∈B0 ⇒ b∈A　, because B0 < A

　　 Con A , so

　　 ∀a∀b ( a∈B0　∧　b∈B0 ) ⇒ ( a = b　V　a < b | A　V　b < a | A )　　....(1)

　　a < b | A　in the right side means the following from the
definition of　" < " .
　　∃C　a∈C　∧　C ma b　∧　C < A　　

　　It is possible to prove that C <B0　　the same way in the consideration about T.C.1.1.

　　So,　it becomes as follows,

　　∃C　a∈C　∧　C ma b　∧　C < B0　　

　　Hence, (1) becomes as the following formula,

　　∀a∀b ( a∈B0　∧　b∈B0 ) ⇒ ( a = b　V　a < b | B0　V　b < a | B0 )　　

　　This is the definition of Con B0.

　　T.C.1.3　Reg B0　　　　　　　　　　　　　　　　　

　　We assume the following axiom,

　　A. Reg.　∀B Com B　⇒　Reg B　

　　T.C.1.1. and A. Reg means Reg B0.

　　A comment :

　　Without this axiom it is possible to prove T.C.1.3. There is no difficulty.

　　T.C.1.1. and T.C.1.2. and T.C.1.3. means Ord B0.

　　So, T.C.1. was proved.

It means the following formula.

∀x　x∈A　⇒　 ∃B B⊆A ∧ B ma x

It is still not enough to Com N.



　8. The existence of 1-1 function between X and the power Atsumari of X.

　　　 member of X　1-1f　⇒　member of P(X)

　　　　　　a　　 corresponds　　 f(a)

　　 P(X)={b : a sub-Atsumari of X makes b} , or precisely it is defined as follows :

　　 ∀a a∈P(X) ⇔ ∃M M ma a ∧ M ⊆ X

　　　　　　　　　　　where,
　　 M ⊆ X means M is a sub Atsumari of X.

　　 M ⊆ X　 Df. ∀a (a∈M ⇒ a∈X)

　If an 1-1 function f exists between an Atsumari X and the P(X) then,

　Let us consider an Atsumari B such that :

　　 ∀a a∈B ⇔ ¬ (∃C a∈C ∧ C ma f(a)) ∧ a∈X　　(B)

　　 and this Atsumari B makes a class b, so B ma b　(1)

　　　　　B⊆X , b∈P(X) , so

　　 ∃b' f(b')=b ∧ b'∈X

　　 let a=b' in formula (B)

　　　 b'∈B ⇔ ¬ (∃C b'∈C ∧ C ma b) ∧ b'∈X

　　　if b'∈B is true, then considering (1), right side of formula is false.

　　　it is contradiction. So,

　　　 ¬ b'∈B , ∃C b'∈C ∧ C ma b

　　 this conclusion is not a contradiction, it means 1-1 function f may exist.

　　 ex. Indeed, in M5, if X=U then P(X)=U, naturally, 1-1f between U and U exists.