=Paper=
{{Paper
|id=Vol-2396/paper22
|storemode=property
|title=Polynomial-Time Satisfiability Tests for Boolean Fragments of Set Theory
|pdfUrl=https://ceur-ws.org/Vol-2396/paper22.pdf
|volume=Vol-2396
|authors=Domenico Cantone,Andrea De Domenico,Pietro Maugeri,Eugenio Omodeo
|dblpUrl=https://dblp.org/rec/conf/cilc/CantoneDMO19
}}
==Polynomial-Time Satisfiability Tests for Boolean Fragments of Set Theory==
https://ceur-ws.org/Vol-2396/paper22.pdf
Polynomial-Time Satisfiability Tests for
Boolean Fragments of Set Theory?
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
2
Scuola Superiore di Catania, University of Catania, Italy
3
Dept. of Mathematics and Geosciences, University of Trieste, Italy
{domenico.cantone,pietro.maugeri}@unict.it,
andrea.dedomenico@studium.unict.it, eomodeo@units.it
Abstract. We recently undertook an investigation aimed at identifying
small fragments of set theory (which in most cases are sublanguages
of Multi-Level Syllogistic) endowed with polynomial-time satisfiability
decision tests, potentially useful for automated proof verification. Leaving
out of consideration the membership relator ∈ for the time being, in
this note we provide a complete taxonomy of the polynomial and the
NP-complete fragments involving, besides variables intended to range
over the von Neumann set-universe, the Boolean operators ∪, ∩, \, the
Boolean relators ⊆, 6⊆, =, 6=, and the predicates ‘· = ∅’ and ‘Disj(·, ·)’,
meaning ‘the argument set is empty’ and ‘the arguments are disjoint
sets’, along with their opposites ‘· 6= ∅’ and ‘¬Disj(·, ·)’.
Keywords: Satisfiability problem, Computable set theory, Boolean set
theory, Proof verification, NP-completeness.
Introduction
The decision problem for fragments of set theory, namely the problem of estab-
lishing algorithmically for any formula ϕ in a given fragment whether or not ϕ is
valid in the von Neumann universe of sets, has been thoroughly investigated over
the last four decades within the field of Computable Set Theory. Research has
mainly focused on the equivalent satisfiability problem, namely the problem of
establishing in an effective manner, for any formula in a given fragment, whether
an assignment of sets to its free variables exists that makes the formula true.
The initial goal (back in 1979) envisaged an automated proof verifier based
on set theory, within which it would become possible to carry out an extensive
formalization of classical mathematics. The inferential kernel of such a proof
assistant should have embodied decision procedures intended to capture the ‘ob-
vious’ (deduction steps). Very soon, and long before the proof verifier came into
?
We gratefully acknowledge support from “Università degli Studi di Catania, Piano
della Ricerca 2016/2018 Linea di intervento 2” and from the INdAM-GNCS 2019
research project “Logic Programming for early detection of pancreatic cancer”.
existence, the initial goal sparked a foundational quest aimed at drawing the
precise frontier between the decidable and the undecidable in set theory (and
also in other important mathematical theories). This inspired much of the sub-
sequent work. Several extensions of the progenitor fragments MLS and MLSS of
set theory were proved to have a solvable satisfiability problem, which led to a
substantial body of results, partly comprised in the monographs [3,5,16,15,8].
We recall that MLS (an acronym for Multi-Level Syllogistic, see [10]) copes
with propositional combinations of literals of the form
x = y ∪ z, x = y ∩ z, x = y \ z, x ∈ y; (1)
to these constructs, MLSS adds the singleton operator {·} .4 Unfortunately, as
shown in [4], the satisfiability problem for either MLS or MLSS is NP-complete,
even if restricted to conjunctions of flat literals of type (1) plus negative literals
of type x ∈ / y. All extensions of MLS will hence have, in their turn, an NP-hard
satisfiability problem (in fact, even hyperexponential in some cases; see [1,6,7]).
Notwithstanding, the decision algorithm for an enriched variant of MLSS, im-
plemented along the guidelines of [9], has come to play a key role among the
inference mechanisms available in the proof-checker ÆtnaNova, aka Ref [16]. In
view of the pervasiveness of that mechanism in actual uses of ÆtnaNova (as
discussed, e.g., in [14, Sect. 3] and in [15, Sect. 5.3.1]), it will pay off to circum-
vent whenever possible the poor performances occasionally originating from the
full-strength decision algorithm.
This is why we recently undertook an investigation aimed at identifying useful
‘small’ fragments of set theory (which in most cases are subfragments of MLS)
endowed with polynomial-time decision tests.
In this note we report on results focused, for the time being, on fragments that
exclude the membership relator ∈.5 We provide a complete taxonomy of the poly-
nomial and the NP-complete fragments involving, besides set variables intended
to range over the von Neumann universe of all sets (see below), the Boolean
operators ∪, ∩, \ and relators ⊆, 6⊆, =, 6=, and the predicates (both affirmed and
negated) ‘· = ∅’ and ‘Disj(·, ·)’, expressing respectively that a specified set is
empty and that two specified sets are disjoint.
The paper is organized as follows: Sect. 1 introduces the syntax and se-
mantics of a language in which several hundreds of decidable fragments will be
framed in this note; a subsection of it defines ‘expressibility’, a notion which
4
Note that, thanks to the following equivalences, 6= and ∈
/ are available in MLS and
∈ is eliminable from MLSS:
x 6= y ↔ ∃ w ( x ∈ w ∧ y ∈
/ w ),
y∈ / w ↔ ∃v ( y ∈ v ∧ w ∩ v = v \ v ),
x ∈ w ↔ {x} ∩ w = {x} .
Also note that by adding Cartesian square literals x = y×y and cardinality literals
|x| = |y|, |x| =
6 |y| to MLS, one makes the satisfiability problem undecidable [2].
5
Some preliminary results involving the membership relator ∈ will also be reviewed
in Appendix B.
eases the systematic assessment of the complexities of the satisfiability decision
tests. A complexity-based classification of the fragments under consideration is
highlighted in Sect. 2. The paper terminates with a conclusion and some hints
for future research, and with two appendices containing, respectively, the proofs
of three lemmas on expressibility matters, and a brief overview of the complexity
taxonomy for a small fragment involving the membership relator.
1 Boolean set theory
This section introduces an interpreted language regarding sets, whose acronym
BST stands for ‘Boolean set theory’. The constructs of BST are borrowed from
the algebraic theory of Boolean rings (see [12]), but its variables are meant to
range over a universe of nested (as opposed to ‘flat’) sets. We dub BST a ‘theory’
simply to emphasize that it has a decidable satisfiability problem. Below we will
browse a wide range of subproblems of the satisfiability problem referring to the
whole of BST, and will assess the algorithmic complexity of those subproblems.
We postpone to future reports the treatment of ∈, the membership relation.
Adding ∈ to BST does not disrupt its decidability and truly calls for nested sets.
1.1 Syntax
The fragments of set theory investigated within the project we are reporting
about are parts, syntactically delimited, of a specific quantifier-free language
BST := BST(∪, ∩, \, =∅, 6=∅, Disj, ¬Disj, ⊆, 6⊆, =, 6=).
This is the collection of all conjunctions of literals of the types
s = ∅, s 6= ∅, Disj(s, t), ¬Disj(s, t),
s ⊆ t, s 6⊆ t, s = t, s 6= t,
where s and t stand for terms assembled from a denumerably infinite supply of set
variables x, y, z, . . . by means of the Boolean set operators: union ∪, intersection
∩, and set difference \.
More generally, we shall denote by BST(op1 , . . . , pred1 , . . .) the subtheory of
BST involving only the set operators op1 , . . . (drawn from the set {∪, ∩, \}) and
the predicate symbols pred1 , . . . (drawn from {=∅, 6=∅, Disj, ¬Disj, ⊆, 6⊆, =, 6=}).
1.2 Semantics
For any BST-conjunction ϕ, we shall denote by Vars(ϕ) the collection of set
variables occurring in ϕ; Vars(τ ) is defined likewise, for any BST-term τ .
A set assignment M is any function sending a collection of set variables V
(called the domain of M and denoted dom(M )) into the von Neumann universe
V of well-founded sets. We recall that the von Neumann universe (see [13, pp.95–
102]), aka von Neumann cumulative hierarchy, is built up in stages as the union
V := ∪α∈On Vα of the levels Vα := ∪β<α P(Vβ ), with α ranging over the class
On of all ordinal numbers, where P(·) is the powerset operator.
Natural designation rules attach recursively a value to every term τ of BST
such that Vars(τ ) ⊆ dom(M ), for any set assignment M ; here is how:
M (s ∪ t) := M s ∪ M t, M (s ∩ t) := M s ∩ M t, and M (s \ t) := M s \ M t.
We also put
( (
true if M s = ∅ true if M s ∩ M t = ∅
M (s = ∅) := M (Disj(s, t)) :=
false otherwise, false otherwise,
M (s 6= ∅) := ¬M (s = ∅) M (¬Disj(s, t)) := ¬M (Disj(s, t))
for all literals s = ∅, s 6= ∅, Disj(s, t), and ¬Disj(s, t) of BST (and similarly for
the literals of BST of the remaining types s ⊆ t, s 6⊆ t, s = t, and s 6= t), and
then, recursively,
M (ϕ ∧ ψ) := M ϕ ∧ M ψ
when ϕ, ψ are BST-conjunctions, Vars(ϕ) ⊆ dom(M ), and Vars(ψ) ⊆ dom(M ).
Given a conjunction ϕ and a set assignment M such that Vars(ϕ) ⊆ dom(M ),
we say that M satisfies ϕ, and write M |= ϕ, if M ϕ = true. When M satisfies
ϕ, we also say that M is a model of ϕ.
A conjunction ϕ is said to be satisfiable if it has some model, else unsatisfiable.
BST is a sublanguage of MLS, which has an NP-complete satisfiability prob-
lem [4]; since, in their turn, the fragments of set theory which we shall examine
are included in BST, their satisfiability problems belong to NP.
1.3 Expressibility
The technique of reduction has been our main tool in the construction of the
complexity taxonomy of BST-fragments, which will be presented at length in
Sect. 2.
In our case, reductions have been mostly based on the standard notion of
‘context-free’ expressibility:
Definition 1 (Expressibility). A formula ψ(x) is expressible in a fragment
T of BST, if there exists a T -conjunction Ψ (x, y) such that
|= ψ(x) ←→ (∃y) Ψ (x, y),
where x and y stand for tuples of set variables.
We also devised a more general notion of ‘context-sensitive’ expressibility,
also characterized by its complexity. We named it O(f )-expressibility, where
f : N → N is any mapping intended to bound the complexity of the underlying
rewriting procedure.
Definition 2 (O(f )-expressibility). Let T be a fragment of BST and f : N →
N a given mapping. A formula ψ(x) is O(f )-expressible in T if there exists a
mapping
ϕ(y) 7→ Ψϕ (x, y, z) (2)
from T into T such that the following conditions are satisfied:
(a) the mapping (2) can be computed in O(f )-time,
(b) if ϕ(y) ∧ (∃z)Ψϕ (x,
y, z) is satisfiable, so is ϕ(y) ∧ ψ(x),
(c) |= ϕ(y) ∧ ψ(x) −→ (∃z)Ψϕ (x, y, z).
It turns out that standard expressibility is a special case of O(1)-expressibility.
This is stated in the following lemma, whose simple proof is provided in Ap-
pendix A.
Lemma 1. If a formula ψ(x) is expressible in a fragment T of BST, then it is
also O(1)-expressible in T .
Various expressibility and inexpressibility results are collected in the following
lemma proved in Appendix A.
Lemma 2. (a) x = y \ z is expressible in BST(∪, Disj, =);
(b) x = y ∩ z and x = y ∪ z are expressible in BST(\, =);
(c) x = y is expressible in BST(⊆);
(d) x ⊆ y is expressible both in BST(∪, =) and in BST(∩, =);
(e) x * y is expressible both in BST(∪, 6=) and in BST(∩, 6=);
(f ) x 6= ∅ is expressible in BST(⊆, 6=), and therefore in BST(∪, =, 6=); moreover,
x 6= ∅ is expressible in BST(*), in BST(6=, Disj), in BST(=∅, 6=), and in
BST(¬Disj);
(g) x = ∅ is expressible in BST(Disj);
(h) Disj(x, y) is expressible both in BST(∩, =∅) and in BST(\, =), and
¬Disj(x, y) is expressible both in BST(∩, 6=∅) and in BST(⊆, 6=∅);
(i) ¬Disj(x, y) (i.e., x ∩ y 6= ∅) is expressible in BST(⊆, 6=), and therefore ex-
pressible in BST(∪, =, 6=);
(j) x = ∅ is not expressible in BST(∪, ∩, =, 6=);
(k) x = y \ z is not expressible in BST(∪, ∩, =, 6=).
The following lemma, whose proof can be found in Appendix A, allows us to
infer that the literal x = ∅ is O(n)-expressible in BST(∪, =, 6=).
Lemma 3. The mapping ϕ(y) 7→ Ψϕ (y, x) from BST(∪, =, 6=) into itself, where
x is any set variable (possibly in ϕ) and
^
Ψϕ (y, x) := z ∪ x = z,
z∈Vars(ϕ)
enjoys the properties
- if ϕ(y) ∧ Ψϕ (y, x) is satisfiable, so is ϕ(y) ∧ x = ∅, and
- |= ϕ(y) ∧ x = ∅ −→ Ψϕ (y, x).
Hence, the literal x = ∅ is O(n)-expressible by Ψϕ (y, x) in BST(∪, =, 6=).
2 Complexity taxonomy of the fragments of BST
Of a fragment of BST, we say that it is NP-complete if it has an NP-complete
satisfiability problem (see [11]). Likewise, we say that it is polynomial if its
satisfiability problem has polynomial complexity.
The number of distinct fragments of BST is equal to 23 · (28 − 1) = 2040, of
which 1278 are NP-complete and the remaining 762 are polynomial. The com-
plexity of any fragment of BST can be efficiently identified once the minimal
NP-complete fragments (namely the NP-complete fragments of BST that do not
strictly contain any NP-complete fragment of BST) and the maximal polynomial
fragments (namely the polynomial fragments of BST that are not strictly con-
tained in any polynomial fragment of BST) have been singled out. Indeed, any
BST-fragment either is contained in some maximal polynomial BST-fragment or
contains some minimal NP-complete fragment.
∪ ∩ \ =∅ 6=∅ Disj ¬Disj ⊆ * = 6= Complexity
? ? NP-complete
? ? NP-complete
? ? NP-complete
? ? NP-complete
? ? ? NP-complete
? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? NP-complete
? ? ? ? ? ? ? O(1)
? ? ? ? ? ? O(1)
? ? ? ? ? ? ? O(n3 )
? ? ? ? ? ? ? ? ? O(n4 )
? ? ? ? ? ? ? ? O(n3 )
Table 1. Complete taxonomy of minimal NP-complete and maximal polynomial frag-
ments of BST
Table 1 reports the 18 minimal NP-complete fragments of BST and the 5 max-
imal polynomial fragments of BST. Each row represents the fragment involving
the operators and the relators that are marked with a ‘?’ symbol.
2.1 Minimal NP-complete fragments of BST
Concerning the NP-complete fragments, initially we proved that the fragments
BST(\, 6=), BST(∪, ∩, 6=), BST(∪, ∩, =∅, 6=∅), and BST(∪, =, Disj, ¬Disj)
are NP-complete, by reducing the well-known NP-complete problem 3SAT (see
[11]) to each of them.
Then it can be observed that:
first block: the NP-completeness of the fragments BST(\, *), BST(\, ¬Disj),
and BST(\, 6=∅) in the first block of Table 1 can be obtained by much the
same technique used to reduce 3SAT to BST(\, 6=);
second block: the NP-completeness of the fragment BST(∪, ∩, *) can be achie-
ved by much the same technique used to reduce 3SAT to BST(∪, ∩, 6=);
third block: the NP-completeness of the fragments BST(∪, ∩, Disj, ¬Disj),
BST(∪, ∩, =∅, ¬Disj), and BST(∪, ∩, 6=∅, Disj) can be obtained by much the
same technique used to reduce 3SAT to BST(∪, ∩, =∅, 6=∅); and
fourth block: the NP-completeness of the fragment BST(∪, =, 6=∅, Disj) can be
shown by much the same reduction technique used for BST(∪, =, Disj, ¬Disj).
Finally, by resorting to some of the expressibility results listed in Lemma 2, it
can readily be proved that:
- BST(∪, =, Disj, ¬Disj) can be reduced in linear time
to BST(∪, ⊆, Disj, ¬Disj), by Lemma 2(c),
- BST(∪, =, 6=∅, Disj) can be reduced in linear time
to BST(∪, =, 6=, Disj), by Lemma 2(f),
to BST(∪, =, *, Disj), by Lemma 2(f),
to BST(∪, ⊆, 6=∅, Disj), by Lemma 2(c),
to BST(∪, ⊆, 6=, Disj), by Lemma 2(c)(f),
to BST(∪, ⊆, *, Disj), by Lemma 2(c)(f).
2.2 Maximal polynomial fragments of BST
Two of the maximal polynomial fragments of BST, namely
BST(∪, ∩, \, =∅, Disj, ⊆, =) and BST(∪, ∩, =, 6=∅, ¬Disj, ⊆)
are trivial as they contain only satisfiable conjunctions, thereby admitting a O(1)
satisfiability test.
Notice that the first fragment comprises all the positive relators and the
complete suite of Boolean operators. It is immediate to check that each of its
conjunctions ϕ is satisfied by the null set assignment M∅ over Vars(ϕ), where
M∅ x = ∅ for each x ∈ Vars(ϕ).
Concerning the second fragment, it can easily be verified that each of its
conjunctions ψ is satisfied by any constant nonnull set assignment Ma over
Vars(ψ), where a is a nonempty set and Ma x = a for every x ∈ Vars(ψ).
Next, we provided O(n3 ) satisfiability tests for the fragments
BST(∪, Disj, ¬Disj, 6=) and BST(∪, =, 6=), and a O(n4 ) satisfiability test
for the fragment BST(∩, =∅, =, 6=).
Since
- |= x * y ←→ x ∪ y 6= y (cf. Lemma 2(e)) and
- |= x = ∅ ←→ Disj(x, x) (cf. Lemma 2(f),(g)),
the O(n3 ) satisfiability test for BST(∪, Disj, ¬Disj, 6=) yields a O(n3 ) satisfiability
test for BST(∪, =∅, 6=∅, Disj, ¬Disj, *, 6=).
In addition, since
- x 6= ∅ is expressible in BST(=∅, 6=) (cf. Lemma 2(f)),
- Disj(x, y) and ¬Disj(x, y) are expressible in BST(∩, = ∅, 6= ∅) (cf.
Lemma 2(h)), and
- x ⊆ y and x * y are expressible in BST(∩, =∅, 6=∅) (cf. Lemma 2(d),(e)),
it follows that the O(n4 ) satisfiability test for BST(∩, =∅, =, 6=) yields a O(n4 )
satisfiability test for the fragment BST(∩, =∅, 6=∅, Disj, ¬Disj, ⊆, *, =, 6=).
Finally, since
- x = ∅ is O(n)-expressible in BST(∪, =, 6=) (cf. Lemma 3),
- x 6= ∅ is expressible in BST(=∅, 6=) (cf. Lemma 2(f)),
- x ⊆ y is expressible in BST(∪, =),
- x * y is expressible in BST(∪, 6=), and
- ¬Disj(x, y) is expressible in BST(6=∅, ⊆),
the O(n3 ) satisfiability test for BST(∪, =, 6=) yields a O(n3 ) satisfiability test for
the fragment BST(∪, =∅, 6=∅, ¬Disj, ⊆, *, =, 6=).
It can be checked that:
(A) none of the fragments listed in Table 1 is strictly contained in another frag-
ment in the same table, and
(B) for every fragment T of BST, there is a fragment in Table 1 that either
contains T or is contained in T .
Properties (A) and (B) imply that the 18 NP-complete fragments in Table 1 are
indeed minimally NP-complete and, symmetrically, the 5 polynomial fragments
in Table 1 are maximally polynomial.
∪ ∩ \ =∅ 6=∅ Disj ¬Disj ⊆ * = 6= Complexity
? ? ? ? ? ? O(n)
? ? ? ? ? O(n3 )
Table 2. Two non-maximal polynomial fragments of BST
2.3 A linear satisfiability test for BST(∪, Disj, 6=)
While there is a limited interest in further investigating the non-minimal NP-
complete fragments of BST, this is not the case for the non-maximal polynomial
fragments, as the latter can admit decision tests more efficient than any of the
maximal polynomial fragments extending them.
We briefly report here some preliminary results obtained so far in this direc-
tion (see Table 2). In particular, we devised:
- a linear-time decision test for the fragment BST(∪, Disj, 6=), which readily
generalizes, by Lemma 2(e),(f),(g), to a linear-time satisfiability test for the
extended fragment BST(∪, =∅, 6=∅, Disj, *, 6=);
- a cubic algorithm for the fragment BST(∩, = ∅, 6=), which yields, by
Lemma 2(f),(h), a cubic satisfiability test for the extended fragment
BST(∩, =∅, 6=∅, Disj, 6=).
For space reasons, we limit ourselves to present only a linear-time satisfiability
test for the fragment BST(∪, Disj, 6=).
For convenience, we shall represent terms of the form x1 ∪ · · · ∪ xh as
∪{x1 , . . . , xh }. Thus, for a set assignment M and a finite nonempty collection
of set variables L ⊆ Vars(ϕ), we shall have M (∪L) = ∪M L = x∈L M x.
S
Towards a linear satisfiability test for BST(∪, Disj, 6=), let ϕ be a satisfiable
BST(∪, Disj, 6=)-conjunction of the form
^p ^q
∪Li 6= ∪Ri ∧ Disj(∪Lj , ∪Rj ), (3)
i=1 j=p+1
where the Lh ’s and the Rh ’s are nonempty collections of set variables, and let
M be a set assignment over Vars(ϕ) satisfying ϕ.S
q
Preliminarily, we observe that, for each x ∈ j=p+1 (∪Lj ∩ ∪Rj ), M x ⊆
M (∪Lj ) ∩ M (∪Rj ) holds for some j ∈ {p + 1, . . . , q}. Hence, since the conjunct
Disj(∪Lj , ∪Rj ) occurs in ϕ, we have M (∪Lj ) ∩ M (∪Rj ) = ∅, which in turn
yields M x = ∅.
Next, for each conjunct of type ∪ Li 6= ∪Ri in ϕ, if any, we have M (∪Li ) 6=
M (∪Ri ), i.e., M (∪Li ) ∪ M (∪Ri ) \ M (∪Li ) ∩ M (∪Ri ) 6= ∅, and a fortiori
M (∪Li ) ∪ M (∪Ri ) 6= ∅. Thus, there is an x ∈ ∪Li ∪ ∪Ri suchSthat M x 6= ∅,
q
and therefore the preceding observaton implies (∪Li ∪ ∪Ri ) \ j=p+1 (∪Lj ∩
∪Rj ) 6= ∅. Summarizing, we have shown that, by assuming the satisfiability of
ϕ, then the following condition is fulfilled:
Sq
(C1) (∪Li ∪ ∪Ri ) \ j=p+1 (∪Lj ∩ ∪Rj ) 6= ∅, for every i = 1, . . . , p.
Conversely, let ϕ be a BST(∪, Disj, 6=)-conjunction of the form (3) for which
the
Sq condition (C1) is true, and let x1 , . . . , xk be the distinct variables in Vars(ϕ)\
j=p+1 (∪ L j ∩ ∪ R j ). Consider any assignment M ∗
over Vars(ϕ) such that
q
- M ∗ := ∅, for each x ∈ j=p+1 (∪Lj ∩ ∪Rj ), and
S
- M ∗ x1 , . . . , M ∗ xk are nonempty pairwise disjoint sets.
Then, it is not hard to check that M ∗ satisfies ϕ. Thus, we have proved the
following lemma, which readily yields a satisfiability test for BST(∪, Disj, 6=).
Lemma 4. Let ϕ be a BST(∪, Disj, 6=)-conjunction of the form (3). Then ϕ is
satisfiable if and only if condition (C1) holds.
Concerning the complexity of the satisfiability test implicit in Lemma 4, we
observe that condition (C1) can be tested in O(|ϕ|) time, since
Sq Pq
- the set j=p+1 (∪Lj ∩ ∪Rj ) can be computed in O
j=p+1 (|Lj | + |Rj |) =
O(|ϕ|) time; Sq
- the set (∪Li ∪ ∪Ri )\ j=p+1 (∪Lj ∩ ∪Rj ) can be computed in O(|Li |+|Ri |)
time and tested
Ppfor emptiness in constant time, for each i = 1m, . . . , p, for
an overall O i=1 (|Li | + |R i | + 1) = O(|ϕ|) time.
Hence, we have:
Lemma 5. The satisfiability problem for BST(∪, Disj, 6=)-conjunctions can be
solved in linear time.
3 Conclusion and future work
We highlighted some preliminary results of an investigation aimed at identify-
ing small fragments of set theory endowed with polynomial-time satisfiability
decision tests, potentially useful for automated proof verification. In this ini-
tial phase, we mainly focused on ‘Boolean Set Theory’, namely the fragment of
quantifier-free formulae of set theory involving variables, the Boolean set oper-
ators ∪, ∩, \, the Boolean relators ⊆, 6⊆, =, 6=, and the predicates ‘· = ∅’ and
‘Disj(·, ·)’, along with their opposites.
Future work will concentrate on the analysis of the sub-maximal polynomial
fragments of BST, so as to obtain a finer complexity taxonomy of the collection
of all BST fragments, and also on enriching the endowment of set operators
and relators of BST. We also plan to further deepen the study of membership
fragments of the types presented in Appendix B and, ultimately, to explore the
cases in which relators correlated to membership and Boolean set predicates are
allowed simultaneously.
References
1. Domenico Cantone. Decision procedures for elementary sublanguages of set theory.
X. Multilevel syllogistic extended by the singleton and powerset operators. J.
Automat. Reason., 7(2):193–230, June 1991.
2. Domenico Cantone, Vincenzo Cutello, and Alberto Policriti. Set-theoretic re-
ductions of Hilbert’s tenth problem. In Egon Börger, Hans Kleine Büning, and
Michael M. Richter, editors, CSL ’89, 3rd Workshop on Computer Science Logic,
Kaiserslautern, Germany, October 2-6, 1989, Proceedings, volume 440 of Lecture
Notes in Computer Science, pages 65–75. Springer, 1990.
3. Domenico Cantone, Alfredo Ferro, and Eugenio G. Omodeo. Computable set theory.
Number 6 in International Series of Monographs on Computer Science, Oxford
Science Publications. Clarendon Press, Oxford, UK, 1989.
4. Domenico Cantone, Eugenio G. Omodeo, and Alberto Policriti. The automation of
syllogistic. II: Optimization and complexity issues. J. Automat. Reason., 6(2):173–
187, June 1990.
5. Domenico Cantone, Eugenio G. Omodeo, and Alberto Policriti. Set theory for
computing - From decision procedures to declarative programming with sets. Mono-
graphs in Computer Science. Springer-Verlag, New York, 2001.
6. Domenico Cantone, Eugenio G. Omodeo, and Pietro Ursino. Formative processes
with applications to the decision problem in set theory: I. Powerset and singleton
operators. Information and Computation, 172(2):165–201, January 2002.
7. Domenico Cantone and Pietro Ursino. Formative processes with applications to
the decision problem in set theory: II. Powerset and singleton operators, finiteness
predicate. Information and Computation, 237:215–242, 2014.
8. Domenico Cantone and Pietro Ursino. An Introduction to the Technique of For-
mative Processes in Set Theory. Springer International Publishing, 2018.
9. Domenico Cantone and Calogero G. Zarba. A new fast tableau-based decision
procedure for an unquantified fragment of set theory. In R. Caferra and G. Salzer,
editors, Automated Deduction in Classical and Non-Classical Logics, volume 1761
of Lecture Notes in Artificial Intelligence, pages 127–137. Springer-Verlag, 2000.
10. Alfredo Ferro, Eugenio G. Omodeo, and Jacob T. Schwartz. Decision procedures for
elementary sublanguages of set theory. I: Multilevel syllogistic and some extensions.
Commun. Pur. Appl. Math., 33:599–608, 1980.
11. Michael R. Garey and David S. Johnson. Computers and Intractability: A Guide
to the Theory of NP-Completeness. Series of Books in the Mathematical Sciences.
W. H. Freeman, 1979.
12. Nathan Jacobson. Lectures in Abstract Algebra, Vol.1 – Basic Concepts. D. Van
Nostrand, New York, 1951.
13. Yuri Ivanovich Manin. A course in mathematical logic. Graduate texts in Mathe-
matics. Springer-Verlag, 1977.
14. E. G. Omodeo and A. I. Tomescu. Set graphs. III. Proof Pearl: Claw-free graphs
mirrored into transitive hereditarily finite sets. J. Automat. Reason., 52(1):1–29,
2014.
15. Eugenio G. Omodeo, Alberto Policriti, and Alexandru I. Tomescu. On Sets and
Graphs: Perspectives on Logic and Combinatorics. Springer, 2017.
16. Jacob T. Schwartz, Domenico Cantone, and Eugenio G. Omodeo. Computational
logic and set theory: Applying formalized logic to analysis. Springer-Verlag, 2011.
Foreword by M. Davis.
A Proofs of Lemmas 1, 2, and 3
Proof of Lemma 1. Let ψ(x) be any formula expressible in T , and let Ψ (x, z)
be a T -conjunction such that
|= ψ(x) ←→ (∃z)Ψ (x, z) . (4)
Consider the mapping
ϕ(y) 7→ Ψ (x, z) (5)
from T into T , where z is any tuple of distinct set variables. Plainly, the mapping
(5) can be computed in O(1)-time. In addition, by (4), we have
|= ϕ(y) ∧ ψ(x) ←→ ϕ(y) ∧ (∃z)Ψ (x, z) .
Hence, in particular, the formulae ϕ(y) ∧ ψ(x) and ϕ(y) ∧ (∃z)Ψ (x, z) are equi-
satisfiable, and we also have
|= ϕ(y) ∧ ψ(x) −→ (∃z)Ψ (x, z).
Thus, conditions (b) and (c) of Definition 2 are also satisfied, proving that the
formula ψ(x) is O(1)-expressible in T .
Proof of Lemma 2. (a) |= x = y \ z ←→ (x ∩ z =∅ ∧ x ∪ z = y ∪ z).
(b) |= x = y ∪ z ←→ x \ y = z \ y ∧ x \ (z \ y) = y and
|= x = y ∩ z ←→ x = y \ (y \ z).
(c) |= x = y ←→ x ⊆ y ∧ y ⊆ x.
(d) |= x ⊆ y ←→ x ∪ y = y and |= x ⊆ y ←→ x ∩ y = x
(e) |= x * y ←→ x ∪ y 6= y and |= x * y ←→ x ∩ y 6= x
(f) We have that:
– |= x 6= ∅ ←→ (∃y, z)(y ⊆ x ∧ z ⊆ x ∧ z 6= y),
– from the latter and (c), it follows that x 6= ∅ is also expressible in
BST(∪, =, 6=),
– |= x 6= ∅ ←→ (∃y)(x * y),
– |= x 6= ∅ ←→ (∃y)(x 6= y ∧ Disj(y, y)),
– |= x 6= ∅ ←→ (∃y)(x 6= y ∧ y = ∅),
– |= x 6= ∅ ←→ ¬Disj(x, x),
(g) |= x = ∅ ←→ Disj(x, x).
(h) We have that:
– |= Disj(x, y) ←→ x ∩ y = ∅ and |= Disj(x, y) ←→ x \ (x \ y) = x \ x,
– |= ¬Disj(x, y) ←→ x ∩ y 6= ∅ and |= ¬Disj(x, y) ←→ (∃z)(z ⊆ x ∧ z ⊆
y ∧ z 6= ∅).
(i) |= x ∩ y 6= ∅ ←→ (∃w, w0 ) w ⊆ x ∧ w ⊆ y ∧ w0 ⊆ w ∧ w0 6= w .
From the latter and (d), it follows that ¬Disj(x, y) is also expressible in
BST(∪, =, 6=).
(j) By way of contradiction, assume that there exists a BST(∪, ∩, =, 6=)-
conjunction Φ∅ (x, y) such that
|= x = ∅ ←→ (∃y) Φ∅ (x, y) (6)
(so that (∃y)Φ∅ (x, y), and therefore Φ∅ (x, y), is satisfiable).
Let M be any set assignment such that M |= Φ∅ (x, y), and set M 0 z := M z ∪
C, for every z ∈ Vars(Φ∅ ), where C is any nonempty set that is disjoint from
M z, for every z ∈ Vars(Φ∅ ) (namely, such that C ∩ ∪M (Vars(Φ∅ )) = ∅).
Then, for y1 , . . . , yn ∈ Vars(Φ∅ ), we have:
M 0 (y1 ∪ . . . ∪ yn ) = M 0 y1 ∪ . . . ∪ M 0 yn
= (M y1 ∪ C) ∪ . . . ∪ (M yn ∪ C)
= (M y1 ∪ . . . ∪ M yn ) ∪ C
= M (y1 ∪ . . . ∪ yn ) ∪ C
and
M 0 (y1 ∩ . . . ∩ yn ) = M 0 y1 ∩ . . . ∩ M 0 yn
= (M y1 ∪ C) ∩ . . . ∩ (M yn ∪ C)
= (M y1 ∩ . . . ∩ M yn ) ∪ C
= M (y1 ∩ . . . ∩ yn ) ∪ C.
Therefore:
(j1 ) if the literal y1 ∪ . . . ∪ yn = z1 ∪ . . . ∪ zm is in Φ∅ , then
M 0 (y1 ∪ . . . ∪ yn ) = M (y1 ∪ . . . ∪ yn ) ∪ C
= M (z1 ∪ . . . ∪ zm ) ∪ C = M 0 (z1 ∪ . . . ∪ zm );
(j2 ) if the literal y1 ∩ . . . ∩ yn = z1 ∩ . . . ∩ zm is in Φ∅ , then
M 0 (y1 ∩ . . . ∩ yn ) = M (y1 ∩ . . . ∩ yn ) ∪ C
= M (z1 ∩ . . . ∩ zm ) ∪ C = M 0 (z1 ∩ . . . ∩ zm );
(j3 ) if the literal y 6= z is in Φ∅ , then we have
M 0 y = M y ∪ C, M 0 z = M z ∪ C, and M y 6= M z.
Since C is disjoint from M y and M z, then M 0 y 6= M 0 z.
From (j1 ), (j2 ), and (j3 ), it follows that M 0 |= Φ∅ , so that we have also
M 0 |= (∃y)Φ∅ .
In addition, we have M 0 x = M x ∪ C 6= ∅. Thus, M 0 6|= (∃y)Φ∅ −→
x = ∅, contradicting (6), hence showing that x = ∅ is not expressible
in BST(∪, ∩, =, 6=).
(k) If x = y \ z were expressible in BST(∪, ∩, =, 6=), then there would exist a
conjunction Ψ (x, y, z, w) in BST(∪, ∩, =, 6=) such that
|= x = y \ z ←→ (∃w)Ψ (x, y, z, w). (7)
From (7), we have
|= x = y \ y ←→ (∃w)Ψ (x, y, y, w).
Since
|= x = y \ y ←→ (∃w)Ψ (x, y, y, w)
=⇒ |= x = ∅ ←→ (∃w)Ψ (x, y, y, w)
=⇒ |= (∀y) x = ∅ ←→ (∃w)Ψ (x, y, y, w)
=⇒ |= (∀y) (∃w)Ψ (x, y, y, w) −→ x = ∅
∧ x = ∅ −→ (∃w)Ψ (x, y, y, w)
=⇒ |= (∀y)((∃w)Ψ (x, y, y, w) −→ x = ∅)
∧ (∀y) x = ∅ −→ (∃w)Ψ (x, y, y, w)
=⇒ |= (∀y)¬(∃w)Ψ (x, y, y, w) ∨ x = ∅
∧ x = ∅ −→ (∀y)(∃w)Ψ (x, y, y, w)
=⇒ |= ¬(∃w)(∃y)Ψ (x, y, y, w) ∨ x = ∅
∧ x = ∅ −→ (∃w)(∃y)Ψ (x, y, y, w)
=⇒ |= (∃w)(∃y)Ψ (x, y, y, w) −→ x = ∅
∧ x = ∅ −→ (∃w)(∃y)Ψ (x, y, y, w)
=⇒ |= x = ∅ ←→ (∃w)(∃y)Ψ (x, y, y, w),
then
|= x = ∅ ←→ (∃w)(∃y)Ψ (x, y, y, w),
i.e., x = ∅ would be expressible in BST(∪, ∩, =, 6=), contradicting (j). Thus,
x = y \ z is not expressible in BST(∪, ∩, =, 6=).
We state without proof the following model-theoretic property for the frag-
ment BST(∪, =, 6=).
Proposition 1. Let ϕ be a satisfiable conjunction of BST(∪, =, 6=) and x any
variable such that ^
|= ϕ ∧ z ∪ x = z.
z∈Vars(ϕ)
Then ϕ has a model M such that M x = ∅.
Proof of Lemma 3. Let ϕ 7→ Ψϕ (y, x) be the mapping from BST(∪, =, 6=) into
itself where ^
Ψϕ (y, x) := z ∪ x = z.
z∈Vars(ϕ)
V
Plainly, |= x = ∅ −→ z∈Vars(ϕ) z ∪ x = z. Hence, a fortiori,
^
|= (ϕ(y) ∧ x = ∅) −→ z ∪ x = z,
z∈Vars(ϕ)
proving condition (c) of Definition 2.
V As for condition (b) of Definition 2, we have to show that if ϕ(y) ∧
z∈Vars(ϕ) z ∪ x = z is satisfiable, so is ϕ(y) ∧ x = ∅. But this follows at
once from Proposition 1. V
Finally, by observing that the mapping ϕ 7→ z∈Vars(ϕ) z ∪ x = z can
clearly be computed in O(n)-time, it follows that the literal x = ∅ can be
O(n)-expressed in BST(∪, =, 6=).
B Complexity taxonomy for small fragments in presence
of the membership relation
In this appendix we present a quick overview of the complexity taxonomy for
the fragment Th(∪, ∩, \, ∈, ∈),
/ which from now on we refer to as MST, acronym
for membership set theory.
The number of distinct fragments of MST is 24, of which 10 are NP-complete
and 14 are polynomial. Much as for BST, the complexity of any fragment of
MST can be efficiently determined once the minimal NP-complete fragments
and the maximal polynomial fragments have been singled out. Table 3 shows
the minimal NP-complete and the maximal polynomial fragments of MST.
∪ ∩ \ ∈ ∈
/ Complexity
? ? NP-complete
? ? ? NP-complete
? ? ? O(n)
? ? ? O(n2 )
? ? ? ? O(1)
Table 3. Maximal polynomial and minimal NP-complete fragments of MST
The maximal polynomial fragment MST(∪, ∩, \, ∈) / is trivial as it contains
only satisfiable conjunctions, thereby admitting a O(1) satisfiability test.
Indeed, every MST(∪, ∩, \, ∈)-conjunction
/ ϕ is satisfied by the null set as-
signment M∅ , sending each x ∈ Vars(ϕ) to ∅.
We provided a O(n) satisfiability test for the fragment MST(∪, ∈). Then
we managed to translate any MST(∪, ∈, ∈)-conjunction
/ into an equisatisfiable
MST(∪, ∈)-conjunction in O(n) time, which resulted in a O(n) satisfiability test
for MST(∪, ∈, ∈).
/
We also provided a O(n2 )-time satisfiability test for the fragment MST(∩, ∈),
which was extended into a satisfiability test for the fragment MST(∩, ∈, ∈) / that
retains the same complexity.
Finally, the fragments MST(∪, ∩, ∈) and MST(\, ∈) were proved to be NP-
complete. We remark that using the axiom of regularity was necessary to prove
the NP-completeness of the former fragment, while regularity was not needed to
prove the NP-completeness of the latter.