[Free Class Theory]

A system which is able to analyze any set theory

 

    0. Introduction. 

   Here is a part of g Fly me to the moonh which Sinatra sings

 

                            Fly me to the moon,

@@@@@@@@@@@@ And let me play among the stars

@@@@@@@@@@@@ Let me see what spring is like on Jupiter and Mars

@@@@@@@@@@@@ In other words: Hold my hand!

@@@@@@@@@@@@ In other words: Darling kiss me!

 

    It is possible to consider about many objects on this poem.

    A language L_1 = {Fly me to the moon}, a significations S_1 which L_1 means.

    A language L_2 = {Hold my hand!. Darling kiss me!}, a signification S_2 which L_2 means.

    A mapping P_1 called  gpoemh form L_1 to L_2, and a mapping P_2 which P_1 generates between S_1 and S_2.

 

    This consideration might be natural and usefull.

    But I think that it is too complicated.

 

    Is it possible to describe it more easily?

    What we should analyze is the sentence that {Fly me to the moon}.

    A sentence that { Hold my hand!. Darling kiss me!} is a meta language of the sentence, because it explains her mind. 

    And correspondences between sentences and significations are almost an one on one mapping ,so we are able to make them equals.

    Notice that it is not necessary to analyze the standard grammar, but we should analyze her grammar.

    If we consider these things, it is described as follows.

 

    The sentence which she said {Fly me to the moon} becomes an idea { Hold my hand!. Darling kiss me!} in her mind.

    If the partner listens to this phrase, then he must imagine  what she want and do it.

 

    These things are  formalized as follows.

 

    Ideas Fly, me, to, the, moon are members of a sentence S={ Fly me to the moon }, and the sentence S makes an idea I={ Hold my hand!. Darling kiss me! }

 

    If we use formulas, it becomes the following.

    Fly¸S, me¸S, to¸S, the¸S, moon¸S, and S ma I

    

    Sentence and idea in language correspond gAtsumarih and gClassh in gFCh=gFree Classh

    So, gidea¸sentenceh and gsentence ma ideah becomes gClass¸Atsumarih and gAtsumari ma Classh in Free Class theory.

 

    In next section, exact explanations about the words gmah or gAtsumarih are described

 

 

 

@1.Axiom of Free Class.

@

@

@A. maAÍBÍxÍy@ A ma x È B ma y È A=B Ë x=y

@This axiom means that any Atsumari makes only one class.

@

@A. elAÍB (Ía a ¸ A Ì a ¸ B) Ë A=B

@This axiom means that an Atsumari is decided by its members.

@

@A.FxÎB (Ía a ¸ B Ì F(a)) È B ma x

@This is the Schema of comprehention axioms.

@

@Where A,B,C,...are variables for Atsumari, which means collection or set or pile in Japanese.

@@@ a,b,c,...are variables for Class,

@@ Í means all, Î means exist, Î! means exist only one, ma means makes,

@@@¸ means element, Ë means then, Ì means equivalent,

@@ V means or, È means and, Atsu is an abbreviation of Atsumari

@@ Ê means negation, {a,b,c} means the Atsu which has members a,b,c

@

@

@2.What does Free Class mean?

@

@

B a¸B È B ma b@means@a¸b@in .ZF@@(TR)

@

@

@For example if {a,c} ma b È {x,y} ma b are true,

@@@@then a¸{a,c} È {a,c} ma b

@@@@soB a¸B È B ma b

@@@@it means a¸b in ZF.

@@@@@@FC@@@@@@@@@          @ ZF

@@@@{a,c} ma b@ corresponds@@ a¸b, c¸b

@@@@{x,y} ma b@@@@@         @@@x¸b, y¸b

@

@

@3. Russel's class

@

a a¸R Ì Ê(ÎB a¸B È B ma a)

@

@

@The right side of formula means Ê(a¸a) in ZF.

@This Atsu R makes Russel's Class r, so R ma r.

@Let a=r then,

