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 \varphi)$ **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\}$ *Define:* $\operatorname {restricted}(x) \iff \operatorname {atom}(x) \lor \exists l: l=\{x\}$ **Replacement:** $\varphi(a,b) \land \varphi (a,c) \to b=c \\ \varphi(a,b) \to \operatorname{restricted}(a) \land \operatorname {restricted}(b) \\ A = \mathcal S \, a: \exists b \, ( \varphi(a,b) ) \\ B= \mathcal S \, b: \exists a \, ( \varphi(a,b) ) \\ \to \\ \exists l: l=\{A\} \to \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?][1]", and I was hoping that the positive [answer][2] 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$". [1]: https://mathoverflow.net/q/462747/95347 [2]: https://mathoverflow.net/a/462761/95347