=Paper=
{{Paper
|id=Vol-2710/paper14
|storemode=property
|title=A Quadratic Reduction of Constraints over Nested Sets to Purely Boolean Formulae in CNF
|pdfUrl=https://ceur-ws.org/Vol-2710/paper14.pdf
|volume=Vol-2710
|authors=Domenico Cantone,Andrea De Domenico,Pietro Maugeri,Eugenio G. Omodeo
|dblpUrl=https://dblp.org/rec/conf/cilc/CantoneDMO20
}}
==A Quadratic Reduction of Constraints over Nested Sets to Purely Boolean Formulae in CNF==
https://ceur-ws.org/Vol-2710/paper14.pdf
A Quadratic Reduction of Constraints over Nested
Sets to Purely Boolean Formulae in CNF ? ??
Domenico Cantone[0000−0002−1306−1166]1 , Andrea De Domenico2 ,
Pietro Maugeri1 , and Eugenio G. Omodeo[0000−0003−3917−1942]3
1
Dept. of Mathematics and Computer Science, University of Catania, Italy
domenico.cantone@unict.it, pietro.maugeri@unict.it
2
Scuola Superiore di Catania, University of Catania, Italy
andrea.dedomenico@studium.unict.it
3
Dept. of Mathematics and Earth Sciences, University of Trieste, Italy
eomodeo@units.it
Abstract. A translation is proposed of conjunctions of literals of the
forms x = y \ z, x 6= y \ z, and x ∈ y, where x, y, z stand for variables
ranging over the von Neumann universe of sets, into unquantified Boolean
formulae of a rather simple conjunctive normal form. The formulae in
the target language involve variables ranging over a Boolean field of sets,
along with a difference operator and relators designating equality, non-
disjointness and inclusion. Moreover, the result of each translation is a
conjunction of literals of the forms x = y \ z, x 6= y \ z and of implications
whose antecedents are isolated literals and whose consequents are either
inclusions (strict or non-strict) between variables, or equalities between
variables.
Besides reflecting a simple and natural semantics, which ensures satisfi-
ability-preservation, the proposed translation has quadratic algorithmic
time-complexity, and bridges two languages both of which are known to
have an NP-complete satisfiability problem.
Keywords: Satisfiability problem, Computable set theory, Expressibil-
ity, Proof verification, NP-completeness.
Introduction
The Flatland of sets [1,4] is inhabited by collections formed by entities named
‘urelements’. Two collections are different when the urelements belonging to
either one, and to the other, are not the same; collections may even differ in
cardinality, namely in the number of constituting urelements. One can conceive
of inclusion between collections, and of operations which they can undergo (in-
tersection, union, difference, etc.), on similar grounds: all of these constructs, in
?
Copyright c 2020 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
??
We gratefully acknowledge partial support from project “STORAGE—Università
degli Studi di Catania, Piano della Ricerca 2020/2022, Linea di intervento 2”, and
from INdAM-GNCS 2019 and 2020 research funds.
fact, rely upon membership. It is more natural, instead, to think of equality com-
parison between urelements as of a primitive operation, because urelements are
devoid of any inner structure. Such shapeless entities vanished, insofar as useless,
from the von Neumann universe: sets can be nested one inside another to an ar-
bitrary depth in this new world, and this is a resource that largely compensates
for the missing urelements.
An apt theoretical framework for the study of flat sets is the theory of
Boolean rings, a merely equational first-order theory endowed with finitely many
axioms—at times, one blends this theory with an arithmetic of cardinals. Frame-
works for the study of nested sets are such all-embracing theories as ZF and NBG
(the Zermelo-Fraenkel and von Neumann-Bernays-Gödel theories), within which
one can cast the entire corpus of mathematical disciplines.
Boolean algebra is decidable in its entirety (cf. [5, Sec. 3.7]); ZF is essentially
undecidable, nonetheless an effort to find decision algorithms for fragments of
it began in 1979, the purpose of this long-standing research being an effective
implementation of specialized inference rules within a programmed system apt to
verifying the correctness of large-scale mathematical proofs [6]. When it comes
to implementations, complexity emerges as an unescapable issue; this is why
we undertook, in recent years (see, in particular, [2,3]), a systematic study on
the algorithmic complexities of inference mechanisms specifically designed for
Boolean reasoning and of akin mechanisms which can cope with nested sets.
A priori, one would expect the distance between the performances of deci-
sion algorithms for fragments of Boolean algebra, and of the seemingly much
more expressive languages whose dictionaries embody nested membership, to be
abysmal. Luckily, though, as we will see, this is not the case.
————
We introduce in Sec. 1 an interpreted formal language, dubbed BST, within
which one can formulate unquantified Boolean constraints. Despite its syntax
being quite minimal—BST only encompasses conjunctions of primitive literals
of two forms, namely x = y \ z and x 6= y \ z —, the satisfiability problem for
BST is NP-complete (see [2]). By way of abbreviations, a number of additional
constraints, e.g. literals of the form x 6= y ∪ z, can be expressed in BST.
According to our semantics, the domain of discourse to which BST refers
is a universe of nested sets; however, as will be seen in Sec. 2, every satisfiable
propositional combination of BST literals (as a special case, a conjunctive BST
constraint) admits a model consisting of sets which are, in a certain sense, “flat”.
This makes it evident that membership cannot be plainly expressed in BST. To
detour this limitation, we propose in Sec. 1.2 a novel notion of expressibility, also
embodying an obligation to supply an algorithmic-complexity assessment. This
roundabout notion is, we believe, a valuable contribution of this paper.
In terms of the novel notion of expressibility, in Sec. 3 we will manage to
translate a conjunction of literals of the three forms x = y \ z, x 6= y \ z, and
x ∈ y, into a propositional combination of BST literals. The proposed translation
is, of course, satisfiability preserving. It leads to a conjunction some of whose
conjuncts are BST literals, while other conjuncts are rather simple disjunctions.
The algorithmic time-complexity of our translation is quadratic, which indirectly
shows that the satisfiability problem remains NP-complete when the relator ∈
is added to the constructs of BST: this NP-completeness result was known (see,
e.g., [3]), but this paper sheds new light on it.
The material treated in this paper bridges, in a sense, the topics treated in
[2] and in [3], which are meant to contribute to the proof-verification technology.
1 The theory BST
Boolean Set Theory (BST) is the quantifier-free theory composed by all conjunc-
tions of literals of the following two types:
x = y \ z, x 6= y \ z, (1)
where x, y, and z are set variables assumed to range over the universe of the
well-founded sets.
Semantics for the theory BST is defined in terms of set assignments. Specif-
ically, given a (finite) collection V of set variables, a set assignment M over
V —the variable-domain of M , denoted by dom(M )—is any map from V into
the von Neumann universe V (see below).4 A set assignment M satisfies a given
literal x = y \z, with x, y, z ∈ dom(M ), if M x = M y \M z holds, where M y \M z
is the standard set difference between M y and M z. Likewise, M satisfies the lit-
eral x 6= y \ z if M x 6= M y \ M z holds. Finally, M satisfies a BST-conjunction
ϕ such that Vars(ϕ) ⊆ dom(M ) (where Vars(ϕ) denotes the collection of the
variables occurring free in ϕ) if it satisfies all of the conjuncts of ϕ, in which case
we say that M is a model of ϕ and write M |= ϕ. A BST-conjunction is said to
be satisfiable if it has some model, otherwise it is said to be unsatisfiable.
In [2], it is proved that the satisfiability problem for BST, namely the prob-
lem of establishing algorithmically the satisfiability status of any given BST-
conjunction, is NP-complete.
We shall also be interested in the extension BST+ of the theory BST con-
sisting of all propositional combinations (resulting from unrestrained use of the
logical connectives ∧,∨,−→,←→,¬) of atomic formulae of type x = y \ z. It is not
hard to check that the satisfiability problem for BST+ can be reduced to the sat-
isfiability problem for BST in nondeterministic polynomial time, and therefore
it is NP-complete in its turn.
1.1 The von Neumann universe
We recall that the von Neumann universe V of (well-founded) sets, also dubbed
von Neumann cumulative hierarchy, is built up through a transfinite sequence of
4
Notice that we are not basing our semantics of BST on flat sets of urelements (as
would be doable, as recalled in the Introduction). Doing so would call for minor
adjustments, unjustified—and perhaps disturbing—in the economy of this paper.
steps as the union V := α∈On Vα of the levels Vα := β<α P(Vβ ), with P(·)
S S
denoting the powerset operator and α ranging over the class On of all ordinals.
Based on the level of first appearance in the von Neumann hierarchy, one can
define the rank of any set s, denoted rk (s). Specifically, rk (s) is the ordinal α
such that s ∈ Vα+1 \ Vα . Hence, for every α ∈ On, the set Vα+1 \ Vα , hereinafter
denoted Vα# , collects all sets whose rank equals α.
The following lower bound on the number of well-founded sets of any positive
integer rank n, to be proved as Proposition 2 in Appendix A.1, will be useful:
Vn# > 2n−1 .
Some handy properties of the rank function which we shall tacitly use are
the following:
for all sets s, t ∈ V, we have:
• if s ∈ t then rk (s) < rk (t),
• if s ⊆ t then
( rk (s) 6 rk (t),
0 if s = ∅
• rk (s) =
supu∈s (rk (u) + 1) otherwise.
We also recall that well-foundedness, as enforced by the regularity or foun-
dation axiom of Zermelo-Fraenkel set theory, precludes the formation of infinite
descending membership chains of the form
· · · ∈ s2 ∈ s1 ∈ s0 ,
and in particular of membership cycles
s0 ∈ sn ∈ · · · ∈ s2 ∈ s1 ∈ s0 ,
for any sequence s0 , s1 , s2 , . . . of sets.
1.2 Existential expressibility and O(f )-expressibility
Despite the conciseness of our presentation of BST, it turns out (see [2]) that
several other Boolean constructs, such as the ones in the following list of literals
x = ∅, x ⊆ y, x = y ∩ z, x = y ∪ z, Disj(x, y), x ( y,
(2)
x 6= ∅, x * y, x 6= y ∩ z, x 6= y ∪ z, ¬Disj(x, y),
can be expressed existentially in BST, where Disj(a, b) is a short for a ∩ b = ∅.
Formally, existential expressibility is defined as follows (cf. [2], wherein several
applications of this notion are reported).
Definition 1 (Existential expressibility). A formula ψ(x) is said to be ex-
istentially expressible in a theory T if there exists a T -formula Ψ ( x, z ) such
that
|= ψ( x ) ←→ ( ∃z ) Ψ ( x, z ),
where x and z stand for tuples of set variables.
Existential expressibility has been generalized in [2] into the definition of
O(f )-expressibility. The latter notion enabled, in [2], a detailed complexity tax-
onomy of the subfragments of BST.
Here we slightly generalize O(f )-expressibility so that it copes with collec-
tions C of formulae, rather than with single formulae as its original definition
did; another difference lies in the fact that the generalized notion has to do with
a source theory T1 and a target theory T2 , whereas [2] took it for granted that
source and target were the same.
Definition 2 (O(f )-expressibility). Let T1 and T2 be any theories and f : N →
N be a given map. A collection C of formulae is said to be O(f )-expressible from
T1 into T2 if there exists a map
h ϕ( y ) , ψ( x ) i 7→ Ξϕψ ( x, y, z ) (3)
from T1 × C into T2 , where no variable in z occurs in either x or y, such that
the following conditions are satisfied:
(a) the mapping (3) can be computed in O f (|ϕ ∧ ψ|) -time,
(b) if ϕ( y ) ∧ Ξϕψ ( x, y, z ) is satisfiable, so is ϕ( y ) ∧ ψ( x ),
(c) |= ϕ( y ) ∧ ψ( x ) −→ ( ∃z )Ξϕψ ( x, y, z ).
The main results in this paper are that membership atoms x ∈ y are not
existentially expressible in BST+ , whereas any conjunction of membership atoms
is O(n2 )-expressible from BST into BST+ .
2 Non-existential expressibility in BST+ of x ∈ y
In this section we show that membership atoms are not existentially expressible
in BST+ . Specifically, we prove that every satisfiable
S BST+ -formula Φ admits a
“flat” model M , namely a model whose union x∈Vars(Φ) M x of values is made
up of members all of the same positive rank. We deduce from this fact that
Mx ∈ / M y, for all x, y ∈ Vars(Φ), namely that M 6|= x ∈ y.
Definition 3. For every ordinal ρ > 1, a set assignment S M over a collection V
of variables is said to be ρ-flat if all sets in the domain {M x | x ∈ V } of M
have rank ρ.
No membership atom x ∈ y is satisfied by any ρ-flat set assignment:
Lemma 1. Let M be a ρ-flat set assignment over a collection V of variables.
Then M x ∈
/ M y, for all x, y ∈ V .
Proof. Because of the ρ-flatness of M , for every x ∈ V either rk (M x) = 0 (when
M x = ∅) or rk (M x) = ρ + 1 (when M x 6= ∅). Hence,
S in any case rk (M x) 6= ρ
(since by definition ρ > 1), and therefore M x ∈/ {M y | y ∈ V }.
A satisfiable BST+ -formula always admits a ρ-flat model, for sufficiently large
ρ. This is proved in the next lemma.
Lemma 2. Every satisfiable formula Φ of BST+ admits a ρ-flat set model, for
every ρ > |Vars(Φ)| + 1.
Proof. Let Φ be a satisfiable formula of BST+ , and let M be a set model for Φ.
Let φ+ M be the conjunction of all the distinct atoms x = y \ z occurring in Φ
that are satisfied by M . Likewise, let φ− M be the conjunction of all the distinct
literals x 6= y \ z such that x = y \ z occurs in Φ and M 6|= x = y \ z. Finally, let
−
φM := φ+
M ∧ φM . (4)
Plainly, M satisfies φM by construction. Additionally, by propositional reasoning,
every set model for φM satisfies our initial formula Φ. Thus, it is enough to show
that the conjunction φM admits a ρ-flat set model for every ρ > n + 1, where
n := |Vars(φM )| = |Vars(Φ)|.
We prove that φM admits a ρ-flat set model by contracting each nonempty
region RW of M of the form
\ [
RW := {M x | x ∈ W } ∪ {M y | y ∈ Vars(φM ) \ W },
for ∅ =
6 W ⊆ Vars(φM ), into a distinct singleton of rank ρ + 1 (hence containing
a single member of rank ρ).
Since the map x 7→ 2x − x is strictly increasing for x > 1, for every integer
ρ > n + 1 we have
#
|Vρ# | = |Vρ+1 |−|Vρ | = 2|Vρ | −|Vρ | > 2|Vn+1 | −|Vn+1 | = |Vn+2 |−|Vn+1 | = |Vn+1 | > 2n ,
where the latter inequality follows from Proposition 2 (see Appendix A.1). Hence,
there exists an injective map =ρ : P(Vars(φM )) → Vρ# from the collection of the
nonempty subsets of Vars(φM ) into the family Vρ# of the (hereditarily finite) sets
of rank ρ.
Next, we define a set assignment Mρ∗ over Vars(φM ) by putting
Mρ∗ x := {=ρ (W ) | ∅ 6= W ⊆ Vars(φM ) ∧ RW 6= ∅}.
By construction, the assignment Mρ∗ is ρ-flat. In addition, it is not hard to check
∗
that, for every ∅ =
6 W ⊆ Vars(φM ), the region RW of M ∗ defined by
\ [
∗
RW := {Mρ∗ x | x ∈ W } ∪ {Mρ∗ y | y ∈ Vars(φM ) \ W }
is nonempty if and only if so is its corresponding region RW of M . Thus, Mρ∗
satisfies φM .
We are now ready to prove that membership atoms x ∈ y are not existentially
expressible in BST+ .
Theorem 1. The atom x ∈ y is not existentially expressible in BST+ .
Proof. By way of contradiction, let us assume that x ∈ y is existentially express-
ible by a formula Ψ (x, y, z) involving only atoms of type x0 = y 0 \ z 0 . Hence,
|= x ∈ y ←→ (∃z) Ψ (x, y, z) (5)
would hold.
Since x ∈ y is trivially satisfiable, by (5) so would be (∃z) Ψ (x, y, z) and
therefore Ψ (x, y, z) would be satisfiable too. Thus, by Lemma 2, Ψ (x, y, z) would
be satisfied by a ρ-flat set assignment M ∗ for some ρ > 1, and therefore, by
Lemma 1, M ∗ x ∈ / M ∗ y. Hence, M ∗ |= (∃z) Ψ (x, y, z) ∧ x ∈
/ y, so that M ∗ 6|=
(∃z) Ψ (x, y, z) −→ x ∈ y, contradicting (5).
3 O(n2 )-expressibility in BST+ of membership
conjunctions
Conforming with Definition 2, we shall prove that any membership conjunction
ψ( x ) is O(n2 )-expressible from BST into BST+ by exhibiting a map
h ϕ( y ) , ψ( x ) i 7→ Ξϕψ ( x, y, z )
with ϕ( y ) in BST, which can be computed in quadratic time and such that
conditions (b) and (c) of Definition 2 are satisfied, where ϕ( y ) ranges over the
collection of BST-conjunctions and the variables in z are distinct from those in
x and in y.
Thus, let ϕ( y ) be any BST-conjunction and ψ( x ) be any conjunction of
membership atoms. We let Left(ψ) denote the collection of all the set variables
x occurring in some membership atom x ∈ y in ψ, for some variable y.
For each variable x ∈ Left(ψ), we introduce a new distinct variable x (which
is intended to represent the singleton {x}), and denote by x their collection.
In addition, for each x ∈ Vars(ϕ ∧ ψ) we introduce a new distinct variable x e,
and denote by x e their collection (these variables will enforce that x ∈ y only if
x
e ( ye). Then we put:
^ ^
Ξϕψ ( x, y, x, x
e ) := (x 6= ∅ ∧ x ⊆ y) ∧ (¬Disj(x, y) −→ x ⊆ y)
x∈y in ψ x∈Left(ψ)
y∈Vars(ϕ∧ψ)
^ ^
∧ (¬Disj(x, y) −→ x = y) ∧ (x = y −→ x = y)
x,y∈Left(ψ) x,y∈Left(ψ)
^ ^
∧ (x ⊆ y −→ x
e ( ye) ∧ (x = y −→ x
e = ye)
x∈Left(ψ) x,y∈Vars(ϕ∧ψ)
y∈Vars(ϕ∧ψ)
(thus, the list of variables z in Definition 2 results from the concatenation of the
lists x and xe ).
Plainly, Ξϕψ is a BST+ -formula5 , which satisfies the following proposition,
implying condition (a) of Def. 2:
Lemma 3. Ξϕψ = Θ |Vars(ϕ ∧ ψ)|2 .
The proof of this lemma is delayed to Sec. 3.3.
In the following subsections, we shall prove that
• if ϕ( y ) ∧ Ξϕψ ( x, y, x, x
e ) is satisfiable, then so is ϕ( y ) ∧ ψ( x ), and
• every model of ϕ( y ) ∧ ψ( x ) can be extended to a model of Ξϕψ ( x, y, x, x e ),
thus showing that also conditions (b) and (c) of Definition 2 are fulfilled, and
therefore proving that every membership conjunction is O(n2 )-expressible from
BST into BST+ .
Translation examples
Here we digress to provide a few examples illustrating how the conjunction Ξϕψ
renders the formula ϕ ∧ ψ.
Example 1. The simple conjunction ϕ ∧ ψ where ϕ := x = y \ z and ψ := z ∈ y,
gets translated into
Ξϕψ := z 6= ∅ ∧ z ⊆ y ∧ (¬Disj(z, x) −→ z ⊆ x) ∧
(¬Disj(z, y) −→ z ⊆ y) ∧ (¬Disj(z, z) −→ z ⊆ z) ∧
(z ⊆ x −→ z̃ ( x̃) ∧ (z ⊆ y −→ z̃ ( ỹ) ∧ (z ⊆ z −→ z̃ ( z̃) ∧
(x = y −→ x̃ = ỹ) ∧ (x = z −→ x̃ = z̃) ∧ (y = z −→ ỹ = z̃).
This shows that any relation M s ∈ M t, respectively M s ∈ / M w, where M is a
model for ϕ ∧ ψ ∧ Ξϕψ , gets translated into M s ⊆ M t ∧ M s̃ ( M t̃, resp. into
Disj(s, w).
In fact, to the literal z ∈ y there corresponds the conjunct z ⊆ y, so that
from z ⊆ y −→ z̃ ( ỹ we also get M z̃ ( M ỹ. Furthermore M z ∈
/ M z must hold,
and in fact we can derive Disj(z, z) from (z ⊆ z −→ z̃ ( z̃) ∧ (¬Disj(z, z) −→
z ⊆ z). Then we can get M z ∈ M x from ϕ ∧ ψ, since M x = M y \ M z and
Mz ∈ / M z; we can, analogously, get M z ⊆ M x from ϕ ∧ Ξϕψ : indeed, it follows
from x = y \ z, z ⊆ y, and from the condition Disj(M z, M z) just obtained;
lastly, from z ⊆ x −→ z̃ ( x̃, we get M z̃ ( M x̃.
In the previous example we saw that the conjunct z ⊆ z, that in our transla-
tion would be the equivalent of the unsatisfiable z ∈ z, does not appear in Ξϕψ .
More generally, the usage of the set variables x̃ in Ξϕψ allows us to detect any
membership cycle x ∈ · · · ∈ x that might be derived from ϕ ∧ ψ. In the following
we exemplify this property:
5
In fact, Ξϕψ is a conjunction of a rather simple form.
Example 2. The conjunction ϕ ∧ ψ, where
ϕ := a = b \ c and ψ := x ∈ y ∧ y ∈ z ∧ z ∈ x,
is plainly unsatisfiable due to the cycle x ∈ y ∈ z ∈ x. To reflect this, Ξϕψ
comprises the literals
x ⊆ y ∧ (x ⊆ y −→ x̃ ( ỹ) ∧
y ⊆ z ∧ (y ⊆ z −→ ỹ ( z̃) ∧
z ⊆ x ∧ (z ⊆ x −→ z̃ ( x̃);
therefore it is unsatisfiable due to the cycle x̃ ( ỹ ( z̃ ( x̃.
Our next example shows how the unsatisfiability proofs for the conjunction
ϕ ∧ ψ and ϕ ∧ Ξϕψ mimic each other, especially bearing in mind that M x ∈ M y
gets translated into M x ⊆ M y ∧ M x̃ ( M ỹ, and M x ∈
/ M z into Disj(M x, M z).
Example 3. The conjunction ϕ ∧ ψ, where ϕ := x = y \ z and ψ := z ∈ x ∧ x ∈ y,
is unsatisfiable since if a model M for it existed, then we would have M x ∈ M x.
Indeed: from z ∈ x we obtain M x ∈ / M z, then from x = y \ z and x ∈ y we
obtain M x ∈ M x. This will be reflected by ϕ ∧ Ξϕψ as M x̃ ( M x̃, which in its
turn implies that also ϕ ∧ Ξϕψ is unsatisfiable, where
Ξϕψ := x 6= ∅ ∧ x ⊆ y ∧ z 6= ∅ ∧ z ⊆ x ∧
(¬Disj(x, x) −→ x ⊆ x) ∧ (¬Disj(x, y) −→ x ⊆ y) ∧
(¬Disj(x, z) −→ x ⊆ z) ∧ (¬Disj(z, x) −→ z ⊆ x) ∧
(¬Disj(z, y) −→ z ⊆ y) ∧ (¬Disj(z, z) −→ z ⊆ z) ∧
(¬Disj(x, z) −→ x = z) ∧ (x = z −→ x = z) ∧
(x ⊆ x −→ x̃ ( x̃) ∧ (x ⊆ y −→ x̃ ( ỹ) ∧
(x ⊆ z −→ x̃ ( z̃) ∧ (z ⊆ x −→ z̃ ( x̃) ∧
(z ⊆ y −→ z̃ ( ỹ) ∧ (z ⊆ z −→ z̃ ( z̃) ∧
(x = z −→ x̃ = z̃).
Above, in proving the unsatisfiability of ϕ ∧ ψ, our first step has been to
get M x ∈ / M z; here, by assuming M |= ϕ ∧ Ξϕψ , we first get Disj(M x, M z):
indeed, from z ⊆ x and z ⊆ x −→ z̃ ( x̃ we obtain M z̃ ( M x̃, then from
x ⊆ z −→ x̃ ( z̃ and ¬Disj(x, z) −→ x ⊆ z we obtain Disj(M x, M z). The
second step, above, has been to get M x ∈ M x; here we will get M x̃ ( M x̃:
indeed, from x ⊆ y and x = y \ z, and from the disjointness clause just proved, it
follows that M x ⊆ M x; and, finally, from x ⊆ x −→ x̃ ( x̃ we obtain M x̃ ( M x̃,
which leads to the unsatisfiability of ϕ ∧ Ξϕψ .
ψ
3.1 If ϕ ∧ Ξϕ is satisfiable, then so is ϕ ∧ ψ
Assume that ϕ ∧ Ξϕψ is satisfiable. Hence, by Lemma 2, ϕ ∧ Ξϕψ is satisfied by
some ρ-flat set assignment M such that ρ > Vars(ϕ ∧ Ξϕψ ) + 1. Since there
can be no (-cycle in {M x
e | x ∈ Vars(ϕ ∧ ψ)}, we can find some ordering ≺ on
Vars(ϕ ∧ ψ) such that
Mx
e ( M ye −→ x ≺ y,
for x, y ∈ Vars(ϕ ∧ ψ).
Following the ordering ≺, define recursively, for x ∈ Vars(ϕ ∧ ψ),
M 0 x := M x ∪ M + x, (6)
where
M + x := {M 0 w | M w ⊆ M x ∧ w ∈ Left(ψ)}. (7)
In preparation for the proof that M 0 models ϕ ∧ ψ, we need a few lemmas.
We begin by proving that no rk (M 0 x) equals ρ, for any x ∈ Vars(ϕ ∧ ψ):
Lemma 4. For every x ∈ Vars(ϕ ∧ ψ), rk (M 0 x) 6= ρ.
Proof. If M x 6= ∅, then rk (M 0 x) > rk (M x) = ρ + 1, so rk (M 0 x) 6= ρ. On the
other hand, if M x = ∅, then M + x = {M 0 w | M w ⊆ M x ∧ w ∈ Left(ψ)} = ∅,
since M |= w 6= ∅, for all w ∈ Left(ψ). Hence, M 0 x = ∅, so that rk (M 0 x) = 0 6=
ρ.
An immediate consequence of the preceding claim is:
Corollary 1. For all x, y ∈ Vars(ϕ ∧ ψ),
M x ∩ M + y = ∅, (8)
Proof. It is enough to observe that, for x, y ∈ Vars(ϕ ∧ ψ), when M x 6= ∅, all
members of M x have rank ρ, whereas by Lemma 4 no member of M + y can have
rank ρ.
Next we prove three lemmas which will enable us to conclude that M 0 models
ϕ and ψ as wanted; the second of these relies on Proposition 3, whose statement
and proof are delayed till Appendix A.2.
Lemma 5. For all w, w0 ∈ Left(ψ), M w = M w0 ⇐⇒ M w = M w0 .
Proof. Let w, w0 ∈ Left(ψ). By construction, the formula Ξϕψ contains the fol-
lowing conjuncts, which are all satisfied by the set assignment M :
– w = w0 −→ w = w0 ,
– w 6= ∅,
– ¬Disj(w, w0 ) −→ w = w0 .
Thus, in view of M |= w = w0 −→ w = w0 , if M w = M w0 then we have
M w = M w0 .
Conversely, if M w = M w0 then from M |= w 6= ∅ we get M |= ¬Disj(w, w0 ).
Hence, from M |= ¬Disj(w, w0 ) −→ w = w0 , we get M w = M w0 .
Lemma 6. For all x, y ∈ Vars(ϕ ∧ ψ), M x = M y ⇐⇒ M 0 x = M 0 y.
Proof. If M x = M y, then by (7) we have M + x = M + y. Thus,
M 0 x = M x ∪ M + x = M y ∪ M + y = M 0 y.
Conversely, if M 0 x = M 0 y, then by (7) again we have M x∪M + x = M y∪M + y, so
that Corollary 1 and Proposition 3(b) (see Appendix A.2) yield M x = M y.
Another useful consequence of definitions (6) and (7) is the following result.
Lemma 7. For w ∈ Left(ψ) and x ∈ Vars(ϕ ∧ ψ), the following statements are
equivalent:
(a) M 0 w ∈ M + x,
(b) M w ⊆ M x, and
(c) M w ∩ M x 6= ∅.
Proof. The implication (b) =⇒ (a) follows readily from the definition (7) of M + .
Concerning the implication (a) =⇒ (c), let us assume that M 0 w ∈ M + x,
for some w ∈ Left(ψ) and x ∈ Vars(ϕ ∧ ψ). Then, by (7), there must exist
a w0 ∈ Left(ψ) such that (i) M 0 w = M 0 w0 and (ii) M w0 ⊆ M x. By (i) and
Lemma 6, we have M w = M w0 , which in turn by Lemma 5 implies M w = M w0 .
Hence, by (ii), M w ⊆ M x. Next, since w 6= ∅ is in ϕ, we have M w 6= ∅, so that
the inclusion M w ⊆ M x yields M w ∩ M x 6= ∅.
Finally, the implication (c) =⇒ (a) follows at once from (7), since ϕ contains
the conjunct ¬Disj(w, x) −→ w ⊆ x.
We have now reached the salient conclusion yielded by the definition of M 0
and by the preparatory proofs carried out so far:
Lemma 8. The set assignment M 0 satisfies the conjunction ϕ ∧ ψ.
Proof. We shall prove that M 0 satisfies
(a) all literals in ψ of type x ∈ y,
(b) all literals in ϕ of type x = y \ z,
(c) all literals in ϕ of type x 6= y \ z.
Concerning (a), let x ∈ y be a conjunct in ψ. Then the literal x ⊆ y occurs
in Ξϕψ , so that M x ⊆ M y holds, and therefore by (7) and (6) we have M 0 x ∈
M + y ⊆ M 0 y. Hence, M 0 |= x ∈ y.
Concerning (b), let x = y \ z be in ϕ. Recalling that M |= ϕ, we have M x =
M y \M z. Hence, by (6), Corollary 1, and Proposition 3(a), in order to show that
M 0 satisfies the literal x = y \ z it is enough to prove that M + x = M + y \ M + z
holds, which we do next.
If M 0 w ∈ M + x, for some w ∈ Left(ψ) such that M w ⊆ M x, then M w ⊆
M y \M z, so that M w ⊆ M y and M w ∩M z = ∅. By Lemma 7, M w ⊆ M y yields
M 0 w ∈ M + y and M w ∩M z = ∅ implies M 0 w ∈
/ M 0 z. Thus, M 0 w ∈ M + y \M + z.
By the arbitrariness of w ∈ Left(ψ), we get
M + x ⊆ M + y \ M + z. (9)
Conversely, if M 0 w ∈ M + y\M + z for some w ∈ Left(ψ), then, again by Lemma 7,
we have M w ⊆ M y and M w ∩ M z = ∅. Hence, M w ⊆ M y \ M z = M x, so that
by another application of Lemma 7 we get M 0 w ∈ M + x. The arbitrariness of
w ∈ Left(ψ) yields M + y \ M + z ⊆ M + x. Together with (9), the latter inclusion
implies M + x = M + y \ M + z, completing the proof of (b).
Finally, concerning (c), let x 6= y \ z be in ϕ. Then we have M x 6= M y \ M z,
so that by Proposition 3(a) we readily obtain M 0 x 6= M 0 y ∪ M 0 z.
ψ
3.2 Every model of ϕ ∧ ψ can be extended into a model of Ξϕ
Assume that ϕ ∧ ψ is satisfiable, and let M be a model for it.
Let V := Vars(ϕ ∧ ψ) and let GM = (V, E) be the directed graph over V
such that
(x, y) ∈ E ⇐⇒ M x ∈ M y. (10)
Plainly, the graph GM is acyclic. For, should GM contain a cycle (xi0 , xi1 , . . . , xik , xi0 ),
then we would have the membership cycle M xi0 ∈ M xi1 ∈ · · · ∈ M xik ∈ M xi0 ,
contradicting the axiom of foundation.
Hence, we can define the following notion of height h : V → N by putting
h(x) := length of the longest path in GM leading to x,
for every x ∈ V (in particular, h(x) = 0 whenever x has no predecessors in GM ).
Next let x1 , x2 , ..., xn be any indexing of the variables in Vars(ϕ ∧ ψ) com-
plying with the height h, namely such that
h(xi ) < h(xj ) =⇒ i < j.
We are now ready to define an extension M over Vars(Ξϕψ ) \ Vars(ϕ ∧ ψ) of the
set assignment M which satisfies Ξϕψ . For x ∈ Vars(ϕ ∧ ψ), we put of course
M x := M x. Then, for x ∈ Left(ψ), we set M x := {M x}. Finally, we put
Mx e1 := {1} and recursively, for i = 1, . . . , n − 1,
(
Mx ei if h(xi+1 ) = h(xi ) ,
Mxei+1 :=
Mx ei ∪ {i + 1} otherwise.
From the definition of M , it follows that, for i, j ∈ {1, . . . , n}:
(H1 ) h(xi ) < h(xj ) =⇒ M x
ei ( M x
ej , and
(H2 ) h(xi ) = h(xj ) =⇒ M x
ei = M x
ej .
Next, we prove that M satisfies Ξϕψ .
Lemma 9. The set assignment M satisfies Ξϕψ .
Proof. Let x ∈ y occur in ψ. By construction, M x = {M x}. In addition, since
M |= x ∈ y, we have M x ∈ M y = M y, so that M x ⊆ M y. Thus, by the
arbitrariness of x ∈ y in ψ, we have
^
M |= (x 6= ∅ ∧ x ⊆ y). (11)
x∈y in ψ
Let now x ∈ Left(ψ) and y ∈ Vars(ϕ∧ψ), and assume that M |= ¬Disj(x, y),
namely M x ∩ M y 6= ∅. Hence, {M x} ∩ M y 6= ∅, so that M x = {M x} ⊆ M y.
Thus, by the arbitrariness of x ∈ Left(ψ) and y ∈ Vars(ϕ ∧ ψ), we have
^
M |= (¬Disj(x, y) −→ x ⊆ y). (12)
x∈Left(ψ)
y∈Vars(ϕ∧ψ)
Next, let x, y ∈ Left(ψ) and assume that M |= ¬Disj(x, y), namely M x ∩
M y 6= ∅. Since by construction M x = {M x} and M y = {M y}, it follows that
M x = M y, and therefore M x = M y. Hence, by the arbitrariness of x, y ∈
Left(ψ), we have
^
M |= (¬Disj(x, y) −→ x = y). (13)
x,y∈Left(ψ)
Let x, y ∈ Left(ψ), but assume now that M x = M y, so that M x = M y
holds. Thus, M x = {M x} = {M y} = M y, proving that
^
M |= (x = y −→ x = y), (14)
x,y∈Left(ψ)
by the arbitrariness of x, y ∈ Left(ψ).
Next, let x ∈ Left(ψ) and y ∈ Vars(ϕ ∧ ψ) be such that M |= x ⊆ y, i.e.,
M x ⊆ M y. Hence, we have {M x} ⊆ M y, and therefore M x ∈ M y. The latter
membership relation implies that the graph GM associated with the assignment
M contains the arc (x, y), and so h(x) < h(y). Thus, by (H1 ) we have M x
e ( M ye,
and therefore we have
^
M |= (x ⊆ y −→ xe ( ye), (15)
x∈Left(ψ)
y∈Vars(ϕ∧ψ)
by the arbitrariness of x ∈ Left(ψ) and y ∈ Vars(ϕ ∧ ψ).
Finally, let x, y ∈ Vars(ϕ∧ψ) and assume that M x = M y, so that M x = M y.
By (10), the nodes in GM labeled x and y have the same predecessors. Therefore,
h(x) = h(y), so that by (H2 ) we have M x e = M ye. Hence, by the arbitrariness of
x, y ∈ Vars(ϕ ∧ ψ), we have
^
M |= (x = y −→ x e = ye). (16)
x,y∈Vars(ϕ∧ψ)
From (11)–(16), it follows that the assignment M satisfies ϕ.
Summing up, from Lemmas 3, 8, and 9, we have:
Theorem 2. Membership conjunctions are O(n2 )-expressible from BST into
BST+ .
3.3 Design and analysis of the translation algorithm
In order to prove Lemma 3, we provide a detailed specification of the algorithm
that generates from the conjunction ϕ ∧ ψ the formula ΞϕΨ .
1: Initialize Vars(ϕ ∧ ψ) and Left(ψ) as empty lists of set variables;
2: Initialize Ξϕψ as an empty list of conjuncts;
3: for all set variable x that appears in ϕ do
4: add x to Vars(ϕ ∧ ψ);
5: for all conjunct x ∈ y that appears in ψ do
6: add x and y to Vars(ϕ ∧ ψ);
7: add x to Left(ψ);
8: add (x 6= ∅ ∧ x ⊆ y to Ξϕψ );
9: for all x ∈ Left(ψ) do
10: for all y ∈ Vars(ϕ ∧ ψ) do
11: add (¬Disj(x, y) −→ x ⊆ y ∧ x ⊆ y −→ x̃ ( ỹ) to Ξϕψ ;
12: for all x, y ∈ Left(ψ) do
13: add (¬Disj(x, y) −→ x = y ∧ x = y −→ x = y ∧ x = y −→ x̃ = ỹ) to Ξϕψ .
Adding elements to Vars(ϕ ∧ ψ), Left(ψ), and Ξϕψ will require constant time
if these are implemented as lists of set variables and conjuncts.
The for-loop at lines 3 and 4 can be performed in Θ(|ϕ|)-time, where |ϕ| is
the total lenght of the conjunction ϕ; similarly the for-loop from line 5 to line 8
can be performed in Θ(|ψ|)-time. The for-loop from line 9 to line 11 is iterated
Θ(|Left(ψ) × Vars(ϕ ∧ ψ)|) times and the for-loop at lines 12 and 13 is iterated
2
Θ |Left(ψ)| times.
The overall time complexity is then Θ |ϕ ∧ ψ| + |Left(ψ) × Vars(ϕ)| +
2
|Left(ψ)| , and since most commonly a conjunction ϕ∧ψ is such that |ϕ ∧ ψ| =
2
O |Vars(ϕ ∧ ψ)| and |Left(ψ)| = Θ(|Vars(ϕ ∧ ψ)|), we can say that Ξϕψ can
2
be generated in Θ |Vars(ϕ ∧ ψ)| time.
4 Future work
By a technique close to to the one proposed above for translating conjunctions
of literals of the forms x = y \ z, x 6= y \ z, and x ∈ y, it is possible to translate
conjunctions of literals of the three forms x = y \ z, x 6= y \ z, and x = { y } into
propositional combinations of BST literals. (This is an enhancement proper of
the translation: in fact, x ∈ y can be restated as s = { x } ∧ z = z \z ∧ z = s\y.)
Moreover, we will strive to enhance the nested-to-flat translation so as to
enable it to handle rank comparison and cardinality comparison constructs.
We also have in mind a linear-cost flat-to-nested translation, exploiting mem-
bership to eliminate the equality relator from conjunctions of BST literals in
terms of membership literals.
With Mattia Furlan, who recently earned a bachelor degree from the Uni-
versity of Trieste, we have spotted out the following valid formulae involving
Boolean difference:
(D.1) x \ (y \ y) = x Existence of zero
(D.2) (x \ y) \ z = (x \ z) \ y Permutativity
(D.3) x \ (x \ y) = y \ (y \ x) Commutativity (of intersection)
(D.4) (x \ y) \ y = x \ y Double subtraction
Let us take the universal closures of these formulae as the axioms of a theory
based on quantificational first-order logic with equality. These axioms charac-
terize an algebraic variety, whose instances we provisionally dub here difference
algebras. We have an open issue: Is every difference algebra D = (D, \D ) isomor-
phic to an algebra of the form S = (S, \) which interprets the operator ‘\’ as
ordinary subtraction between sets? Here, of course, S must be a family of sets
closed w.r.t. subtraction, hence w.r.t. ∩, because X ∩ Y = X \ (X \ Y ) holds for
all sets X, Y . Perhaps, in order to settle this issue positively, we should somehow
manage to apply Stone’s celebrated representation theorem, stating that every
Boolean algebra is isomorphic to a field of sets. However, we see no direct way of
relying on that theorem, because there are difference algebras D whose support
domain D fails to be closed w.r.t. symmetric difference intended as an operation
h Y , Z i 7→ Y 4D Z such that, for all X, Y, Z in D,
X = Y 4D Z ↔ X \D (Y \D Z) = Z \D Y ∧ Y \D Z = X \D Z ;
moreover, it is not clear to us how one can embed a generic difference algebra
into one which is a Boolean ring proper, because it enjoys this closure property.
References
1. Edwin A. Abbot. Flatland: A romance of many dimensions, Seeley & Co. of London,
1884.
2. Domenico Cantone, Andrea De Domenico, Pietro Maugeri, and Eugenio G. Omodeo.
Complexity assessments for decidable fragments of set theory. I: A taxonomy for the
Boolean case, 2020. To appear.
3. D. Cantone, P. Maugeri, and E.G. Omodeo. Complexity assessments for decidable
fragments of set theory. II: A taxonomy for ‘small’ languages involving membership,
Theoretical Computer Science, 2020. To appear.
4. Agostino Dovier. Computable Set Theory and Logic Programming, PhD thesis, Uni-
versità degli Studi di Pisa, March 1996. TD–1/96.
5. Michael O. Rabin. Decidable theories. In Barwise, J., editor, Handbook of Mathe-
matical Logic, Studies in Logic, No. 90, pages 595–629, North Holland, Amsterdam,
1977.
6. Jacob T. Schwartz, D. Cantone, and E.G. Omodeo. Computational logic and set
theory: Applying formalized logic to analysis, Springer-Verlag, 2011. Foreword by
Martin Davis.
A Some auxiliary results
A.1 A lower bound on the number of sets of a positive integer rank
Here we figure out inequalities preparatory to the proof of Proposition 2 below.
Proposition 1. (a) For every k > 3, we have k > 2 + blog kc;
(b) for every k > 2, we have 2k − k > 2 k − blog kc .
Proof. We prove (a) by induction on k > 3. For k = 3, we have 3 = 2 + blog 3c.
For k > 3, by induction we have
k − 1 > 2 + blog(k − 1)c.
Hence,
k > 2 + blog(k − 1)c + 1 > 2 + blog kc.
Concerning (b), we proceed by induction on k > 2. For k = 2, we have
22 − 2 = 2 = 2(2 − blog 2c).
For k > 2, by induction we have:
2k−1 − (k − 1) > 2 k − 1 − blog(k − 1)c
and therefore
2k − k > 2k − 2(k − 1) > 4 k − 1 − blog(k − 1)c > 4 k − 1 − blog kc .
By (a), we have
4 k − 1 − blog kc > 2 k − blog kc ,
so that
2k − k > 2 k − blog kc .
Next we come to a proposition which lies in the background of this paper:
Proposition 2. For every positive integer n, the number of well-founded sets of
rank equal to n is greater than or equal to 2n−1 , namely
|Vn# | > 2n−1 .
Proof. We proceed by induction on n > 1. For n = 1, we have |V1# | = 1 = 21−1 .
For n > 1, by induction we have:
#
|Vn | − |Vn−1 | = |Vn−1 | > 2n−2 ,
so that
2 |Vn | − |Vn−1 | > 2n−1 .
(17)
Since Vn = P(Vn−1 ), we have |Vn | = 2|Vn−1 | . Thus, by (17) and since |Vn−1 | is
a power of 2, we obtain
2 |Vn | − blog |Vn |c > 2n−1 .
(18)
Finally, from Proposition 1(b) and (18) (since |Vn | > 2), we have
|Vn# | = |Vn+1 | − |Vn | = 2|Vn | − |Vn | > 2 |Vn | − blog |Vn |c > 2n−1 .
A.2 Two useful syllogisms
The syllogisms validated by our next proposition play a role in the proofs of
Lemma 6 and Lemma 8 as presented above.
Proposition 3. For all sets A, B, C, A0 , B 0 , C 0 such that
A ∪ B ∪ C ∩ A0 ∪ B 0 ∪ C 0 = ∅,
(19)
we have:
(a) A ∪ A0 \ B ∪ B 0 = C ∪ C 0 ⇐⇒ A \ B = C ∧ A0 \ B 0 = C 0 ;
(b) A ∪ A0 = B ∪ B 0 ⇐⇒ A = B ∧ A0 = B 0 .
Proof. Concerning (a), by the left distributivity of ∪ over \, we have
(A ∪ A0 ) \ (B ∪ B 0 ) = A \ (B ∪ B 0 ) ∪ A0 \ (B ∪ B 0 ) .
In addition, from (19) it follows that
A \ (B ∪ B 0 ) ∪ A0 \ (B ∪ B 0 ) = (A \ B) ∪ (A0 \ B 0 ).
Hence, we have:
(A ∪ A0 ) \ (B ∪ B 0 ) = (A \ B) ∪ (A0 \ B 0 ).
Thus, if C = A \ B and C 0 = A0 \ B 0 , the latter equation readily yields
A ∪ A0 \ B ∪ B 0 = C ∪ C 0 .
On the other hand, if A ∪ A0 \ B ∪ B 0 = C ∪ C 0 , setting U := A ∪ B ∪ C
and U 0 := A0 ∪ B 0 ∪ C 0 , by (19) we have
A \ B = U ∩ (A \ B) ∪ (A0 \ B 0 ) = U ∩ (C ∪ C 0 ) = C
and
A0 \ B 0 = U 0 ∩ (A \ B) ∪ (A0 \ B 0 ) = U 0 ∩ (C ∪ C 0 ) = C 0 .
Next, concerning (b), if A = B and A0 = B 0 , we plainly have A∪A0 = B ∪B 0 .
For the converse implication, let us assume that A ∪ A0 = B ∪ B 0 holds. Then
we have:
A = (A ∪ B) ∩ A
= (A ∪ B) ∩ A ∪ (A ∪ B) ∩ A0
= (A ∪ B) ∩ (A ∪ A0 )
= (A ∪ B) ∩ (B ∪ B 0 )
= (A ∪ B) ∩ B ∪ (A ∪ B) ∩ B 0
= (A ∪ B) ∩ B
= B.
Likewise, by interchanging in the previous proof A with A0 and B with B 0 , one
can readily prove that A0 = B 0 holds as well.