Triclass Theory
- From: "zuhair" <zaljohar@xxxxxxxxx>
- Date: 13 Mar 2007 09:24:28 -0700
Hi All,
The following is a set theory that I developed latelly.
I don't know if it is consistent or not?
Hereby I present it to be tested.
Introduction: This theory is an extension of first order logic with
identity. It contains three types of classes.
Types of classes
1) A unique class of all classes that is not a member of any class
other than itself. And this class is T.
x=T <-> Ay(yex & ~Ez(~z=x & xez)).
2) classes other than T, that only T contain them as members, and
these classes are called 'proper classes'.
x is a proper class <-> (~x=T & ~Ez(~z=T & xez)).
3) classes that are members of a class other than T, and these
classes
are called 'sets'
x is a set <-> Ez(~z=T & xez).
Structure:
All sets are members of one unique proper class V.
All proper classes are subclasses of V and are not in V.
T contains all classes and itself as members.
Defining the theory.
Name of the theory is 'Triclass' .
Triclass is the set of sentences entailed
(from first order logic with identity)by these axioms:
1) Extensionality: AxAy(x=y<->Az(zex<->zey)).
2) Universe: E!xAy(yex & ~Ez(~z=x & xez)).
Definition 1) x =T<-> Ay(yex & ~Ez(~z=x & xez)).
3) Regularity:
Ax((~x=T & Ez(zex))->Ey(yex & ~Ec(cey & cex))).
4) Schema of Global comprehension: if P is a formula in which x
doesn't occure free, then all closures of:
ExAy(yex<->(P(y)&Ez(~z=T & yez)))
are axioms.
Theorum 1) V.
E!xAy(yex<->Ez(~z=T& yez)).
Proof: From global comprehension if we let P(y)<->y=y
we get
ExAy(yex<->Ez(~z=T& yez)).
To prove x is unique, let x1 and x2 be defined as
Ay(yex1<->Ez(~z=T& yez)).
Ay(yex2<->Ez(~z=T& yez)).
for a proof by negation suppose that ~x1=x2
Then there should be a set u: uex1 and ~uex2
Or u: uex2 and ~uex1.(Extensionality).
if u: uex1 and ~uex2 , then x2 is not the class
of all sets, violating its definition.
if u: uex2 and ~uex1 , then x1 is not the class of
all sets, violating its definition.
Therefore x1=x2.
This means the following.
Ax1Ax2 ((Ay(yex1<->Ez(~z=T& yez)) &
Ay(yex2<->Ez(~z=T& yez)))->x1=x2).
Thus proving E!xAy(yex<->Ez(~z=T& yez)).
Now since x is unique then we proceed to name it.
Definition 2) x=V <-> Ay(yex<-> Ez(~z=T & yez)).
Definition 3) x is a proper class <-> (~x=T & ~Ez(~z=T & xez)).
Definition 4) x is a set <-> Ez(~z=T & xez)
Accordingly V is the proper class of all sets.
Theorum 2) ~VeV.
Proof: let VeV. then we have Ez(~z=T & Vez) otherwise
~VeV. (The definition of V).
so ~V=T, since ~Ez(~z=T & Tez). definition 1.
Since VeV then pairing applies to it and we have
from pairing B={V}. Now from pairing we have BeV
and since ~V=T, then B is a member of a set that is not T
therefore ~B=T. And since B has V as a member then
Ez(zeB). Thus regularity applies to B..
But B vioates regularity! A contradiction.
Thus ~VeV.
Theorum 3) ~T=V
Since ~VeV (theorum2) and since VeT (axiom 2).
Thus ~V=T (Extensionality).
5) Empty set: ExeVAy(~(yex)).
From extensionality x is unique.
Definition 5): x=0<->Ay(~(yex)).
6) Pairing:AaeVAbeVExeVAyeV(yex<->(y=a or y=b)).
7) Union:AaExAy((yex<->Ez(zea&yez))&(Em(~m=T & aem)<->En(~n=T &
xen))).
Definition 6) x=Ua<->Ay(yex<->Ez(zea&yez)).
This axiom simply states that the union class of a set is a set
and the union class of a proper class or T is a proper class or T
respectivelly. so we have the following theorum.
Theorum 4)Ax(x is a set<->Ux is a set)
Theorum 5) small binary union
AaeVAbeVE!xeVAy(yex<->(yea or yeb)).
Proof: Since a and b are sets then from pairing
c={a,b} is a set.
From Union we have UceV. i.e Uc is a set.
and Uc here is the unique x in this theorum.
Definition 7) x=aUb <-> Ay(yex<->(yea or yeb)).
were aeV and beV.
8) Infinity:ENeV(0eN&(AxeV(xeN->xU{x}eN))).
were{x}comes from pairing x with itself.
9)Power: Aa(~a=T)ExAyeV((yex<->Az(zey->zea))&
(Em(~m=T & aem)<->En(~n=T & & xen))).
Definition 8) x=P(a)<->AyeV(yex<->Az(zey->zea)).
were ~a=T.
So this axiom simply states that the power class
of a set is a set and the power class of
a proper class is a proper classs. so we have the
following theorum
Theorum 6)Ax(~x=T)( x is a set <-> P(x) is a set ).
Definition 9) y subclass_of a <-> Az(zey->zea)
were ~a=T.
Definition 10) y subset_of a <-> (y subclass_of a & yeV)<-> yeP(a).
were ~a=T.
Definition 11) y proper subclass_of a <-> (y subclass_of a & ~yeV)
Theorum 7) Large binary union.
Aa(~a=T)Ab(~b=T)ExAy(yex<->(yea or yeb))
Proof: follows directly from global comprehension,since
y is always a set , because it is a member of a or b
which are not T.
so we have aUb even when "a is a proper class or b is a proper
class'.
Theorum schema 8) Large separation
if Q is a formula in one variable in which x doesn't occure free then
all closures of
Aa(~a=T)ExAy(yex<->(Q(y) & yea))
are theorums.
Proof: since ~a=T and yea then y is a set
and simply substituting P(y)<->(Q(y)&yea)
in global comprehension yields theorum 8.
Theorum 9) Cartesian Product:
Aa(~a=T)Ab(~b=T)E!xAy(yex<->EuEw(y=<u w> & uea & web)).
were '< >' means an ordered pair, as defined in the standard manner.
Proof: since neither a nor b are T
then for every u ,every w such that uea and web
,u and w are sets. ( definition of set ). Therefore
we can have ordered pairs of u and w i.e <u w> eV
and <w u>eV .(Axiom of pairing).
let P(y)<->EuEw(y=<u w> & uea & web)
substituting it in global comprehension yields theorum 9.
Definition 12) z=axb <-> Ay(yez<->EuEw(y=<u w> & uea & web)).
axb is the cartesian product of a and b.
of course in this theory we have 'axb subclass_of P(P(aUb))' as a
theorum, this can be easily proved from large separation.
Theorum schema 10) Relation
if P is a formula in one variable in which x doesn't occure free then
all closures of
Aa(~a=T)Ab(~b=T)ExAy( yex<->(ye(axb) & P(y)))
are theorums.
Proof: it follows from theorum 8 & 9.
This theorum schema allows us to define functions, injections,
surjections and bijections in the standard way between any two
classes
weather sets
or proper classes provided that any of them is not T.
Definition 13) x is supernumerous to a <->(~Ef(f:x->a &
f is injective) & Eg(g:a->x & g is injective)).
were ~a=T and ~x=T
Definition 14) x is subnumerous to a <-> (Ef(f:x->a & f is injective)
& ~Eg(g:a->x & g is injective)). were ~a=T and ~x=T
Definition 15) x is equinumerous to a <-> Ef(f:x->a & f is
bijective).were ~a=T and ~x=T
Theorum 11) Non supernumerosity of subclasses.
AxAa( x subclass_of a -> ~ x is supernumerous to a ).
Proof: Let f be the identity function f(x)=x
from x to a. Then f is injective from x to a.
So it cannot be supernumerous to a ( definition 13).
Theorum schema 12) Large replacement.
if Q is a formula in two variables in which b is not free,then
all closures of
(AxeVE!yeV(Q(x,y)))->Aa(~a=T)EbAy(yeb<->Ex(xea):Q(x,y)).
are theorums.
Proof:
since yeV then y is a set, then
letting P(y)<->Ex(xea):Q(x,y)
substituting it in global comprehension
we get theorum schema 12.
Theorum 13)Non supernumerosity of
the range of any function over its domain
if AxAyAf( (x is dom(f) & y is range(f)) -> ~ y is supernumerous to
x).
were dom(f) and range(f) defined in the standard manner.
Proof: if y is supernumerous to x , then there exist
at least two ordered pairs in f such that for the same uex
there are different sets w and k in y. i.e there must exist
at least two ordered pairs <u w>ef and <u k>ef were ~w=k
violating the definition of a function.
10) limitation of size:
Ax((Ez(~z=T & xez)) <-> x is subnumerous to V).
From this axiom follows four important theorums/schemas.
Thoerum schema 14) small separation
if P is a formula in one variable in which x is not free then all
closures of AaeVExeVAy(yex<->(yea & P(y))) are theorums.
Proof: follows from large separation and non supernumerousity of
subclasses and axiom 10.
Theorum schema 15) small replacement.
if P is a formula in two variables in which b is not free then
all closures of
(AxeVE!yeV(Q(x,y)))->AaeVEbeVAy(yeb<->Ex(xea):Q(x,y)).
are theorums.
Proof: this follows from large replacement and non supernumerosity of
the range of any function over its domain, and axiom 10.
Another proof: Since for every yeb there exist x in a
and since for every y1eb and y2eb such that ~y1=y2 there exist at
least x1ea and x2ea such that ~x1=x2
Then there exit an injection from b to a, Thus ~b is supernumerous to
a.
Theorum 16) Proper binary union.
Aa(~a=T &~aeV)Ab(~b=T)Ex(~x=T&~xeV)Ay(yex<->(yea or yeb))
Proof: This follows from large union and non supernumerousity
of subclasses and limitation of size.
Definition 16) x is an ordinal <-> AzAy(zey&yex->(zex&Au(uez->uey))).
Theorum 17) global choice: Ey( y is an ordinal & V is equinumerous to
y).
Proof:
we already have E!yAx( xey<-> (x is an ordinal and Ez(~z=T & xez)))
as
a theorum in this theory [because if we let
Let P(x)<->AzAy(zey&yex->(zex&Au(uez->uey))).
substituting P(x) in global comprehension yields.
EyAx(xey<->(x is an ordinal and Ez(~z=T & xez))).
y is proved to be unique in a similar manner to how uniqueness
of V is proved.].
Definition 17) y=O<->Ax( xey<->(x is an ordinal and Ez(~z=T &
xez))).
Now we have ~OeO as a theorum in this theory (Proof similar to ~VeV).
Thus O is the proper class, i.e ~Ez(~z=T & Oez) ,of all ordinals that
are sets. and O is itself an ordinal( definition 16).
(it is easy to prove that O is an ordinal).
Since we have ~Ez(~z=T & Oez) then O is not subnumerous to V ( axiom
10).
Now since O subclass_of V, then O is not supernumerous to V(theorum
11).
so O is neither super- nor sub- numerous to V. then
O is equinumerous with V.
Since O is an ordinal, then global choice proved.
Theory definition finished.
/
The above is the theory with the important defining theorums in it
There are a lot of theorums concerning proper classes,but these are
to be discussed later.
The important results that I think this theory can acheive are
1) Prove ZFC
2) define intersections
3) defining cardinalities of proper classes.
As for 1) it is clear that all axioms in ZFC except infinity and
pairing and empty are theorums in this theory, while infinity and
pairing and empty are axioms here. so ZFC is in this theory.
2)Theorum of Interesection:
AyE!xAz(zex <-> Aj(jey -> zej)) can be easily proved
in this theory.
the problem was when y=0 , what would be x.
here the answer is x=T.
so x=intersection y is defined here for all y.
3) This theory defines relations not only between sets
but also between proper classes, and between sets and proper classes.
Now we can have equivalence classes of all sets
i.e Frege definition of cardinality, but this won't work
for the case of proper classes, therefore Von Neuman's
method is better, since it defines the cardinality of
proper classes which is O.
Cardinality is defined here in the following manner.
card x <-> The intersectional class of all ordinals bijectable to x.
so the intersectional class of all ordinals bijectable to V is O.
so card V = O.
( Just to clarify that:
Definition of Cardinality
Ax(~x=T)(card(x)=y <->(y is an ordinal & y is equinumerous to x &
~Ez(z is an ordinal & z is equinumerous to x & zey))).
Of course
Ax(~x=T)E!y(y is an ordinal & y is equinumerous to x & ~Ez(z is an
ordinal & z is equinumerous to x & zey)).
is a theorum in this theory. It can be easily proved.
Now we have card(V) = O.
This is because Ax(xeO -> x is a set), then
x is subnumerous to V (axiom 10). we know that O is equinumerous to
V.
Then there do not exist an ordinal
in O that is equinumerous to V.
O is an ordinal (definition 16).
then O is card V.)
T in this theory is somewhat detached from the other sets and proper
classes, you cannot define subclasses of T that are not subclasses of
V,
Union T = T. Power is not defined for T.
You cannot have separation on T, nor replacement , T is outside the
reach of regularity and choice, no cartesian product is defined
between T and any class including itself.
So the main function of T is intuitive: it has them all including
itself as members, besides it might lead to the emergence of theorums
that requires the existance ot T, a situation similar to theorum of
intersection.
Now this theory might be balantently inconsistent, or might be
consistent, I don't know, that's why I presented it here , in order
to be checked.
Zuhair
.
- Prev by Date: Re: Review of Mueckenheims book.
- Next by Date: Re: Fermat's Last theorem short proof
- Previous by thread: fixed point space
- Next by thread: One interesting sequence
- Index(es):
Relevant Pages
|
