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

　11. a contradiction of { NF + some axioms }.

　R and U have self-membership, so this concept has the meaning of "large".

　 A.1.　x is large ⇒ {x} is large
　 A.2.　b is individual ⇒ {b} is not large

　Both axioms seem to be correct.
　NF doesn't adjust to　these two axioms.


A representation of a Set Theory on FC is defined in the next subsection “11-1. Object”

　11-1. Object
　 If we defined "Object" in FC, then we obtain a representation of a set
theory.

　　 Obj x　Df. a formula of x

　The formula in the definition describes what have sethood in the represented set theory.

　ex.1.　a ZF like set theory

　　 1. Obj 0

　　 2. Obj a ∧ Obj b ∧ {a,b} ma c ⇒ Obj c

　　 3. One X ∧ X ma b ∧ Obj b ∧ UX ma c ⇒ Obj c
　　 One B Df. ∀X∀Y∀c X ma c ∧ Y ma c ∧ c∈B ⇒ X=Y
　　 UC　　Df. [A[b b∈UC ⇔ ∃a∃K b∈K ∧ K ma a ∧ a∈C

　　 4. X ma b ∧ Obj b ∧ P(X) ma c ⇒ Obj c

　　 5. A ma a ∧ B ma b ∧ A⊆B ∧ Obj b ⇒ Obj a

　　 6. A ma a ∧ B ma b ∧ A=f"B ∧ Obj b ⇒ Obj a
　　　　f"B　　Df. the image of B with f.

　　 7. 0∈X ∧ (b∈X ⇒ b'∈X) ∧ X ma c ⇒ Obj c

　ex2.　NF

　　 Obj x　Df. x is stratified.

　11-2. object class , individual, proper class.
　I define some relative ideas to Object such that "At, Cl, Obcl, Ind, Prcl."

　These are abbreviations of relative "Atsumari, class, object class, individual, proper class" from a point of view on Object.

　　 At C　Df. ∀b b∈C ⇒ Obj b

　　　　 If all members of an Atsu are Objects then the Atusmari is a relative Atsumari for the represented set theory.

　　　　 ex.1.　in NF
　　　　 At {0,u}　, where U ma u, ∀b∈U ⇔ b=b
　　　　 Both 0 and u are stratified, so Obj 0 ∧ Obj u

　　　　 ex.2.　in NF
　　　　 ¬At {r}　 , where r means Russel's class.
　　　　 r is not stratified, it means ¬Obj r

　　 A.At　　∀B ¬At B ⇒ (∀x x∈B ⇒ ¬Obj x)

　　　 This axiom separates Obj and ¬Obj.

　　 Cl b　Df. ∃C At C ∧ C ma b
　　　　 If a relative Atsumari makes a class then the class must be a relative class for the represented set theory.
　　　　 ex.　 in NF
　　　　 Cl c　, where {0,u} ma c

　　 A.Cl　　∀b Cl b ⇒ (∀X X ma b ⇒ At X)

　　　　 This axiom separates At and ¬At.

　　 Obcl b　 Df. Cl b ∧ Obj b

　　 Ind x　　Df. ¬Cl x ∧ Obj x

　　 Prcl c　　Df. Cl c ∧ ¬Obj c

　　　　 These definitions are obvious.
　　　　　　　　　 ex.　　in ZF
　　　　　　　　　 set is object and class, so ∀b setzf b ⇒ Obcl b
　　　　　　　　　 where setzf means "set" in ZF.


　11-3. A contradiction of NF.

　We assume three axioms as follows :

　　 A.Set.　 ∀C∀b (∃x x∈C ∧ C ma b ∧ ¬Set x) ⇒ ¬Set b

　　 ¬Set means something great like r or u, so if {u} ma k then k is also great, hence k must be ¬Set.

　　 A.Obcl.　 ∀x∀b {x} ma b ∧ Ind x ⇒ Obcl b

　　 For example, an apple is individual, and if {an apple} ma b then b must be Obcl.

　　 A.Set'. ∀x∀b {x} ma b ∧ Ind x ⇒ Set' b

　　　　　　　　　　　　　　　　　 Set' b Df. ¬(∃C b∈C ∧ C ma b ∧ At C)

　　 [ A proof of { NF+A.Set.+A.Set' } has a contradiction ]

　　 Consider about Class r.
　　 ¬Set r　　　　　, where r is Russel's class.

　　 ¬Set r'　　　　 , where {r} ma r' . We used A,Set.

　　 ¬Set　r''　　　　, where {r'} ma r''. Again from A.Set.

　　 And, the other hand.
　　 ¬stratified r　　 , it is obvious.

　　 ¬Obj r　　　　 , see section 1 ex,2

　　 Ind r'　　　　 , ¬At {r} and use A.Cl , so ¬Cl r'. And {r} is stratified, so Obj r'

　　 Set'　r''　　　　, see A.Set'

　　 So,

　　 ¬Set　r''　∧　Set'　r''

　　 It means ∃B r''∈B ∧ B ma r'' ∧ ¬At B.　　 (F)

　　 with A.At and the formula (F), we get ¬Obj　r''.　

　But, stratified r'' so Obj r''. This is a contradiction.

　　　Another conclusion ;

　　 with A.Cl and the formula (F), we get ¬Cl r''.　　　

　But, Ind r' ∧ A.Obcl means Obcl r'', so Cl r''. It is a contradiction too.