Can rules of set theory be founded by paralleling parts of atomic Mereology?

Question

If we work in General Extensional Atomic Mereology [without bottom], so the primitives of the language are $P$ standing for "is a part of", and equality, now we add to it membership $\in$ relation symbol.

I observed that all rules of $\text{ZF}$ can be derived from the following Mereology-Set translation rule:

If $\phi$ is a formula in the pure language of mereology (only uses $P$ and $=$ as predicates) in which the symbol $x$ doesn't occur free, and such that all quantifiers in it are restricted to atoms (i.e. of the form $\forall x (\operatorname{atom}(x) \to\cdots)$, or $\exists x (\operatorname{atom}(x) \wedge\ldots)$, these denoted as $\forall ^* x (\cdots)$ and $\exists^* x(\ldots)$ respectively), and in which only symbols $y$, $p_1$, …, $p_n$ occur free, and if $\phi^{\in}$ is the formula obtained from $\phi$ by merely replacing each occurrence of the symbol $P$ by $\in$ and the symbols $\forall^*$, $\exists^*$ by symbols $\forall$, $\exists$ respectively, then:

$$[\forall^* p_1,\dotsc, \forall^* p_n \exists k (\operatorname{atom}(k) \wedge \forall y (\phi(y) \to y=k)] \to \forall p_1,\dotsc,\forall p_n \exists x \forall y (y \in x \leftrightarrow \phi^{\in})$$

is an axiom.

Now take the formulas: $$y=p_1,$$ $$\exists^* z \ (z \ P \ p_1 \wedge y\ P \ z),$$ $$\forall^* z \ (z \ P \ y \to z \ P \ p_1),$$ $$\exists^* x \ P \ p_1 [ \phi(x,y)], \quad\text{where}\quad\forall^* x \ P \ p_1 \ \exists^*! y (\phi(x,y)), $$ $$\forall^* I (p_1 \ P \ I \wedge \forall^* m \ P \ I (\exists^* n \ P \ I (\forall^*z \ P \ n \leftrightarrow z=m)) \to y \ P \ I) $$

All of the above formulas fulfill the hypothesis of the above schema and so the consequence would be axioms of Singletons, Set Union, Power, Replacement, and Infinity. Which are all the constructive axioms of $\text{ZF}$, except empty set, which can be simply added.

Of Note is that the known paradoxes of Cantor's, Russell's, Burali-Forti, Mirimanoff, and Lesniewski's, all are avoidable here.

I'm not really sure if that schema is consistent, but the idea is that it reflects a certain relationship between atomic Mereology and set theory, all axioms of set theory can be viewed as in some sense paralleling or rather mimicking the atomic part-hood relation of Mereology. So membership relation can be viewed as a kind of a binary relation between atoms and sets themselves are viewed as atoms.

Has such forms of mimicry between pieces of Mereology and Sets been considered before, especially along lines of setting some Mereological basis for deriving rules of set theory?

Answer 1

Many people find it natural to consider the set-theoretic analogue of mereology to be the inclusion relation $\subseteq$ rather than $\in$, since after all, $\subseteq$ is reflexive and transitive and admits relative complements, and these are all axioms listed on the mereology page to which you link, but $\in$ does not have these features. (For this reason, I am a little unsure about what you are trying to do with your translation of the part-hood relation as $\in$, since this seems flawed in many ways.)

If one does proceed with $\subseteq$ as the basis of set-theoretic mereology, then there is a bit of literature.

David Lewis, for example, in his 1991 book Parts of Classes outlines an approach to mereology by which the parthood relation is understood as $\subseteq$ in a system of class theory similar to Gödel-Bernays, and Lewis's system satisfies many of the axioms on the list itemized in the article to which you link.

More recently, I've written a few articles:

• Hamkins, Joel David; Kikuchi, Makoto, Set-theoretic mereology, Logic and Logical Philosophy 25, No. 3, 285-308 (2016). Doi:10.12775/LLP.2016.007, ZBL1369.03047.

• Hamkins, Joel David; Kikuchi, Makoto, The inclusion relations of the countable models of set theory are all isomorphic, arxiv:1704.04480, 2017.

Kikuchi and I undertake to analyze the nature and strength of what we call set-theoretic mereology, which is the study of the subst $\subseteq$ relation as it arises in ZFC set theory. Given a model of set theory $\langle V,\in\rangle\models\text{ZFC}$, we consider the definable reduct of this structure to the subset relation $\langle V,\subseteq\rangle$. Among other things, we prove that $\in$ is not definable from $\subseteq$ and that the theory of $\langle V,\subseteq\rangle$ is decidable — it is the theory of an unbounded atomic relatively complemented distributive lattice, and this is a finitely axiomatizable complete theory. Furthermore, we prove that all countable models of ZFC have isomorphic reducts to the subset relation. This is a sense in which set-theoretic mereology doesn't know any set theory, since it can't tell whether CH holds or fails, whether there are large cardinals or not, or ultimately, we prove, even whether there are infinite sets or not.

One philosophical point we make is that these results can be understood as an explanation of why there has been no successful implementation of set-theoretic mereology as a foundation of mathematics. Namely, one cannot use a decidable theory as a foundation of mathematics, since such a theory is not capable of serving as a foundation for the undecidable parts of mathematics, including arithmetic.

You can see more discussion of this at:

• The MathOverflow question, Why hasn't mereology succeeded as a foundation of mathematics?
• Various posts in the mereology tag on my blog, which includes the articles above as well as various other expository posts I've made and the mereology talks I've given.

Meanwhile, let me mention that if you augment $\subseteq$ with the singleton operator $a\mapsto\{a\}$, then you can easily recover the $\in$ relation via $x\in y\leftrightarrow \{x\}\subseteq y$, and so mereology-with-singleton-operator is bi-interpretable with $\in$-based set theory.