# What do the ZFC axioms look like in terms of subset?

I'm reasonably familiar with the ZFC axioms. I know they can be formalized in many different ways. However, I usually see them presented in terms of the elementary "propositional calculus primitives" $\rightarrow$, $\neg$, $\wedge$, $\vee$, $\leftrightarrow$; the "predicate calculus with equality" primitives $\forall$, $\exists$, $=$ ; and the single "set-theoretic primitive" $\in$. Then one usually proceeds to define other set operators like $\subseteq$ (and everything else) in terms of $\in$.

What happens if you instead take $\subseteq$ to be the primitive operator of set theory, and define $\in$ in terms of $\subseteq$?

Obviously we could rewrite any formalization of ZFC by replacing each occurrence $x \in y$ with $\{x\} \subseteq y$, but this would not be the most compact or elegant formulation. For example, it seems to me that Extensionality could best be cast as $x \subseteq y \wedge y \subseteq x \rightarrow x = y$.

Surely someone has studied this question and presented an elegant formalization of ZFC based on $\subseteq$. Where can I find it?

• Can you define $x\in y$ in terms of $\subseteq$? – Asaf Karagila Jun 1 '15 at 5:27
• Equivalently to Asaf's question, given a set $x$, how would you define the set $\{x\}$ without using $\in$? – Zev Chonoles Jun 1 '15 at 5:27
• Set theories based on the notion of part (subset) rather than elementhood can be found by googling mereology. – André Nicolas Jun 1 '15 at 5:54
• I saw an Q&A from MO that $\in$ is not definable from $\subseteq$ before. Hamkins answers it, as far as I remember, but I can't find it. – Hanul Jeon Jun 2 '15 at 2:30

As Noah so kindly mentioned, my work on set-theoretic mereology is exactly about this question. See my recent paper with Makoto Kikuchi:

J. D. Hamkins and M. Kikuchi, Set-theoretic mereology, Logic and Logical Philosophy, special issue “Mereology and beyond, part II”, pp. 1-24, 2016. (click through to the arxiv for pdf)

Abstract. We consider a set-theoretic version of mereology based on the inclusion relation $\subseteq$ and analyze how well it might serve as a foundation of mathematics. After establishing the non-definability of $\in$ from $\subseteq$, we identify the natural axioms for $\subseteq$-based mereology, which constitute a finitely axiomatizable, complete, decidable theory. Ultimately, for these reasons, we conclude that this form of set-theoretic mereology cannot by itself serve as a foundation of mathematics. Meanwhile, augmented forms of set-theoretic mereology, such as that obtained by adding the singleton operator, are foundationally robust.

See more at the blog post, or take a look at the paper itself.

• Thanks! This is exactly what I was looking for with my (admittedly ill-posed) question. – Adam Bliss Sep 3 '16 at 15:07

I just noticed this question; here is the answer by Joel David Hamkins which resolves it (this was mentioned above in the comments by Hanul Jeon). I've made this answer CW since it does not involve any work by me.

Hamkins showed that $(V, \subseteq)$ admits lots of automorphisms. From this, we know that "$\in$" cannot be defined in terms of "$\subseteq$". Why? Well, $(V, \in)$ has no nontrivial automorphisms at all (exercise: first show that any automorphism fixes the ordinals, and then show that it is in fact the identity)! But any automorphism of $(V, \subseteq)$ would also be an automorphism of $(V, \in)$, if "$\in$" were definable from "$\subseteq$" (this is a good exercise in model theory).

• Why don't you count the identity as an automorphism? – YoTengoUnLCD Sep 3 '16 at 1:48
• @YoTengoUnLCD By "isomorphism" I meant "nontrivial isomorphism." – Noah Schweber Sep 3 '16 at 2:22