Set-theoretic mereology: the theory of the subset relation is decidable

In this post I’d like to explain a certain aspect of my on-going project with Makoto Kikuchi on set-theoretic mereology, which is set theory, undertaken in the full set-theoretic universe $V$, but using only the inclusion (subset) relation $\newcommand\of{\subseteq}\of$, rather than the element-of relation $\in$.  (See my earlier post, Different models of set theory with the same subset relation) The subset relation is of course a partial order and indeed a lattice order, since any two sets $a$ and $b$ have a least upper bound, the union $\newcommand\union{\cup}a\union b$, and a greatest lower bound, the intersection $\newcommand\intersect{\cap}a\intersect b$. Furthermore, the lattice has a least element $\emptyset$, but no greatest element, and for any set $a$, the collection of sets with $\emptyset\of b\of a$ forms an atomic Boolean algebra.Venn_Diagram_of_sets_((P),(Q),(R))To assist with the analysis, let’s work a bit more generally. Recall that a partial order is a lattice order, if any two elements have a least upper bound (join) and greatest lower bound (meet), which I shall denote by $a\union b$ and $a\intersect b$, respectively, since I am interested in the set-theoretic cases; similarly, I’ll denote the order by $a\of b$. Let me define that a lattice is locally Boolean, if there is a least element $0$, and for every $a$, the interval $[0,a]$ is a Boolean algebra. Such a lattice is unbounded, if there is no maximal element. In such a lattice, an atom is a non-zero element that is minimal above $0$, and the lattice is atomic, if every element is the least upper bound of the atoms below it. For each natural number $n$, let us introduce the unary predicate denoted $|x|\geq n$, which expresses that $x$ admits a decomposition as the join of $n$ distinct nonzero incompatible elements: $x=y_1\union\cdots\union y_n$, where $y_i\neq 0$ and $y_i\intersect y_j=0$ for $i\neq j$. In an atomic locally Boolean lattice, the relation $|x|\geq n$ holds just in case there are at least $n$ atoms $a\leq x$.

To give a few examples, if $\newcommand\HF{\text{HF}}\HF$ is the set of hereditarily finite sets, then $\langle\HF,\of\rangle$, using the usual subset relation, is an unbounded atomic locally Boolean lattice. More generally, if $V$ is any model of set theory (even a very weak theory is sufficient), then $\langle V,\of\rangle$ is an unbounded atomic locally Boolean lattice.

I should like to prove here that the theory of unbounded atomic locally Boolean lattice orders is decidable, and furthermore admits elimination of quantifiers down to the language including the Boolean operations and the relations expressing the height or size of an object, $|x|\geq n$ and $|x|=n$.

Theorem. Every formula in the language of lattices is equivalent, over the theory of unbounded atomic locally Boolean lattices, to a quantifier-free formula in the language of the order $a\of b$, equality $a=b$, meet $a\intersect b$, join $a\union b$, relative complement $a-b$, constant $0$, the unary relation $|x|\geq n$, and the unary relation $|x|=n$, where $n$ is respectively any natural number.

Proof. We prove the result by induction on formulas. The collection of formulas equivalent to a quantifier-free formula in that language clearly includes all atomic formulas and is closed under Boolean combinations. So it suffices to eliminate the quantifier in a formula of the form $\exists x\, \varphi(x,\ldots)$, where $\varphi(x,\ldots)$ is quantifier-free in that language. Let us make a number of observations that will enable various simplifying assumptions about the form of $\varphi$.

Because equality of terms is expressible by the identity $a=b\iff a\of b\of a$, we do not actually need $=$ in the language (and here I refer to the use of equality in atomic formulas of the form $s=t$ where $s$ and $t$ are terms, and not to the incidental appearance of the symbol $=$ in the unary predicate $|x|=n$, which is an unrelated use of this symbol, a mere stylistic flourish). Similarly, in light of the equivalence $a\of b\iff |a-b|=0$, we do not need to make explicit reference to the order $a\of b$. So we may assume that all atomic assertions in $\varphi$ have the form $|t|\geq n$ or $|t|=n$ for some term $t$ in the language of meet, join, relative complement and $0$. We may omit the need for explicit negation in the formula by systematically applying the equivalences:
$$\neg(|t|\geq n)\iff \bigvee_{k<n}|t|=k\quad\text{ and}$$
$$\neg(|t|=n)\iff (|t|\geq n+1)\vee\bigvee_{k<n}|t|=k.$$
So we have reduced to the case where $\varphi$ is a positive Boolean combination of expressions of the form $|t|\geq n$ and $|t|=n$.

Let us consider the form of the terms $t$ that may arise in the formula. List all the variables $x=x_0,x_1,\ldots,x_N$ that arise in any of the terms appearing in $\varphi$, and consider the Venn diagram corresponding to these variables. The cells of this Venn diagram can each be described by a term of the form $\bigwedge_{i\leq N} \pm x_i$, which I shall refer to as a cell term, where $\pm x_i$ means that either $x_i$ appears or else we have subtracted $x_i$ from the other variables. Since we have only relative complements in a locally Boolean lattice, however, and not absolute complements, we need only consider the cells where at least one variable appears positively, since the exterior region in the Venn diagram is not actually represented by any term. In this way, every term in the language of locally Boolean lattices is a finite union of such cell terms, plus $\emptyset$ (which I suppose can be viewed as an empty union). Note that distinct cell terms are definitely representing disjoint objects in the lattice.

Next, by considering the possible sizes of $s-t$, $s\intersect t$ and $t-s$, observe that
$$|s\union t|\geq n\iff \bigvee_{i+j+k=n}(|s|\geq i+j)\wedge(|s\intersect t|\geq j)\wedge(|t|\geq j+k).$$
Through repeated application of this, we may reduce any assertion about $|t|$ for a term to a Boolean combination of assertions about cell terms. (Note that size assertions about $\emptyset$ are trivially settled by the theory and can be eliminated.)

Let us now focus on the quantified variable $x$ separately from the other variables, for it may appear either positively or negatively in such a cell term. More precisely, each cell term in the variables $x=x_0,x_1,\ldots,x_N$ is equivalent to $x\intersect c$ or $c-x$, for some cell term $c$ in the variables $x_1,\ldots,x_N$, that is, not including $x$, or to the term $x-(x_1\union\cdots\union x_N)$, which is the cell term for which $x$ is the only positive variable.

We have reduced the problem to the case where we want to eliminate the quantifier from $\exists x\, \varphi$, where $\varphi$ is a positive Boolean combination of size assertions about cell terms. We may express $\varphi$ in disjunctive normal form and then distribute the quantifier over the disjunct to reduce to the case where $\varphi$ is a conjunction of size assertions about cell terms. Each cell term has the form $x\intersect c$ or $c-x$ or $x-(x_1\union\cdots x_N)$, where $c$ is a cell term in the list of variables without $x$. Group the conjuncts of $\varphi$ that use the same cell term $c$ in this way together. The point now is that assertions about whether there is an object $x$ in the lattice such that certain cell terms obey various size requirements amount to the conjunction of various size requirements about cells in the variables not including $x$. For example, the assertion $$\exists x\,(|x\intersect c|\geq 3)\wedge(|x\intersect c|\geq 7)\wedge(|c-x|=2)$$ is equivalent (over the theory of unbounded atomic locally Boolean lattices) to the assertion $|c|\geq 9$, since we may simply let $x$ be all but $2$ atoms of $c$, and this will have size at least $7$, which is also at least $3$. If contradictory assertions are made, such as $\exists x\, (|x\intersect c|\geq 5\wedge |x\intersect c|=3)$, then the whole formula is equivalent to $\perp$, which can be expressed without quantifiers as $0\neq 0$.

Next, the key observation of the proof is that assertions about the existence of such $x$ for different cell terms in the variables not including $x$ will succeed or fail independently, since those cell terms are representing disjoint elements of the lattice, and so one may take the final witnessing $x$ to be the union of the witnesses for each piece. So to eliminate the quantifier, we simply group together the atomic assertions being made about the cell terms in the variables without $x$, and then express the existence assertion as a size requirement on those cell terms. For example, the assertion $$\exists x\, (|c\intersect x|\geq 5)\wedge(|c-x|=6)\wedge (|d\intersect x|\geq 7),$$ where $c$ and $d$ are distinct cell terms, is equivalent to $$(|c|\geq 11)\wedge(|d|\geq 7),$$ since $c$ and $d$ are disjoint and so we may let $x$ be the appropriate part of $c$ and a suitable piece of $d$. The only remaining complication concerns instances of the term $x-(x_1\union\cdots\union x_N)$. But for these, the thing to notice is that any single positive size assertion about this term is realizable in our theory, since we have assumed that the lattice is unbounded, and so there will always be as many atoms as desired disjoint from any finite list of objects. But we must again pay attention to whether the requirements expressed by distinct clauses are contradictory.

Altogether, I have provided a procedure for eliminating quantifiers from any assertion in the language of locally Boolean lattices, down to the language augmented by unary predicates expressing the size of an object. This procedure works in any unbounded atomic locally Boolean lattice, and so the theorem is proved. QED

Corollary. The theory of unbounded atomic locally Boolean lattices is complete.

Proof. Every sentence in this theory is equivalent by the procedure to a quantifier-free sentence in the stated language. But since such sentences have no variables, they must simply be a Boolean combination of trivial size assertions about $0$, such as $(|0|\geq 2)\vee \neg(|0|=5)$, whose truth value is settled by the theory. QED

Corollary. The structure of hereditarily finite sets $\langle\HF,\of\rangle$ is an elementary substructure of the entire set-theoretic universe $\langle V,\of\rangle$, with the inclusion relation.

Proof. These structures are both unbounded atomic locally Boolean lattices, and so they each support the quantifier-elimination procedure. But they agree on the truth of any quantifier-free assertion about the sizes of hereditarily finite sets, and so they they must agree on all truth assertions about objects in $\HF$. QED

Corollary. The structure $\langle V,\of\rangle$ has a decidable theory. The structure $\langle\HF,\of\rangle$ has a decidable elementary diagram, and hence a computably decidable presentation.

Proof. The theory is the theory of unbounded atomic locally Boolean lattices. Since the structure $\langle\HF,\of\rangle$ has a computable presentation via the Ackerman coding of hereditarily finite sets, for which the subset relation and the size relations are computable, it follows that we may also compute the truth of any formula by first reducing it to a quantifier-free assertions of those types. So this is a computably decidable presentation. QED

6 thoughts on “Set-theoretic mereology: the theory of the subset relation is decidable

  1. I can’t help but mention a little bit about how these facts fall in the more general framework of elementary classes of Boolean algebras, their decidability, and generalizations. The elementary classes of Boolean algebras have been completely classified by Tarski according to his Tarski invariants and the relatively complemented Boolean algebras have a similar classification due to Ershov in a Russian paper (I have not read any of the details for relatively complemented distributive lattices but I would imagine that one uses the elementary classes of the initial segments of the relatively complemented distributive lattices with 0 to characterize the elementary class of the entire Boolean algebra). Furthermore, Ershov has shown that the theory of relatively complemented Boolean algebras is a decidable theory. The model theory book by Chang and Keisler and the Handbook of Boolean algebras both develop the theory of these Tarski invariants of Boolean algebras.

    • Thanks, Joseph. I had assumed that this was how the Boolean algebra result went, and I asked model theorists all around, but nobody could tell me where to find it, so I just did it myself. (I had looked in Hodges and also Chang-Keisler, but evidently missed it there.) I have now learned about the Ershov result also from Makoto (and I think you mean relatively complemented distributive lattices), and clearly that is where the credit is due.

  2. Each time that I see set theoretic structures endowed with $\subseteq$ instead of $\in$ as a topic of study, I can’t resist against asking some questions about the philosophy behind studying such relations/structures!

    1) What makes us interested in studying a particular relation or structure in set theory (or in general in mathematics)? Maybe its “naturality” or its “nice applications in or out of mathematics”. Perhaps its “rich and beautiful theory”.

    2) Regardless to any answer to this question, one should be prepared for another question like: What do you mean by “naturality”, “nice applications” or “rich theory” associated to a particular structure?

    The difficulty of answering the second question is that one should define them in such a way that match the common sense of mathematicians about the importance of some particular structures like $\mathbb{N}$ as a model of Peano Arithmetic or $\mathbb{R}$ as a model of Real Closed Fields.

    3) Localizing the previous questions to the case of this research project: what can one say if a mathematician from another discipline, say a category theorist, asks us (set theorists) about the importance or necessity of studying $\langle V, \subseteq\rangle$? Should your paper be accompanied by another paper investigating the philosophy behind studying this particular structure? Or it is too soon to see what would happen in this field, “Set Theoretic Mereology”?

    For those who are not familiar with the term one should remind that it is not new! A brief information about the history of mereology together with a good collection of references to the topic could be found here:

    https://en.wikipedia.org/wiki/Mereology

    4) All these discussions about structures in set theory somehow reminds me the recent discussion that Qiaochu Yuan brought up in MSE:

    http://math.stackexchange.com/questions/1519330/is-it-possible-to-formulate-category-theory-without-set-theory/1519338#1519338

    Personally despite of my willingness to provide a response when Qiaochu Yuan criticized set theory and set theorists I preferred not to do so because I think “the best way to convince everybody that an idea is false is to defend it via weak reasons!”, that is what happened when some people rushed to set theory’s defence after Qiaochu’s post.

    Anyway it is not just Qiaochu’s words. I have heard many critical comments from category theorists, algebraic geometrists and even model theorists regarding “set theorists’ lack of intuition about the notion of structure and its importance. And that they are not paying enough attention to the relation between structures.”

    So the last question is: what can we say to such people criticizing us? Are we really missing something about the structures in mathematics?

    It would be very nice if we hear from you a thorough response to issues raised by people like Qiaochu in the “Set Theory vs. Category Theory” intuition war, say in a philosophical article, or lecture or a blog post.

  3. Pingback: Set-theoretic mereology | Joel David Hamkins

  4. Dear Joel,

    Another observation is that you can permit the bounds that you used in quantifier elimination to be variables, which establishes a nice connection with Presburger arithmetic, see, in particular, the beginning of Section 6 here:

    Viktor Kuncak, Huu Hai Nguyen, and Martin Rinard. Deciding Boolean Algebra with Presburger Arithmetic. Journal of Automated Reasoning, 36(3), 2006.

    http://lara.epfl.ch/~kuncak/papers/KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic.pdf

    Another nice connection of viewing elements as singleton sets is that you can use results on Boolean algebras to show decidability of monadic class of first-order logic, which in turn is related to set constraints, see this paper that also clarifies that the result dates to Loewenheim 1915 and simplified by Ackermann in his book:

    L. Bachmair, H. Ganzinger and U. Waldmann, “Set constraints are the monadic class,” Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, QC, Canada, 1993, pp. 75-83, doi: 10.1109/LICS.1993.287598.

    https://doi.org/10.1109/LICS.1993.287598

Leave a Reply