EXPOSITION: T' is a theory in FOL(=,e) with the following axioms: 

Def.) elm(x):= [y](x e y) 
Def.) trs(x):= (y)(y e x -> y c x)

Axioms: 
I. Construction: if phi is a formula in which x is not free, then 
([!x](y)(y e x <-> elm(y) & phi)) is an axiom. 

II. Relations: (a)(b)(x)((y)(y e x -> y=a ? y=b) -> elm(x)) 

Def.) x < y:= [f](f:x-->y & f is injection)
Def.) U(x)=y:= (z)(z e y <-> [m](m e x & z e m)) 

III. Size axioms: 

(x)(y)(elm(x) & y < x -> elm(y)) 
(x)(y)(elm(x) & trs(y) & (z)(z e y -> z < U(x)) -> elm(y)) 

/

Zuhair Al-Johar
14/12/2011
PS: notation at: http://zaljohar.tripod.com/logic.txt


An even shorter axiomatization of mine along generally the same lines is:

Def.) elm(x):= [y](x e y) 

Axiom I. Construction: if phi is a formula in which x is not free, then
([!x](y)(y e x <-> elm(y) & phi)) is an axiom. 

Def.) x < y:= [f](f:x-->y & f is an injection) 

Def.) x <" y:= x < y & (z)(z e TC(x) -> z < y) 

Def.) y << x:= [f](f:x-->y & (z)(z e y\rng(f) -> z <" U(x))) 

Def.) accessible(x):= [=<2y](y e x) ? [y](elm(y) & x << y) 

Axiom II. Size: (x)(accessible(x) -> elm(x)) 

/ 

This Theory depends on two themes that of Construction and Size.
It interprets MK over the realm of well founded sets of it.

Even a clearer version is the following one:

Def.) x < y:=  (x={} ? [f](f:y --> x & x=rng(f)))

Def.) x <" y:= (x < y & (z)(z e TC(x) -> z < y))

Def.) accessible(x):= ([=<2y](y e x) ? [y,z](elm(y) & z < y & (m)(m e x -> m <" U(z))))

And state the axioms of Construction and Size in the same manner above.


Zuhair Al-Johar

PS: [=<2y] stands for there exist at most two sets y; TC,\,rng and U
stand for Transitive Closure, exception, range and Union respectively
defined in the standard manner. 


27.2.2015 : A reformulation of Morse-Kelley (MK) class theory.

Define a set as an element of a class. 

Stipulate the existence of a unique Class {x|phi} for each formula phi that holds of sets only. 

Then add the axiom of pairing which is for any two sets x,y the class {x,y} is a set. 

Then add the following axiom: 

Set(x) <-> Ez (Ayez(z<y) ^ Ayex(y<<TC(z))) 

where "<" stand for "is subnumerouse to" defined in the usual manner
(non strict subnumeroustiy); TC stands for 'transitive closure of"; 
"<<" stands for hereditarily subnumerouse to. 

/ Theory definition finished.

We call  z in the last formula as a "bound" on x.

Actually this theory is equi-interpretable to a version of MK where size
limitation is stated as: what is subnumerouse to a set is a set. This
is sufficient to interpret ZFC. Now if we weaken the above axiom
by replacing TC(z) by z, then we get a theory that is equi-interpretable 
with a version of MK that is sufficient to interpret ZC.

Proof 

Axiom 3 (the last axiom above) is a theorem of MK. 
The first direction is clear since every set x would be bounded 
by the singleton of its transitive closure, or otherwise it is empty, 
and the empty set is bounded by itself. 

The second direction implies that every class of sets that are 
hereditarily subnumerouse to a given set, is a set. This is 
provable in MK since ZF proves the existence of the set of
all sets that are hereditarily subnumerouse to a given set,
by then subclasses of that set are sets according to Mk,
thus proving that direction. 

Proof that this theory prove all axioms of MK-foundation. 

theorems: 0 is a set. 
Clearly TC(0)=0 
Now we do have Aye0(0<y) 
and we do have Aye0(y<<0) 
Thus by the last axiom the empty class is a set! 

Theorem: P(x) is a set if x is a set. 

Proof: Since x is a set thus x has a bound on all its elements 
Now TC(x) will have exactly the same bound on x being a bound 
on all its elements, thus TC(x) will be a set. Now P(x) for non empty x 
will have {TC(x)} being a bound on all its elements, thus P(x) is a set, 
and also clearly P(0)=1 and 1 has 0 a bound on its elements thus 1 is a set. 
QED. 

Theorem: y subset_of x ^ x is a set -> y is a set. 

Clearly the bound on elements of x will be a bound on all elements of y 
thus y is a set. 

Theorem: U(x) is a set if x is a set. 

Since TC(x) is a set and U(x) subset TC(x) then U(x) is a set (above theorem). 

Theorem: The class of all Zermelo naturals is a set. 

All of elements of that class are bounded by {{0}}, then it is a set. 

Theorem: set(Y) ^ X < Y -> set(X) 

We take the set Y and construct the set of all singletons of elements of Y,
i.e. P1(Y). Now we take X, remove empty elements from it, i.e. we take 
the X\{0}, and then take (X\{0}) x {0} which is of course subnumreouse to X, 
then we construct {P1(Y) U {m} | m in  (X\{0}) x {0}}, call this class K,
now clearly K is subnumerouse to Y, so K is subnumerouse to each 
of its elements. Clearly K bounds X, thus X is a set. QED 


Theorem: The range of a function whose domain is a set, is a set. 

Clearly every function is subnumerouse to its domain, then by the above 
theorem it would be a set, now the range of a Kuratowski based function 
is a subset of the double union of it, thus it is a set. 

The later theorem prove replacement over sets easily. 

So all axioms of MK-Foundation (with size limitation stated as mentioned above) 
are axioms or theorems of this theory, and this is known to interpret MK with that
version of size limitation. Thus interpreting ZFC.

Zuhair