Reformulation of Morse-Kelley set Theory

Language: Mono-sorted First order logic

Primitives: =, e

"in" will be used in a synonymous manner to e.

Define: set(x) <-> Ey (x e y) 

1.Extensionality: Az(z e x <-> z e y) -> x=y 

2.Class comprehension: if phi is a formula in which x do not occur free, 

then all closures of: 

Ex Ay (y e x <-> set(x) ^ phi) 

are axioms. 

3.Size: y subnumerous_to x ->[set(Ux) -> set(y) ^ set(Uy)] 

4.Infinity: There exists an infinite set. 

Definitions: 

x subnumerous_to y <-> x=y or Ef(f:x-->y ^ f is injective), 

Ux means the class union of x defined in the customary manner. 

/Theory definition finished. 

Proof: 

Theorem 1. Exist x (set(x)). 

Proof: Axiom 4. 

Theorem 2. Set(x) -> Set({x}) 

proof: 

U{x}=x, we have Set(x) and 

Since {x}={x} (ID) so 

{x} equinumerous to {x} by definition 

thus set({x}) [Axiom.3]. 

Theorem 2. Set(0) 

Proof: 0 is subnumerous to any singleton set 

Any singleton set is a class whose union is a set! 

So 0 is a set. [Axiom.3]. 

Theorem 3. Set(Ux) -> Set(x) 

Proof: x=x thus x equinumerous to x 

we have Set(Ux), thus Set(x). [Axiom.3] 

Theorem 4. Set ({x,y}) 

if x=y then {x,y}={x} thus set({x,y}) [Th.2] 

If y=0 then {x,y}={x,0}, now U{x,0}= x 

Since x is a set then {x,0} is a set. [Th.3] 

Same applies if x=0. 

if x=y and ~x=0 and ~y=0, then 

we have U{{x},{x,0}}= {x,0} 

Since set({x,0}) thus set({{x},{x,0}}). [Th.3] 

so we have set((x,0)) where "(,)" is the Kuratowski ordered pair (by definition). 

From Th.2 and this result and Axiom 2, we have the class {(x,0),(y,y)} 

which is an injection from {x,y} to {0,y} (by definition) and since 

U{0,y} is a set thus {x,y} is a set. [Axiom 4]   

Theorem 5. Set(x) -> Set(Px) 

Proof: UP(x)=x, we have Set(x) then Set(Px). Th.3 

Theorem 6. Set(x) -> Set(Ux) 

Proof: x equinumerous to the class x"={{y}| y in x} 

since already have Ux"=x and Set(x) thus Set(Ux). [Axiom 4] 

Theorem 7. x subset_of y ^ set(y) -> set(x) 

Proof: the identity function on x would be an injection 

from x to y and since U(y) is a set (Th.6) then x is a set. [Axiom 4] 

Theorem 8. x subnumerous to y ^ set(y) -> set(x) 

Proof: we have U(y) is a set [Th.6] then set(x). [Axiom 4] 

Thus all axioms of ZF-Regularity are provable here.

Another version of the size axiom is:

 3. Size: Ay [y in V <-> Ex (y =< x ^ Ux < V)] 

Where V is the class of all sets. 

Where < denotes 'strict subnumerousity' defined as: 

x < y <-> x =< y ^ ~ y =< x. 

x =< y <-> x subset_of y or Ef(f:x-->y ^ f is injective) 

In English a set is what is subnumerous to a class whose union is strictly subnumerous to the class of all sets. 

This axiom would prove also all constructive axioms of ZF, as well it will also prove Global choice. 

Proof: 

Theorem.1: x in V ^ y subset_of x -> y in V 

Proof: x in V -> Exist z (x =< z ^ Uz < V) 

now fix such a set z. Since y is a subset of x then y =< z also, thus y is a set [Axiom 3] 

Theorem.2: x in V -> x < V 

Proof: from Th.1 and Axiom 2 we have the class Px,   

now x subset_of V but Px is not injective to x, so V 

is not injective to x and of course V is not a subset_of x 

thus x < V. 

Theorem 3. x in V -> Px in V 

Proof: x in V -> x < V Th.2 

Now UPx=x, and Px =< Px 

so Px in V.[Axiom 3] 

Theorem.4: Singleton(x) -> x in V 

Proof: x is subnumerous to itself 

and Ux in V since Ux is the sole member of x. 

so Ux < V [Th.2], so x in V [Axiom 3]. 

Theorem.5: {x,y} in V. 

Proof: similar to the proof of pairing in the theory in the head post. 

Theorem 6. x < V -> x in V 

Proof: take the set x" of all singletons of elements of x 

so x is subnumerous to x" 

Ux"=x, and since x in V -> x < V 

thus x in V. {Axiom 3]. 

Theorem 7. x in V <-> x < V 

Proof: Th.2,6 

Theorem 8. 0 in V 

Proof: From infinity we have V is non empty 

so we have 0 subnumerous to V and V not subnumerous to 0 

so 0 < V. Now 0 subnumreous to 0, and U0=0, so 0 in V. [Axiom.3]

Theorem 9: On =< V

where ON is the set of all ordinal numbers.

Proof: If ON < V , we have ON is equinumerous to itself

and UON=ON then it follows that ON in V [Axiom 3]

but ON in V will raise Burali-Forti paradox. (von Nuemann 1928)  

Theorem 10. x in V -> Ux in V 

Proof: Since the above theorems are proved then all axioms MK class theory 

are proved, and that proves set Union. (Azriel Lévy 1968 )

Another reformulation of size limitation that is inspired directly by a mereological foundation of set theory is the following axiom.

U(Z) = X ^ Z =< P(Y) ^ Set(Y) -> Set(X)

This coupled with Pairing would interpret Union, Power , Separation and Replacement.

(addendum (7/2/2018)): there is another approach related to the last of what is present in page the essence of sets in this site: The Essence of Sets

Here this would be:

x equinumerous to y -> [Set(x) <-> Exist z (Set(z) ^ U(y)  C  z)]

where x equinumerous to y <-> x=y or there is an injection from x to y and an injection from y to x.

where C is the known sub-class relation

This would also prove all constructive axioms of ZF.

Proof:

theorem: Set(x) ^ y C x -> Set(y)

Proof: Since x is a set, then Ez(Set(z) ^ U(x)Cz)

Since y C x, then U(y) C U(x), thus

Ez (set(z) ^ U(y)Cz), But y equinumerous y

thus y is a set (above axiom)

theorem: Set(x) -> Set(U(x))

Proof: we have x equinumerous x

and Set(x), then by above axiom

Exist z (set(z) ^ U(x)Cz)

thus U(x) is a set! (above theorem)

theorem: Set(x) -> Set(P(x))

Proof: we have P(x) equinumerous P(x)

But U(P(x))=x, and we have Set(x), and since

every set is a subset of itself, then there exists

a set such that U(P(x)) is a subset of namely x itself.

so P(x) is a set! [above axiom]

theorem: Set(x) ^ x equinumerous y -> Set(y)

Proof: Since Set(x), then Set(Ux), since U(x) C U(x)

and y equinumerous to x, thus Set(y)! [Above axiom]

theorem: full replacement

Proof: since injective replacement above works then

it with separation easily prove full replacement.

theorem: Pairing

Proof: full replacement.

Zuhair