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?

  • 8
    $\begingroup$ Can you define $x\in y$ in terms of $\subseteq$? $\endgroup$
    – Asaf Karagila
    Jun 1, 2015 at 5:27
  • 4
    $\begingroup$ Equivalently to Asaf's question, given a set $x$, how would you define the set $\{x\}$ without using $\in$? $\endgroup$ Jun 1, 2015 at 5:27
  • 4
    $\begingroup$ Set theories based on the notion of part (subset) rather than elementhood can be found by googling mereology. $\endgroup$ Jun 1, 2015 at 5:54
  • 1
    $\begingroup$ 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. $\endgroup$
    – Hanul Jeon
    Jun 2, 2015 at 2:30

2 Answers 2


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.

  • 1
    $\begingroup$ Thanks! This is exactly what I was looking for with my (admittedly ill-posed) question. $\endgroup$
    – Adam Bliss
    Sep 3, 2016 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).

  • $\begingroup$ Why don't you count the identity as an automorphism? $\endgroup$ Sep 3, 2016 at 1:48
  • 1
    $\begingroup$ @YoTengoUnLCD By "isomorphism" I meant "nontrivial isomorphism." $\endgroup$ Sep 3, 2016 at 2:22

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .