Underneath sets

Labeled-Mereological system have the capability of interpreting all axioms of ZF-Infinity set theory. 

Language: first order logic 

Extra-logical primitives: equality "="; Part-hood "P"; Labeling "L", 

where x P y is read as: x is a part of y, and x L y is read as x is a label of y. 

Axioms: ID axioms + 

1. Transitive: for all x,y,z: x P y ^ y P z -> x P z 

2. Anti-symmetric: for all x,y: x P y ^ y P x -> x=y 

3. Reflexive: for all x: x P x 

Define: atom(x) <-> for all y (y P x -> x=y) 

Define: x atom_of y <-> atom(x) ^ x P y 

4. Supplementation: ~ x P y -> Exist z (z atom of x ^ ~ z P y) 

5. Composition: if phi is a formula in which x is not free, then 

[(Exist y. phi) -> Exist x for all y (y atom_of x <-> atom(y) ^ phi)] 

is an axiom. 

Defne: x=[y|phi] <-> for all y (y atom_of x <-> atom(y) ^ phi)

6. Atomicity: For all x Exist y: y atom_of x 

7. Distinctiveness: for all x,y,a,b (a L x ^ b L y -> [x=y <-> a=b]) 

8. Simplicity: for all x,y (x L y -> atom(x)) 

9. Excellence: Exist! x (~Exist y: x L y) 

Define: x=O <-> ~Exist y: x L y 

10. Size rule: 

If R is a one-one relation from labeled objects satisfying pi to labeled objects satisfying phi and if the totality of all atoms of labeled objects satisfying phi has a label, then the totality of all atoms of labeled objects satisfying pi has a label. 

11. Binary rule: exist a,b,x,y (a L O ^ b L a ^ x=[O,a] ^ y L x)

/ Theory definition finished 

Define (set): x is a set <-> [x=O or for all y atom of x Exist z (y L z))] 

Define (membership): x E y <-> y is a set ^ Exist z (z atom of y ^ z L x) 

Now it is clear that we have Extensionality over sets. Also Parts of sets are sets also. Now a non empty subset of a set is also a part of that set, but the empty set is not a part of any non empty set. 

Pairing, Union, Power, Separation and Replacement are clearly provable in the above system. 

So ZF-Infinity finds a nice interpretation in Labeled Mereology.

 I'd say that all of the axioms except the size rule axioms are totally justified, they ideally grasp what part-hood and an excellent distinctive labeling impart. However the size rule schema is just a technical fix, it is hard to justify on intuitive grounds. However technically speaking it does sum up things into a shorter statement!  so instead of stipulating union,power and replacement, one can have the above statement summing all of them in one. 

In a class theory like Morse-Kelley, the counterpart of the size rule would be the following:

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

which with pairing would prove Union,Power, Replacement and Separation.

Zuhair