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