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