[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. ma@ÍAÍBÍxÍy@ A ma x È B ma y È A=B Ë x=y
@This axiom
means that any Atsumari makes only one class.
@
@A. el@ÍAÍB (Ía a ¸ A Ì a ¸ B) Ë A=B
@This axiom
means that an Atsumari is decided by its members.
@
@A.F@ÎxÎ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
@@@@so@ÎB 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 "
@@ 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
@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,
@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 È
@@ For
example, an apple is individual, and if {an apple} ma b then b must be Obcl.
@@@@
@@ A.Set'. ÍxÍb {x} ma 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.