This question is about synonymy of $\sf ZFC$ set theory 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 *total* 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$

*Define:* $x \ O \ y \iff \exists z: z \subseteq x \land z \subseteq y$

**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  $

 

*Define:* $ x= \lceil   a \mid \varphi \rceil \iff \forall  \operatorname {atom}  a \, (a \subseteq x \leftrightarrow \exists y: \varphi(y) \land a \subseteq y) $

*Define:* $x=\lceil a_1,..,a_n \rceil \iff  \forall  \operatorname{atom} y \, (y \subseteq x \leftrightarrow y=a_1 \lor .. \lor y=a_n ); \\\text{ if } a_1,..,a_n \text { are atoms}$

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

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

 
**Start:** $\exists a \exists b \exists c: a=\{a\} \land b\neq a \land c= \lceil a,b \rceil   \land b=\{c\}$

**Foundation:** $ \exists a \exists b \forall h: \forall x \, ( \{x\} \subseteq h \to x \ O  \ h ) \to a \subseteq h \lor b \subseteq h$

*Define:* $x=\mathcal A \iff x=\{x\} \\  x=\mathcal B \iff x \neq \{x\} \land x=\{\lceil \mathcal A, x\rceil \}$

So, we have: $\mathcal A=\{\mathcal A\}\\ \mathcal B= \{\lceil \mathcal A, \mathcal B \rceil\}$


**Replacement:** $\varphi(a,b) \land \varphi (a,c) \to b=c   \\ \land   \exists A: A= \lceil  { a \mid \exists b: \varphi(a,b)}\rceil  \\ \to \\ \exists B: B= \lceil b \mid \exists a: \varphi(a,b) \rceil; \\ \text { if } B \text { doesn't occur in } \varphi    $

   


**Infinity:** $\exists x: x \neq \mathcal A \land \forall y: \{y\} \subseteq x \to \{\{y\}\} \subseteq x$

**Choice:** $\forall x  \exists C \forall y \in x: \{C(y)\} \subseteq y$

This theory does not violate any of the tenets of Mereology, though it doesn't adopt the Unrestricted Composition principle. 

Define set membership $\in$ as:

$$x \in y \iff \{x\}  \subseteq y $$

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 MZFC$", standing for "Mereological $\sf ZFC$". 

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

> Is this system synonymous with $\sf MZFC$ and with $\sf ZFC$?


> Is this system minus Choice synonymous with $\sf ZF$?

 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]", but the global choice function there played a significant role in the synonymy. Here, we don't have global choice. Also, the Mereological theory presented is a modification of the theory presented in an [earlier][2] posting to suit withdrawal of proper classes, and also to suit making the starting atoms definable. The idea is that the definability of the starting atoms $\mathcal A, \mathcal B$ may enable us to achieve synonymy even in absence of global choice, and possibly even in absence of axiom of choice.

 

 


 


  [1]: https://mathoverflow.net/q/462747/95347
  [2]: https://mathoverflow.net/q/462852/95347