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

Question

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?

Answer 1

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.

Answer 2

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).