@@ r¸R Ì Ê(ÎB r¸B È B ma r)

@If@r¸R is true, considering that R ma r is also true,then

@@ ÎB r¸B È B ma r@is true, then right side of formula is false. This is a contradiction.

@So, the following formulas are gotten.

@@ Ê(r¸R), ÎB r¸B È B ma r.

@This conclusion means that the diagonal logic was dissolved.

@So, it is possible to think that 2^aleph(0)=aleph(0).@@ ..... See the description about M5.

@

@

@4.Idea gSet g

@I use the word "Set" for representing a scale of a Class.

@The definition of Set is the following.

@

@

@Set x@Df. Ê(ÎB x¸B È B ma x)

@

@@ a comment :

@@ I think  that  it might be better to describe "little" or "Normal" or "NSM" for non-self-membership.

@@ All of the classes in FC have sethood, so "set" is useless. I recycled it.

@

@Then Russel's Class is written as follows.

@

a a¸R Ì Set a

@

@

@And results are,

@@ Ê(r¸R), ÊSet r

@

@

@T.1 ÊSet u

@Proof.

a a¸U Ì a=a

@@ This Atsu U makes u, U ma u@ (1)

@@ a=u

@@ u¸U Ì u=u

@So@u¸U@is true

@@ u¸U È U ma u@because (1)

@@ÊSet u

@

@

@But it is impossible to prove Set 0.

@The Atsu P which makes 0 is defined as follows,

a Ê(a¸P) , so

@@@Ê(0¸P),

@But another Atsu P' which has 0 as an element and also makes 0 may exist.

@P={ }, P'={0,x,y}, P ma 0, P' ma 0

@It means that Class 0 may not be Set.

@We need the following Axiom.

@

@A.0 Set 0

@

@

@5. An explanation of the concept "make".

@I give some examples of how to use the "make" in the other theories or systems.

 

@ex.1

@Ideas "I", "love" and "you" are members of sentence {I,love,you}.

@And a sentence {I,love,you} makes an idea "I love you.".

@So, it is written as follows,

@@ I¸{I,love,you}, and {I,love,you} ma "I love you".

@We should denote that {I,love,you} is only an arrangement of members, and "I love you." is an idea.

@Ordinary theories of language don't distinguish these two things.

@In this case, idea and sentence correspond Class and Atsu.

 

@ex.2

@A sheep is a member of a group of all sheep, and a group of all sheep makes an idea "sheep".

@Where the idea "sheep" is defined as follows,

@@ "cattle which we use their meat and milk and hair."

@If we told this definition to the people of mountains Andes, they would say, "Ah, I understand what the word sheep means.", and they must be thinking that it means "alpaka".

@So, it is possible to say that a group of all alpakas also makes the idea "sheep" which has another name "alpaka".

@All these things are written as follows,

@@ a sheep¸{x : x=sheep}, and {x : x=sheep} ma an idea "sheep",

@@an alpaka¸{x : x=alpaka}, and {x : x=alpaka} ma an idea "sheep".

@

@6.Model of FC.

 

    [M5]

@M5 is defined as follows:

@

@

@U={0,1,2,3, n}

@{  } ma 0, {0} ma 1, {0,1} ma 2, {0,1,2} ma 3, {0,1,2,3} ma n, {0,1,2,3,n} ma n,

@for all other Atsu X, X ma n

@

@

@We are able to verify the result of section 3. on M5.

@On M5, classes 0, 1, 2, 3 are Set.

@So, R={0,1,2,3}

@and r=n , because {0,1,2,3} ma n

@The two formulas of a conclusion of section 3 are Ê(r¸R), ÎB r¸B È B ma r.

@Both are true, because Ê(n¸{0,1,2,3}) and n¸{0,1,2,3,n} È {0,1,2,3,n} ma n

@

@M5 satisfies almost all of ZF, except the axiom of foundation.

@Any model of FC satisfies all axioms of ZF except the axiom of foundation.

@Because A.F. of FC says any@class exists.

