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