I apologize, if my question seems too elementary for "mathoverflow.net". Let T be a set theory formalized in the classical first order predicate calculus whose atomic formulas are "x is a subset of y" and "x=y". On the other hand, the set theory ZF is formalized in the same type of languagebut its atomic formulas are "x is an element of y" and "x=y". Now the "subset" relation is, of course, definable in terms of the "elementhood" relationbut it is not clear to me whether the converse is really possible. So my question is this. Can a collection of axioms for the theory T be found such that (1) a large part of "naïve" set theory can be derived from these axioms and (2) ZF is interpretable in T?.

2$\begingroup$ Questions about appropriateness can be put to meta.mathoverflow.net. Elementhood is equivalent to subsethood for singletons, and singletonness of $x$ can be defined as $\forall y \subseteq x.(y = x \vee \forall z.(y \subseteq z))$. $\endgroup$ – LSpice Jul 5 '16 at 18:08

2$\begingroup$ If my memory serves me right, this is what mereology is all about. $\endgroup$ – Asaf Karagila Jul 5 '16 at 19:07

3$\begingroup$ @LSpice: I don't think your definition will work. It tells you what a singleton is but doesn't help you extract that singleton's element which is what you would need to define $\in$. $\endgroup$ – Miha Habič Jul 5 '16 at 19:15

5$\begingroup$ This problem was discussed in Hamkins, Kikuchi: Settheoretic mereology. They show that $\in$ is not definable from $\subseteq$ and that the theory of $(V,\subseteq)$ is decidable. $\endgroup$ – Miha Habič Jul 5 '16 at 19:24

2$\begingroup$ @MihaHabič, thanks. I don't understand the issues well enough to know why that's fatal (why can't we just identify elements with singletons, so that there's no 'extract'ion involved?), but I guess the spirit is something like Theorem 2 of the linked paper, which says that different interpretations of membership can give the same subset relation. $\endgroup$ – LSpice Jul 5 '16 at 20:03
Though Hamkins and Kikuchi show that $\in$ is not definable from $\subseteq$ and that the theory of $($$V$, $\subseteq$$)$ is decidable, they also show the following:
What we should like to observe here is merely if we were to expand the language by adding a singleton operator [ $s$: $a$$\mapsto${$a$}, which maps every object to its own singletontheir definition] as well as the inclusion operator $\subseteq$, then we would get a structure that is equally powerful as the usual membershipbased set theory.
Thm 13. Every model of membershipbased set theory $($$V$,$\in$$)$ is interdefinable with the corresponding singletonexpanded mereological model $($$V$,$\subseteq$,$s$$)$.
Proof. For the one direction, we can easily define $\subseteq$ and the singleton operator $s$ using $\in$ as follows:
$u$$\subseteq$$v$ $\leftrightarrow$($\forall$$x$)($x$$\in$$u$$\rightarrow$$x$$\in$$v$)
$y$=$s$($x$)$\leftrightarrow$($\forall$$z$)($z$$\in$$y$$\leftrightarrow$$z$=$x$)
Conversely, we may define $\in$ from $\subseteq$ and $s$ via
$x$$\in$$y$$\leftrightarrow$$s$($x$)$\subseteq$$y$
So the theorem is proved.
Given the above, the following question seems natural:
What's the good of mereology, anyway?
To try to understand the good of mereology from a naive mereological standpoint consider the following thoughtexperiment:
As is wellknown, one can define a linear continuum as follows:
A linear continuum is a linearly ordered set $S$ with the following two properties (this from Wikipedia):
i) $S$ has the leastupperboundproperty [i.e. for every nonempty subset of $S$ with an upper bound has a least upper bound (so in that sense $S$ 'lacks gaps')].
ii) For each $x$ in $S$ and each $y$ in $S$ with $x$$\lt$$y$, there exists $z$ in $S$ such that $x$$\lt$$z$$\lt$$y$.
If one defines $x$,$z$, and $y$ as 'points', one can ask the following two questions:
Is a 'line' the settheoretic union of all of its 'singletons' (i.e. sets of individual points, or 'atoms', that is, can a 'line' be reduced to a set of 'points', i.e 'atoms' and the 'point' is the primary ontological entity), or is the 'line' the primary ontological entity, and the 'point' is to be defined in terms of the 'line' by '$\subseteq$'?
Given Theorem 13 quoted above, the two questions might be considered extensionally equivalent, but a naive mereologist might ask a further question that might not be extensionally equivalent:
Does the notion of "linear continuum" defined above adequately capture the intuitive notion of a line (that is, does the leastupperbound principle adequately assure that a dense, linear order 'lacks gaps'?
In order for it to do so, I believe that a theorist of membershipbased set theory would have to resort to the notion of "Model" in the sense that the only 'points' the linear continuum $S$ would contain are only those elements of $S$ contained in the "Model". On the other hand, the Naive Mereologist (who holds that a 'point' is merely a location on a line and that a line cannot be reduced to a set of 'points') need not do so.
Question: Can a theorist of membershipbased set theory construct a dense linear order satisfying the leastupperbound property that cannot be reduced to a set of elements of any given infinite cardinal $\kappa$ in some model $\mathfrak M$ of $ZFC$ or in a model of some fragment thereof?

$\begingroup$ I think the portion of this answer beginning "given the above" should really be a separate question  I don't think it has direct bearing on this question. (Also, I think it will take some work to make your final question precise  as it stands, it's very unclear to me exactly what it means.) $\endgroup$ – Noah Schweber Jul 6 '16 at 13:45

$\begingroup$ Many thanks for clearing up this question for me once and for all. $\endgroup$ – Garabed Gulbenkian Jul 6 '16 at 20:31

$\begingroup$ @GarabedGulbenkian: I'm glad the answer helped. $\endgroup$ – Thomas Benjamin Jul 6 '16 at 21:34