This question is about synonymy between Set theory and Mereology. 

David Lewis in [Mathematics is Megethology][1] tried to reduce Set Theory to Mereology augmented with a singleton function. The following exposition is a formal capture of his Mereology. 

Lets define a mereological theory $\sf M$ in mono-sorted first order logic with identity, add primitives of *part-hood* "$P$", and the partial unary function "$\mathfrak L $", denoting "*is the lable of*". Add the following axioms:

***Mereological Axioms:***

***M1*** $\textbf{Anti-symmetry: }X \ P \ Y \land Y \ P \ X \to X=Y$

***M2*** $\textbf{Bottom: }\exists X \forall Y: X \ P \ Y$

***Define:*** $X = \varnothing \iff \forall Y: X \ P \ Y$
 
***Define:*** $ X \ PP \ Y \iff X \ P \ Y \land \neg (Y \ P \ X)$

***Define:*** $atom(X) \iff \forall Y: Y \ PP \ X \to Y=\varnothing$

***Define:*** $ X\ P^*\ Y \iff atom(X) \land X \ P \ Y$

***M3*** $\textbf{Atomism: } \forall X (X \ P^* \ Y \to X \ P^* Z) \leftrightarrow Y \ P \ Z$

***M4*** $\textbf{Composition: }\\ \exists X \forall Y \ (Y \ P^* \ X \leftrightarrow Y=\varnothing \lor [atom(Y) \land \psi] ); \text{ if } X \text { is not free in } \psi $

***Define:*** $X = \bigl[Y \mid \psi \bigr] \iff \forall Y \ (Y \ P^* \ X \leftrightarrow Y=\varnothing \lor [atom(Y) \land \psi] )$

***Labeling Axioms***

***L1*** $\textbf{Labeling: } \mathfrak L (X)=\mathfrak L (Y) \to X=Y$

***L2*** $\textbf{Purity: } \exists X \ (\mathfrak L(X)=Y)  \leftrightarrow atom(Y) \land Y \neq \varnothing$

***L3*** $\textbf{Replacement: } \text  { if } \psi(X,Y) \text { is a formula, then: } \\ \forall X \neg \exists^{>1} Y: \psi(X,Y), \land   \\ B= \bigl[K \ P^* \ Y \mid \exists V (V=\mathfrak L(Y) \lor Y=\mathfrak L(V)) \land \exists X \ P \ A \ :\psi(X,Y)\bigr] \land \\\exists Z: \mathfrak L(A)=Z \\\to\\\exists Z: \mathfrak L(B)=Z $

***L4*** $\textbf{Infinity: } \exists I  \exists X: \forall Y    \ P^* \ X \bigl(\exists Z \ P \ X: \mathfrak L(Y)=Z \bigr) \land \mathfrak L (X)=I  $

/

In David Lewis account he didn't round the system with a bottom object, so a modified version of his system would be captured by $\sf M$-$\sf Bottom$ which is obtained here by removing $\sf Bottom$ axiom, re-defining atoms as objects devoid of proper parts, and stipulating the existence of a unique non-labeling atom $\varnothing$. 


> Is theory $\sf M$ synonymous with "$\sf MK$ sans **Foundation** sans **Choice**"?

> Is $\sf M$-$\sf Bottom$ bi-interpretable with "$\sf MK$ sans **Foundation** sans **Choice**"?

My plan is to keep equality, and to identify part-hood $P$ with subset-hood relation $\subseteq$, and the labeling function $\mathfrak L$ with the singleton function $X \mapsto \{X\}$; and on the other hand to define $\in$ as: $X \in Y \iff \exists K \ P \ Y: \mathfrak L (X)=K$. 

This way we come to identify classes with mereological totalities, and sets with labeled mereological totalities. All of this is following Lewis's own specifications. However, seeing that Lewis in his "[Mathematics is Megethology][1]" doesn't agree to Bottom axiom, it appears to me that without this axiom the whole Ontology would be plagued with Ur-elements, and so it appears to be so hostile to Extensionality, that I think synonymy with Set Theory cannot be achieved. However, the weaker requirement of bi-interpretability might be possible?


  [1]: https://www.andrewmbailey.com/dkl/Mathematics_is_Megethology.pdf