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 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" defined
as the "minimal transitive superclass of"; and "<<" stands for hereditarily 
subnumerouse to. 

/ Theory definition finished.

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

Notation: "e" stands for membership; "E" for existential quantifier
and "A" for universal quantifier.

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 
March 1 2015

Addendum (March 6 2015):
It's worth noting that if we tweak the definition of 'is subnumerouse to' to the following: 

x subnumerouse to y <-> (EzAmex(m=z)^Ek.key)V(Ef(f:x->y^f is injective)). 

In English: x is subnumerouse to y if and only if x at most have one element and y has 
at least one element or if there exist an injective function from x to y.

then this would prove pairing, i.e. render the pairing axiom redundant! 

Proof. We first prove that if x is a set then x subnumerouse to x. 
Now each y in x is subnumerouse to the the transitive closure of the bound b on x, 
now if y is empty then {y}=1 which is bounded by 0 thus a set, if y is non empty then
b is non empty then {y} would be subnumerouse to TC(b), thus {y} hereditarily
subnumerouse to TC(b),thus the class {{y}| y in x} would be bounded by b thus a set, 
thus the class {{{y}}| y in x} would exist and this is the identity map from x to x thus
x subnumerouse to itself! 

So every subclass of a set is subnumerouse to that set. Accordingly each set is 
hereditarily subnumerouse to its transitive closure. 

Now we prove the power set axiom in the ordinary manner stipulated above. 

Now take any two  distinct sets x,y we have the class K={PP(TC(x)) , PP(TC(y))} 
being a bound on the class {x,y}, the reason is that we'll be having 
(PP(TC(x)),0) and (PP(TC(y)),{0}) as sets! since those are clearly subsets 
of PPPP(TC(x)) and PPPP(TC(y)) respectively. So we'll be having the class 
{(PP(TC(x)),0) , (PP(TC(y)),{0})} which constitutes an injective map from K 
to each of its elements (it is clear that any double power would contain both 
0 and {0} as elements of), and clearly each set s whatsoever is hereditarily 
subnumerouse to the transitive closure of PP(TC(s)), thus K constitutes a bound 
on {x,y}, thus {x,y} is a set. If x=y then {TC(x)} would constitute a bound
on {x} if x is non empty, if x is empty then {0} is bounded by 0.

Zuhair