@This axiom also allows a class x such that ÎB x¸B È B ma x which means x¸x in ZF.

@But it is obvious that the existence of such a class contradicts to the axiom of foundation.

@

@@   comment :

    Podnieks claimed that FC doesnft prove existence of number g6h because M__5 whose members are 5 exists.

@@ It is      impossible to prove existence of infinity, because in ZF if {  } exists it means an infinite set exists, but in FC it doesn't mean an infinite Atsu exist.

 

It means that axioms of FC are weak.        

It is rather good.

 

    [M_k]

@@T. continum

k k is a natural number Ë {2^alepf(0)=alepf(k) is not contradict to ZF}

@

@[proof]

@Consider the following model of FC named M_k.

@M_k :

@ {0,1,2,3,...k,k+1,k+2,k+3,...2*k}

@ { } m 0, {0} m 1, {0,1} m 2, ... , {0,1,2,3,...,k-1} m k, {0,1,2,3,...,k} m k,

@ {1} m k+1, {2} m k+2, ... {k} m 2*k

@ other B B<N Ë B m k

@{0,1,2,3,...k-1, {k}} m k+1, {0,1,2,3,...k-1, {k}, k+1} m k+2, ... ,

@{0,1,2,3,...k-1, {k}, k+k} m 2*k

@@other B ÊB<N È BºU Ë B m 2*k

@

@

@ N={0,1,2,3,....,k}

@ P(N)={0,1,2,3,....,k,k+1,k+2,k;3,....,2*k}

@ So,

@@@aleph(0)=#N=k+1

@@@2^aleph(0)=#P(N)=2*k+1=aleph(0)+k

@@@all aleph (1), aleph(2),...., aleph(k-1) exist.

@@@It means,

@@@2^alepf(0)=alepf(k)

@@@@@where #N means the number of members of N.@

 

@7. The definition of Ordinal Number.

@Ordinal class is defined as follows :

@

@

@Ord x@ Df. Î B Ord B È B ma x

@ and Ordinal Atsu 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-Atsu 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 Atsu.

@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

@

@See fig.1

@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. ...See fig.1.

@

@P.1 Îc c¸C È Ê c¸B0

@

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

