Can this kind of Mereology be synonymous with Set Theory?

Question

This question is about synonymy of Morse-Kelley set theory "$\sf MK$" with the following Mereological theory:

Language: first order logic with equality. Extra-logical primitives: $\subseteq$ standing for the binary relation "is a part of", and a partial unary function symbol $\{\}$ standing for "is the label of", or can also be read as "is the singleton of".

Extra-logical Axioms:

Parthood: $x \subseteq x \\ x \subseteq y \subseteq x \to x=y \\ x \subseteq y \subseteq z \to x \subseteq z$

Supplmentation: $y\not \subseteq x \to \exists z \subseteq y: \neg z \ O \ x$

Define: $\operatorname{atom}(x) \iff \forall y \subseteq x \, (y=x)$

Atomicity: $\forall x \, \exists \text{ atom } y: y \subseteq x $

Composition: $\exists z: \varphi, \to \exists x \, \forall \text{ atom } y \,( y \subseteq x \leftrightarrow \exists z: \varphi(z) \land y \subseteq z); \text{ if } x \text { is not free in } \varphi$

Define: $(x= \mathcal S \, y: \varphi) \iff \forall \text{ atom } y \,( y \subseteq x \leftrightarrow \exists z: \varphi(z) \land y \subseteq z)$

Labeling: $\{x\}=\{y\} \to x=y$

Purity: $ \exists x \, (y=\{x\}) \leftrightarrow \operatorname{atom}(y)$

Start: $\exists a \, \exists b: a \neq b \land \forall x \,( x=\{x\} \leftrightarrow x=a \lor x = b)$

Foundation: $ \forall x (\exists \{x\} \subseteq h \to x \ O \ h ) \to \exists a \subseteq h: a=\{a\}$

Replacement: $\varphi(a,b) \land \varphi (c,d) \to [a=c \leftrightarrow b=d] \\ \varphi(a,b) \to \operatorname {atom}(a) \land \exists l: l=\{b\} \\ A = \mathcal S \, a: \exists b \, ( \varphi(a,b) ) \\ B= \mathcal S \, b: \exists a \, ( \varphi(a,b) ) \\ \to \\ \exists l: l=\{A\} \leftrightarrow \exists l: l= \{B\} $

Define: ${\sf Q}= \mathcal S \, a: a=\{a\}$

Abundance: $\exists l: l= \{{\sf Q}\}$

Infinity: $\exists x: x \not \subseteq {\sf Q} \land \exists l: l=\{x\} \land \forall y: \{y\} \subseteq x \to \{\{y\}\} \subseteq x$

Choice: $\exists C \, \forall x \, \exists y : y=C(x) \land \exists \{y\} \subseteq x$

This theory does respect all tenets of Mereology, the first four principles are the axioms of Atomic General Extensional Mereology "$\sf AGEM$". Define set membership $\in$ as:

$$x \in y \iff \exists z \subseteq y: z=\{x\} $$

Call the collection of all sentences written in $\sf FOL(=,\in)$ over the whole domain of this theory (i.e. all quantifiers unrestricted) that are provable in this theory as "$\sf MMK$", standing for "Mereological $\sf MK$".

It should be made clear that $\sf MMK$ proves the non-existence of an empty set, minimally breaches Foundation, and that it is fully extensional.

Is $\sf MMK$ synonymous with $\sf MK$?

Is $\sf MK$ synonymous with this theory?

This question is related to the question "Is ZFGC, minimally modified to allow two Quine atoms instead of the empty set, synonymous\bi-interpretable with ZFGC?", and I was hoping that the positive answer to it can be extended to the case here.

Note: "$ O $" stands for the overlap relation (i.e. existence of a common part), and "$\mathcal S \, a: \varphi$" stands for "the sum of all atoms realizing $\varphi$". The expression "$\exists \{x\} \subseteq y$" stands for "$\exists z: z=\{x\} \land z \subseteq y$".

Answer 1

If, for every atom $a$, $a \subseteq x$ implies $a \subseteq y$, then $x \subseteq y$. Assume $x \nsubseteq y$, then by Supplementation, there is a $z \subseteq x$ such that $\neg z \ O \ y$. By Atomicity, there is an atom $a \subseteq z \subseteq x$, and $a \nsubseteq y$ because $\neg zOy$, contradicting the assumption that if $a \subseteq x$ then $a \subseteq y$.

This implies that the usual definition $a \subseteq b \iff \forall x (x \in a \Rightarrow x \in b)$ and your definition of $\in$ from $\subseteq$ are inverses of each other, so it does not matter whether the language is $\in$ or ($\subseteq$, $\{\}$); your mereological theory is synonymous with $\sf MMK$.

MMK and MK are not synonymous. A model of MK has no nontrivial definable automorphisms, but any model of MMK has a definable automorphism by swapping the two Quine atoms. If they were synonymous, then a model of MK would also be a model of MMK (with a different $\in$), and therefore have a nontrivial definable automorphism, which is impossible. (A similar argument might work to prove they are not bi-interpretable, but I'm not sure of the details). So the issue is that we can't distinguish the two Quine atoms. (The reason this argument didn't work in the case of ZFGC was the global choice function $C$, which can be used to pick one of the Quine atoms; in MMK, while choice functions do exist, there isn't a choice of one particular one that an isomorphism has to preserve).

If we add a constant $q$ and the axiom $q \in q$ (so that we can distinguish the Quine atoms), the resulting theory is synonymous with MK, by a similar argument to my previous answer, except we use $q$ to remember which Quine atom was the empty set.