@@ concider the Atsu {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 Atsu {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 Atsu of X.

@

@@@ member of X@1-1f@Ë@member of P(X)

@@@@@@a@@ corresponds@@ f(a)

@

@@ P(X)={b : a sub-Atsu 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 Atsu of X.

@@ M º X@ Df. Ía (a¸M Ë a¸X)

@

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

@

@Let us consider an Atsu B such that :

@@ Ía a¸B Ì Ê (ÎC a¸C È C ma f(a)) È a¸X@@(B)

@@ and this Atsu 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.

@

@

@9.      Dificulty of cardinal number of an Ordinal number.

 

@Ordinal class is defined as follows :

 

@Ord x@Df. ÎB Ord B È B ma x

 

@So, it seems to be possible that two different Ordinal Atsu make an Ordinal class.

@If it is true, it means the following :

@@@ Ord A È A ma x

@@@ Ord B È B ma x

@@@ Generally, the cardinal number of Atsu A and Atsu B are different, then which is the cardinal number of Ordinal number x?

@If an Ordinal number has two cardinal number, it is not useful. We are not able to use it as a number.

@But, fortunately, it is possible to prove that only one Ordinal Atsu makes an Ordinal number.

@[Ploof]

@We assume T.2. and the following theorem :

@@@ T.Or ÍA Ord A Ë (Íb b¸A Ë Ord b)

@@@ it is possible to prove T.Or.

@AºN È BºN , because Ord A and Ord B and T.Or.

@If ÊA=N È ÊB=N then

@A<N È B<N@@@(1)

@and the other hand, T.2. include Com N. It means :

@@@ Ía a¸N ËÎ!M M ma a È M<N

@@@ Ord x , so x¸N , hense,

@@@@@@@ Î!M M ma x È M<N@ (2)

@ If both Atsu A and B make x, considering (1), it contradicts to (2).

@Because (2) means only one such Atsu exists.

@

@We get the following theorem :

@

@T.Or1.AÍBÍxÍy Ord A È Ord B È ÊA=N È ÊB=N È A ma x È B ma y

È x=y Ë A=B

@

@If we ask the cardinal number of an Ordinal class, it means we ask the cardinal number of the only one Ordinal Atsu which makes the Ordinal class, and the answer is the number of members of the Atsu.

@There is a possibility that other Atsu C which is not Ordinal Atsu makes x. I am sure it is no problem, because if we are talking about numbers, an Atsu which is not Ordinal has no relationship with the subject.

@

@

@

@

@10. about infinity

@

@M5 allows the existence of Infinite Atsu@:

@Where "infinite" is defined as follows :

@@ Inf N@Df. 0¸N È (a¸N Ë a'¸N)

@

@  comment :

@@ I wrote at section 6. that no infinite Atsu exists in M5.

@@ It means that an Atsu which has all of the characters of "infinity" doesn't exist.

@@ But, a kind of infinity exists in M5.

@@ The definition above is one character of infinity.

@

@Indeed,

@

@@ { } ma 0,

@@ { }'={ }U{0}={0},@{0} ma 0', 0'=1,

@@ {0}'={0}U{1}={0,1}, {0,1} ma 1', 1'=2,

@@ {0,1}'={0,1}U{2}={0,1,2}, {0,1,2} ma 2', 2'=3,

@@ .....

@@ {0,1,2,3}'={0,1,2,3{U{n}={0.1.2.3.n}, {0,1,2,3,n} ma n', n'=n,

@@ {0,1,2,3,n}'={0,1,2,3,n}U{n}={0,1,2,3,n}, {0,1,2,3,n} ma n', n'=n,

@@ .....

@@ it continues infinitely, because n'=n in M5, so {0,1,2,3,n } satisfies the difinition of Inf .

@

@@ So, in M5,

@@ ÎB Inf B

@

@@ More exactly,

@@ See the definitions of {a,b,c}' and x', (D1) and (D2) respectively as follows :

@

@

@@ Natural Number is defined as follows :

@

@

@@ Nat { }@È@ ÍAÍa Nat A È A ma a Ë Nat A'

@

@@@@@ where@A' is defined as follows :

@@@@@ A'@Df.AÍa A ma a Ë@A'=AU{a}@@(D1)

@

@@ Nat x@Df.B Nat B È B ma x

@

@Natural Number in a finite model doesn't satisfy Peano's Axiom, because

it has a terminal class such that n'=n.

@@@@@ x'@Df.BÍx B ma x Ë@B' ma x'@@(D2)

@But Natural Number in a infinite model is the same thing as Natural Number in ZF.

@@@@@ ex. U={0,1,2,3,....u}, {0,1,2,3,...} m u, U m u

@Notice that in M5, the following equation is true :

@@@@@ 3^4+3^4=3^4

@@@@@ because 3^4=n and n+n=n

@@@@@ it is easy to define + and ^ .

@ It means a^m+b^m=c^m , 2<m have a solution in M5.

@@ m+n@@Df.@(m+(n-1))'

@@ m*n@@Df.@m*(n-1)+m

@@ m^n@@Df.@m^(n-1)*m

@

@It is not possible to prove the existence of an Atsu which has six members, though Axioms of FC allows to prove the existence of an infinite Atsu such that {0,1,2,3,n} in M5.

@It follows the fact that the definition of Inf N says nothing about the number of member of N.

@

@

@For more interesting class theory, we need the following Axioms of infinity.

@

@A. Infp

C Infp C

@@@@@@@Infp X@Df. ÎB B<X È a 1-1 function exists between B and X.

@

@

@

@

@

@

@

@

@

 

@

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 g11-1. Objecth

 

@

@

@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 "Atsu, 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 Atus is a relative Atsu 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 Atsu 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.