=Paper=
{{Paper
|id=Vol-1195/long11
|storemode=property
|title=Herbrand-Satisfiability of a Quantified Set-theoretical Fragment
|pdfUrl=https://ceur-ws.org/Vol-1195/long11.pdf
|volume=Vol-1195
|dblpUrl=https://dblp.org/rec/conf/cilc/CantoneLA14
}}
==Herbrand-Satisfiability of a Quantified Set-theoretical Fragment==
https://ceur-ws.org/Vol-1195/long11.pdf
Herbrand-satisfiability of a Quantified
Set-theoretical Fragment?
Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo
Dipartimento di Matematica e Informatica, Università di Catania, Italy
{cantone, longo, nicolosi}@dmi.unict.it
Abstract. In the last decades, several fragments of set theory have been
studied in the context of the so-called Computable Set Theory. In gen-
eral, the semantics of set-theoretical languages di↵ers from the canonical
first-order semantics in that the interpretation domain of set-theoretical
terms is fixed to a given universe of sets, as for instance the von Neu-
mann standard cumulative hierarchy of sets, i.e., the class consisting of
all the pure sets. Because of this, theoretical results and various machin-
ery developed in the context of first-order logic cannot be easily adapted
to work in the set-theoretical realm. Recently, quantified fragments of
set-theory which allow one to explicitly handle ordered pairs have been
studied for decidability purposes, in view of applications in the field of
knowledge representation. Among other results, a NexpTime decision
procedure for satisfiability of formulae in one of these fragments, 8⇡0 , has
been provided. In this paper we exploit the main features of such a de-
cision procedure to reduce the satisfiability problem for the fragment 8⇡0
to the problem of Herbrand satisfiability for a first-order language ex-
tending it. In addition, it turns out that such reduction maps formulae of
the Disjunctive Datalog subset of 8⇡0 into Disjunctive Datalog programs.
1 Introduction
The quantified fragment of set-theory 8⇡0 (see [3]) allows the explicit manipu-
lation of ordered pairs. It is expressive enough to include a relevant amount of
set-theoretic constructs, in particular map-related ones: in fact, it is character-
ized by the presence of terms of the form [·, ·] (ordered pair) and ⇡
¯ (·) (collection
of the non-pair members of its argument). This language has applications in the
field of knowledge representation. In fact, a large amount of description logic con-
structs are expressible in it. In particular, the very expressive description logic
DLh8⇡0 i can be expressed in a sublanguage of 8⇡0 which has an NP-complete
decision problem, in contrast with the description logic SROIQ (cf. [9]), which
underpins the current standard language for Semantic Web OWL21 and whose
decision problem is N2ExpTime-complete (see [10]). Despite of these desirable
?
This work has been supported by the project PON04a2 A “PRISMA - PiattafoRme
cloud Interoperabili per SMArt-government.”
1
http://www.w3.org/TR/owl2-primer/
162
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
properties of the language 8⇡0 , no decision procedure for it has been implemented
yet.
In general, the semantics of set-theoretical languages (see [11] for an in-
troduction to set theory, and [5, 12] for an overview on decidable fragments of
set-theory) di↵ers from the canonical first-order semantics (see [7]) in that the
interpretation domain of set-theoretical terms is based on the von Neumann
standard cumulative hierarchy of sets V. This is the class consisting of all the
pure sets, and is recursively defined by
V0 = ;
V +1 = P(V
S ), for each ordinal
V = µ< Vµ , for each limit ordinal
S
V= 2On V ,
where P(·) is the powerset operator and On denotes the class of all ordinals.
Because of such peculiarity of set-theoretical languages, reusing of theoreti-
cal results and machinery developed in the context of first-order logic for set-
theoretical matters is not straightforward.
In this paper we show that these difficulties can be circumvented for the
fragment 8⇡0 by encoding some axioms of set theory (namely regularity and a
weak form of extensionality) as 8⇡0 -formulae. More specifically, we will prove that,
for every 8⇡0 -formula ', one can construct in polynomial time a corresponding
8⇡0 -formula ' such that ' admits a set-theoretical model if and only if ' ^ '
admits a Herbrand model (cf. [8]), when set-theoretic predicates in ' ^ ' are
regarded as uninterpreted predicates.
It turns out that these formulae ' can be considered as DATALOG_,¬ pro-
grams. As a consequence, the reduction we are going to discuss can be seen as
a reduction from 8⇡0,D_ to DATALOG_,¬ , where 8⇡0,D_ consists of the formulae
in 8⇡0 which satisfy the syntactic constraints required to be regarded also as
DATALOG_,¬ programs.
We recall that DATALOG_,¬ (read Disjunctive Datalog, see [6]) extends Dat-
alog by allowing disjunctions in the head of program rules. Decidability and
complexity of Datalog extensions with various combinations of disjunction and
negation has been studied. Also, optimization strategies have been provided for
algorithms devised in this context, and a considerable amount of academic and
commercial software implementing these algorithms is available (see for exam-
ple [1]). Thus, the reduction we present in this paper allows one to reuse the
machinery available for DATALOG_,¬ in the implementation of an optimized
reasoning engine for the language 8⇡0,D_ and, consequently, for the description
logic DLh8⇡0 i mentioned before, as all the constructs in DLh8⇡0 i are expressible
in 8⇡0,D_ .
The link between set-theoretical languages and logic programming we start
to investigate here is of a certain interest to projects related with the production
and usage of open data such as P RISM A⇤ : on one hand, it provides a way to
implement with small e↵orts a solid and efficient reasoning and query engine for
the very expressive representation language DLh8⇡0 i; on the other hand, it allows
163
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
one to implement typical logic-programming tasks for DLh8⇡0 i knowledge bases
such as, for example, answer-set programming and non-monotonic reasoning,
which may be of some interest for public utility applications.
The rest of the paper is organized as follows. In Section 2 we review some
notions and definitions from first-order logic, including the definition of the Dis-
junctive Datalog fragment of first-order logic. Then, in Section 3, after recalling
the syntax and semantics of the fragment of set-theory 8⇡0 , we briefly review a
decision procedure for 8⇡0 -formulae, together with some lemmas useful to our
needs. A polynomial-time reduction of the satisfiability problem for 8⇡0 -formulae
to the Herbrand satisfiability problem for first-order formulae is described in
Section 4. Finally, we draw our conclusions and provide some hints for future
research in Section 5.
2 Preliminaries
We briefly review some notations and definitions from first-order logic which will
be used throughout the paper.
We shall denote with Vars = {x, y, z, . . .} and Consts = {a, b, c . . .} two denu-
merably infinite collections of variables and constants, respectively.2 In addition,
we denote with Preds = {P, Q, R, . . .} a denumerably infinite set of predicate
symbols, and with ar : Preds ! N the related arity function.
Atomic formulae are expressions of the following form
P (⌫1 , . . . , ⌫n ),
where P 2 Preds, ar (P ) = n, and {⌫1 , . . . ⌫n } 2 Vars [ Consts. Literals are
atomic formulae or their negations. Quantifier-free formulae are propositional
combinations of atomic formulae; thus, in particular, literals are quantifier-free
formulae. Universally quantified prenex-formulae are expressions of the following
form
(8x1 ) . . . (8xn ) ,
where n 2 N, {x1 , . . . xn } ✓ Vars and is a quantifier-free formula. In the rest
of the paper we will sometime abbreviate quantifier prefixes as (8x1 ) . . . (8xn )
by (8x1 , . . . , xn ). Here we do not mention existential quantifiers because they do
not serve our purposes. However, notice that constants and free variables3 may
be regarded as existentially quantified variables when dealing with satisfiability.
In addition, quantifier-free formulae can be considered as universally quantified
prenex formulae with an empty quantifier prefix.
We consider also restricted universal quantifiers, i.e., quantifiers of the form
(8x1 , . . . , xn |P (x1 , . . . , xm )) ,
2
We do not mention function symbols here as we are going to consider function-free
languages only.
3
An occurrence of a variable x is free in a formula if it does not fall within the scope
of the quantifier (8x).
164
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
where 1 m n, x1 , . . . , xn are variables, and P is a predicate of arity m, whose
intended meaning is that (universal) quantification is restricted to all x1 , . . . , xn
such that P (x1 , . . . , xm ) holds. Notice, however, that restricted universal quan-
tifiers can easily be expressed by universally quantified prenex formulae, by way
of the following equivalence:
(8x1 , . . . , xn |P (x1 , . . . , xm )) ⌘ (8x1 , . . . , xn )(P (x1 , . . . , xm ) ! ).
Given any formula ', we denote with Preds('), Consts('), and Vars(') the
sets of the predicate symbols, constant symbols, and variables occurring in ',
respectively. Analogously, for a set ⌃ of formulae, we denote with Preds(⌃),
Consts(⌃), and Vars(⌃) the sets of all the predicate symbols, constant symbols,
and variables occurring in any formula ' 2 ⌃, respectively.
We denote with '[x ! y] the formula obtained from ' by replacing every
free occurrence of x with y.
A formula is said to be ground if no variable occurs in it. It is said to be closed
(or to be a sentence) if no free variable occurs in it, i.e., if every variable x in it
occurs ony within the scope of the quantifier (8x). Plainly, ground formulae are
closed.
Finally, given any set ⌃ of atomic formulae and any atomic formula , with
a slight abuse of notation we write ⌃ |= to express that is a member of ⌃,
i.e., 2 ⌃. Likewise, we write ⌃ 6|= when 62 ⌃.
First-order interpretations, whose universe is Consts and such that each con-
stant is interpreted by itself,4 are called Herbrand interpretations. Plainly, a
Herbrand interpretation is characterized by the set of ground atomic formulae
which are evaluated to true by it. A Herbrand interpretation H is said to be a
Herbrand model for a formula ' if it evaluates ' to true, in which case we write
H |= '.
A formula is said to be Herbrand-satisfiable if and only if it admits a Her-
brand model. It is a fundamental result of first-order logic that, for satisfiability
purposes, it is not restrictive to limit oneself to Herbrand satisfiability, since a
formula is satisfiable if and only if it is Herbrand-satisfiable. Additionally, when
considering a (function-free) universally quantified prenex sentence ', the search
space for Herbrand models of ' can be limited to Herbrand interpretations over
the constants occurring in it. This result can easily be generalized to finite con-
junctions of universally quantified prenex sentences, as stated in the following
theorem.
Theorem 1. Let ' be a finite conjunction of universally quantified prenex sen-
tences. Then ' is satisfiable if and only if it admits a Herbrand model H whose
universe coincides with the set Consts(H), if Consts(H) 6= ;, otherwise is any
singleton. t
u
We conclude this section by recalling the DATALOG_,¬ first-order fragment.
Notice that DATALOG_,¬ -formulae are often referred to also as programs, so that
4
We recall that we are assuming that there are no function symbols.
165
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
the expressions “DATALOG_,¬ -formulae” and “DATALOG_,¬ -programs” must be
regarded as synonyms. A DATALOG_,¬ -formula is a finite conjunction of rules,
i.e., closed formulae of the following form
(8x1 ) . . . (8xn )(' ! ) ,
where ' (the rule body) is a conjunction of literals, (the rule head ) is a dis-
junction of literals, and Vars( ) ✓ Vars(') (safety condition). Facts are special
ground rules whose body is always true. For this kind of rules, one may omit
to indicate the rule body. Thus facts can just be regarded as disjunctions of
ground literals. They are used to express facts about real world items, such as
for example childOf (Alice, Bob), isM ale(Bob), etc.
Finally, we observe that restricted universal quantifiers can easily be embed-
ded in DATALOG_,¬ rules and formulae. Indeed, let us consider a closed formula
of the form
(8x1 , . . . , xn |P (x1 , . . . , xm ))(' ! ) , (1)
where ' is a conjunction of literals, is a disjunction of literals, Vars( ) ✓
Vars(') [ {x1 , . . . , xm }, and P is a predicate symbol of arity m. Then, as re-
marked above, (1) is equivalent to the closed formula
(8x1 , . . . , xn )(P (x1 , . . . , xm ) ! (' ! )),
which, in its turn, is equivalent to the closed formula
(8x1 , . . . , xn )((P (x1 , . . . , xm ) ^ ') ! ). (2)
Plainly, (2) is a (standard) DATALOG_,¬ -rule, with body (P (x1 , . . . , xm ) ^ ').
3 The language 8⇡0
We recall the syntax and semantics of the set-theoretic language 8⇡0 , whose
decision problem has been studied in [3]. Atomic 8⇡0 -formulae are of the following
types
⌫2⇡ ¯ (µ), [⌫, ⌫ 0 ] 2 µ, ⌫ = µ (3)
with ⌫, ⌫ 0 , µ 2 Vars [ Consts. Intuitively. a formula of type ⌫ 2 ⇡ ¯ (µ) expresses
that ⌫ is a non-pair member of µ, whereas a formula of type [⌫, ⌫ 0 ] 2 µ ex-
presses that the pair [⌫, ⌫ 0 ] belongs to µ. Atomic 8⇡0 -formulae and their negations
are called 8⇡0 -literals. Quantifier-free 8⇡0 -formulae are Boolean combinations of
atomic 8⇡0 -formulae. Simple-prenex 8⇡0 -formulae have the following form:
(8x1 2 ⇡
¯ (a1 )) . . . (8xn 2 ⇡
¯ (an ))(8 [y1 , z1 ] 2 b1 ) . . . (8 [ym , zm ] 2 bm ) ,
where n, m 0, xi 2 Vars and ai 2 Consts, for 1 i n, yj , zj 2 Vars
and bj 2 Consts, for 1 j m, and is a quantifier-free 8⇡0 -formula. The
constants a1 , . . . , an , b1 , . . . bm are the domain constants of the simple-prenex
8⇡0 -formula under consideration. Finally, 8⇡0 -formulae are finite conjunctions of
166
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
closed simple-prenex 8⇡0 -formulae. The collection of the domain constants of a 8⇡0 -
formula ', which we denote with Consts D ('), consists of the domain constants
of all of its conjuncts.
Semantics of the language 8⇡0 is based on the von Neumann standard cumu-
lative hierarchy of sets, briefly reviewed in Section 1. Other set-theoretic notions
particularly useful to our purposes are those of Cartesian product and of ordered
pairs. Let ⇡ be a binary operation which associates to each pair of sets u, v 2 V
another set in V (i.e., ⇡(u, v) 2 V). Then the Cartesian product of u, v 2 V with
respect to ⇡, denoted by u ⇥(⇡) v, is defined by
u ⇥(⇡) v = Def {⇡(u0 , v 0 ) | u0 2 u ^ v 0 2 v}.
The binary operation ⇡ is said to be a pairing function if and only if the following
two conditions hold for any u, v, u0 , v 0 2 V:
1. ⇡(u, v) = ⇡(u0 , v 0 ) () u = u0 ^ v = v 0 ,
2. u ⇥(⇡) v is a set in V.
Let ⇡ be a pairing function, and let u be a set in the von Neumann cumulative
hierarchy. We denote with ⇡ ¯ (u) the collection of the members of u which are not
pairs, with respect to the pairing function ⇡.
The semantics for 8⇡0 -formulae is given in terms of pair-aware set-theoretical
interpretations. These are first-order interpretations I whose domain is V (so
that pure sets are assigned to constants and variables) and such that:
– the membership predicate 2 is interpreted as the membership relation among
sets in V;
– the pairing symbol [·, ·] is interpreted by a pairing function, in the sense
described above;
⇡ (x) = {u 2 Ix | (8v1 , v2 )(I[v1 , v2 ] 6= u)}, for all x 2 Vars [ Consts.
– I¯
Then, a 8⇡0 -formula ' is said to be satisfiable if and only if it admits a
pair-aware set-theoretical interpretation which satisfies it (i.e., a pair-aware set-
theoretical model). We use the notation I |=s ' to indicate that I is a pair-aware
set-theoretical model for the 8⇡0 -formula '.
The satisfiability test for 8⇡0 -formulae reported in [3] relies on the existence
of finite structures of bounded size, called skeletal representations, which witness
the existence of certain particular models called realizations (see Definitions 1
and 2).
The definition of skeletal representation adopted in this paper di↵ers slightly
from the one presented in [3]. In particular, here we extend the notion of skeletal
representation so as to also encapsulate the notion of V-extensionality and the
technical condition (i) of Theorem 3 in [3]. It turns out that all the lemmas and
theorems in [3] can be adapted to cope with this extended definition of skeletal
representation. A reformulation of Theorem 3 in [3], which is central for the
satisfiability problem for 8⇡0 -formulae, is reported in Theorem 2 below.
In the following definition, we shall make use of the membership closure
relation 2+ ⇡
S of a set S of atomic 80 -formulae. This is the minimal transitive
relation on Consts(S) such that, for a, b, c 2 Consts(S), we have
167
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
– if S |= a 2 ⇡¯ (b) then a 2+
S b, and
– if S |= [a, b] 2 c then a 2+ +
S c and b 2S c.
Definition 1 (Skeletal Representation). Let ' be a 8⇡0 -formula and let V ,
T be two disjoint sets of constants. A skeletal representation S relative to (V, T )
is a finite set of ground atomic 8⇡0 -formulae such that the following conditions
hold:
(S1) the membership relation induced by S is acyclic, i.e., a 62+ S a, for all a 2
V [ T;
(S2) if S |= a = b, for some a and b, then, for every in S, [a ! b] and
[b ! a] are both in S;
(S3) if S 6|= a = b, for some a, b 2 V , then a and b must be distinguished in S
by some constant c, in the sense that S |= c 2 ⇡ ¯ (a) i↵ S 6|= c 2 ⇡¯ (b), or by
some pair [c, d], in the sense that S |= [c, d] 2 a i↵ S 6|= [c, d] 2 b;
(S4) statements in S of the form a = b can involve only constants occurring in
V;
(S5) Consts(S) ✓ V [ T . t
u
Condition (S1), which is closely related to the regularity axiom of set theory,
guarantees that a skeletal representation S can be turned into a corresponding
pair-aware set-theoretic interpretation (its realization; see below). Conditions
(S2) and (S3) concern the extensionality axiom of set theory, which states that
any two sets are equals if and only if they have the same members. Finally, (S4)
and (S5) are technical conditions which, together with (S1)–(S3) in Definition
1, guarantee some properties of realizations, as reported in Lemma 1 below.
In the following definition of realization of a skeletal representation, taken
from from [3] (Definition 1), we shall make use of the family {⇡n }n2N of pairing
functions, recursively defined by
⇡0 (u, v) = Def {u, {u, v}}
⇡n+1 (u, v) = Def {⇡n (u, v)} ,
for u, v 2 V.
Definition 2 (Realization [3]). Let V and T = {t1 , t2 , . . . , tn }, with n 2 N,
be two finite, nonempty, and disjoint sets of constants, and let S be a skeletal
representation relative to (V, T ). Then the realization of S relative to (V, T ) is
the pair-aware set-theoretical model R defined as follows:
R [u, v] = Def ⇡h (u, v) for all u, v 2 V
R x = Def {R y | S |= y 2 ⇡ ¯ (x)} [ {R [y, z] | S |= [y, z] 2 x} for x 2 V
R ti = Def {R y | S |= y 2 ⇡¯ (ti )} [ {R [y, z] | S |= [y, z] 2 ti } [ for ti 2 T
{{k + 1, k, i}} ,
where h = |V | + |T | and k = |V | · (|V | + |T | + 3).5 t
u
5
We are assuming that integers are represented à la von Neumann, namely 0 = Def ;
and, recursively, n + 1 = Def n [ {n}.
168
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
The following lemma is a direct consequence of Definition 2 and of Lemma 2 in
[3].
Lemma 1. Let V , T be two finite, nonempty, and disjoint sets of constants, S
a skeletal representation relative to (V, T ), and R the realization of S relative
to (V, T ). Then
R a ✓ {R b | S |= b 2 ⇡
¯ (a)} [ {R [b, c] | S |= [b, c] 2 a} ,
for all a 2 V . In addition, the following conditions hold, for all a, b, c 2 V [ T :
– R a = R b i↵ S |= a = b;
– Ra 2 R⇡ ¯ (b) i↵ S |= a 2 ⇡
¯ (b);
– R [a, b] 2 R c i↵ S |= [a, b] 2 c. t
u
We observe that, in view of Definition 2, the names of the variables in the
set T do not a↵ect the realization of a skeletal representation relative to (V, T ).
In other words, if S is a skeletal representation relative to (V, T ), t is a constant
in T , and t0 is another constant not occurring in V [ T , then the realization
of S relative to (V, T ) and the realization of S[t ! t0 ] (i.e., the set of atomic
8⇡0 -formulae obtained from S by replacing each occurrence of t by t0 ) relative to
(V, T \ {t} [ {t0 }) coincide. In addition, if V , T are two disjoint set of constants,
and T 0 is a set of constants disjoint from V and such that T ✓ T 0 , then
– every skeletal representation S relative to (V, T ) is a skeletal representation
relative to (V, T 0 ) as well, and
– the realization of S relative to (V, T ) coincides with the realization of S
relative to (V, T 0 ).
We conclude this section by restating Theorem 3 of [3], in view of the above
observations and of Definition 1.
Theorem 2. Let ' be a 8⇡0 -formula, let V = Consts('), and let T be a set of
constants disjoint from V and such that |T | = 2 · |V |. Then ' is satisfiable if
and only if there exists a skeletal representation S relative to (V, T ) such that
the realization R of S relative to (V, T ) is a pair-aware set-theoretical model for
'. t
u
The decidability of the satisfiability problem for 8⇡0 -formulae easily follows
from Theorem 2, as the number of possible skeletal representations for any given
8⇡0 -formula is finitely bounded, and it is e↵ectively verifiable whether the real-
ization of a skeletal representation is a pair-aware set-theoretical model for a
8⇡0 -formula.
Next we define the Disjunctive Datalog subset 8⇡0,D_ of 8⇡0 as the collection
of the closed 8⇡0 -formulae whose conjuncts are closed simple-prenex 8⇡0 -formulae
of the form
(8x1 2 ⇡
¯ (a1 )) . . . (8xn 2 ⇡
¯ (an ))(8 [y1 , z1 ] 2 b1 ) . . . (8 [ym , zm ] 2 bm ) , (4)
169
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
such that has the form
( 1 ^ ... ^ l) ! ( 1 _ . . . _ h) ,
where l, h 0 and 1 , . . . , l , 1 , . . . h are 8⇡0 -literals. Since (4) is closed, each
variable x which may occur in the head of the rule must be bound, so that x
occurs in at least one atom of the rule body, as required for Disjunctive Datalog
rules, when restricted quantifiers in (4) are expanded as indicated in (2).
In the next section we present a reduction of the set-theoretic satisfiability
for 8⇡0 -formulae to Herbrand satisfiability.
4 Herbrand Satisfiability of 8⇡0 -formulae
In this section we show how to reduce the satisfiability problem for the fragment
8⇡0 to the problem of first-order Herbrand satisfiability.
For this purpose, we introduce the function-free first-order language L⇡0 which
involves, besides constants, also the following predicate symbols:
binary ternary 4-ary
b , P = , P ⇡¯ , dist, dist⇡
2 P [,] , distBy distBy⇡
Next, we define a polynomial-time reduction ' 7! ' from 8⇡0 -formulae into
L0 -formulae such that any 8⇡0 -formula ' is set-theoretically satisfiable if and
⇡
only if its image ' in L⇡0 is Herbrand-satisfiable.
In our reduction, the predicate 2 b will be used to model the transitive clo-
sure of the membership relation among sets, whereas the predicates dist, dist⇡ ,
distBy, and distBy⇡ will be used to model the fact that two sets are distinct. In
particular, the predicates dist and distBy will take care of the case in which two
sets x, y are distinguished by a set z that is not a pair, whereas the predicates
dist⇡ and distBy⇡ will take care of the case in which two sets x, y are distin-
guished by a [⌫1 , ⌫2 ]. Finally, the predicate P = (⌫1 , ⌫2 ) will be used to model
equality between ⌫1 and ⌫2 , the predicate P ⇡¯ (⌫1 , ⌫2 ) will stand for the set-
theoretic formula ⌫1 2 ⇡ ¯ (⌫2 ), and P [,] (⌫1 , ⌫2 , ⌫3 ) will stand for [⌫1 , ⌫2 ] 2 ⌫3 ,
where ⌫1 , ⌫2 , ⌫3 2 Vars [ Consts.
For the sake of clarity, with a slight abuse of notation, we shall write ⌫1 = ⌫2 ,
⌫1 2 ⇡¯ (⌫2 ), and [⌫1 , ⌫2 ] 2 ⌫3 in place of P = (⌫1 , ⌫2 ), P ⇡¯ (⌫1 , ⌫2 ) and P [,] (⌫1 , ⌫2 , ⌫3 ),
respectively, for all ⌫1 , ⌫2 , ⌫3 2 Vars [ Consts. With such an understanding, 8⇡0
can be regarded as a sublanguage of L⇡0 , and skeletal representations as Herbrand
interpretations (over L⇡0 ) subject to the conditions reported in Definition 1.
In the rest of the paper, we shall refer to the subset of a Herbrand interpre-
tation H consisting of the atomic 8⇡0 -formulae in H as the 8⇡0 -subset of H.
As a first step in our reduction, we provide a polynomial-time procedure to
construct an L⇡0 -formula (V,T ) from two disjoint sets of constants V and T ,
which enforces the conditions of Definition 1 on its models, in such a way that
– the 8⇡0 -subset of every Herbrand model H for (V,T )
is a skeletal representa-
tion relative to (V, T ), and
170
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
– every skeletal representation relative to (V, T ) can easily be extended to a
Herbrand model for (V,T ) .
Then, to complete the reduction of 8⇡0 -satisfiability to Herbrand satisfiability,
we shall prove that
S |= (V,T ) ^ ' () R |=s ',
where V , T are two disjoint sets of constants, ' is a 8⇡0 -formula such that
Consts(') = V , S is a skeletal representation relative to (V, T ), and R is the
realization of S relative to (V, T ).
Thus, let V , T be two disjoint sets of constants. The formula (V,T ) is defined
as follows:
(V,T ) (V,T ) (V,T )
= Def 1 ^ 2 ^ 3 ^ 4 ,
where
1 = Def (8x, y)(x 2 ⇡¯ (y) ! x2 b y)
^ (8x, y)([x, y] 2 z ! x2 b z)
b
^ (8x, y)([x, y] 2 z ! y 2z)
^ (8x, y, z)(x2b y ^ y2
b z ! x2 b z)
b
^ (8x)¬(x2x)
2 = Def (8x, y)(x = y ! y = x)
^ (8x, y, z)(x = y ^ y = z ! x = z)
^ (8x, y, z)(x 2 ⇡¯ (y) ^ x = z ! z 2 ⇡¯ (y))
^ (8x, y, z)(x 2 ⇡¯ (y) ^ y = z ! x 2 ⇡¯ (z))
^ (8x, y, z, v)([x, y] 2 z ^ x = v ! [v, y] 2 z)
^ (8x, y, z, v)([x, y] 2 z ^ y = v ! [x, v] 2 z)
^ (8x, y, z, v)([x, y] 2 z ^ z = v ! [x, y] 2 v)
(V,T ) V
3 = Def ¬(x = y) ! dist(x, y) _ dist⇡ (x, y)
x,y2V ✓ ◆
W
^ (8x, y) dist(x, y) ! distBy(x, y, z) _ distBy(y, x, z)
z2V [T !
W
^ (8x, y) dist⇡ (x, y) ! distBy⇡ (x, y, z, v) _ distBy⇡ (y, x, z, v)
z,v2V [T
^ (8x, y, z) distBy(x, y, z) ! (z 2 ⇡ ¯ (x) ^ ¬(z 2 ⇡¯ (y)))
^ (8x, y, z, v) distBy⇡ (x, y, z, v) ! ([z, v] 2 x ^ ¬([z, v] 2 y))
(V,T ) V
4 = Def ¬(x = t).
x2V [T,t2T,x6=t
It can be easily verified that (V,T ) is a DATALOG_,¬ -formula. The subformulae
(V,T ) (V,T )
1, 2, 3 , and 4 formalize the conditions (S1), (S2), (S3), and (S4)
of Definition 1, as clarified by the following lemma.
171
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
Lemma 2. Let V ,T be two disjoint sets of constants. Let H be a model for
(V,T )
such that Consts(H) ✓ V [ T , and let S be the 8⇡0 -subset of H. Then S
is a skeletal representation relative to (V, T ).
Proof. Plainly, S is a set of atomic 8⇡0 -formulae, since it is the 8⇡0 -subset of H.
We must prove that S satisfies all the conditions reported in Definition 1.
We first observe that the relation 2 b H = {[a, b] | H |= a2 b b} is acyclic, as H
models correctly the conjunct 1 of (V,T ) . Hence, 2+ S must be acyclic as well,
as required by Condition (S1), since 2+ S ✓ b
2 H . 6
Thus, we can conclude that S
satisfies (S1), since S ✓ H.
Next, suppose that S |= x = y, for some constants x, y 2 V [ T . Plainly,
H |= x = y. Let us consider any 8⇡0 -formula in S ✓ H involving either x or
y, say x 2 ⇡ ¯ (z). The definition of S yields that z 2 V [ T , as we are assuming
that S |= x 2 ⇡ ¯ (z). Then, H |= [x ! y], where [x ! y] is the literal y 2 ⇡ ¯ (z),
easily follows, since H models correctly the conjunct (8x, y, z)(x 2 ⇡ ¯ (y) ^ x =
z!z2⇡ ¯ (y)) of 2 . In addition, S |= y 2 ⇡ ¯ (z) holds as well, as y 2 ⇡ ¯ (z) is a
8⇡0 -formula with y, z 2 V [ T . Property (S2) for S can be proved by reasoning
in similar way, for all the 8⇡0 -formulae occurring in S.
Conversely, let x, y 2 V be such that S 6|= x = y and, consequently, H 6|= x =
y. Thus, H |= ¬(x = y), so that H |= dist(x, y) _ dist⇡ (x, y), as we are supposing
(V,T )
that H is a model for 3 . It can easily be verified that if H |= dist(x, y),
then x and y are distinguished in S by a constant (in the sense of Definition 1),
whereas, if H |= dist⇡ (x, y), then x and y are distinguished in S by a pair term.
Let us assume that H |= dist(x, y). Thus H |= distBy(x, y, z) _ distBy(y, x, z),
for some constant z 2 V [ T , so that either H |= z 2 ⇡ ¯ (x) and H 6|= z 2 ⇡ ¯ (y),
or H |= z 2 ⇡ ¯ (y) and H 6|= z 2 ⇡ ¯ (x). Then x and y are distinguished in H by
z, and, consequently, they are distinguished in S by z too, since z 2 ⇡ ¯ (x) and
z2⇡ ¯ (y) are 8⇡0 -formulae and x, y, z 2 V [ T . By reasoning as above, it can be
proved that if H |= dist⇡ (x, y) then x and y are distinguished in S by the pair
[z, v] if H |= dist⇡ (x, y), thus concluding the proof that H satisfies (S3).
Concerning (S4), by way of contradiction we prove that S |= x = y implies
that x and y are constants in V . Thus, let us assume that y 2 / V . Then y must
be in T , as T and V are disjoint, and Consts(S) ✓ Consts(H) ✓ V [ T . But H
(V,T )
must model the conjunct ¬(x = y) of 4 . Hence, we have H 6|= x = y and,
a fortiori, S 6|= x = y, since S ✓ H, contradicting our initial assumption. Thus,
y 2 V . In addition, S |= x = y yields that S |= y = x, as H models the conjunct
(8x)(x = y ! y = x) of 2 , x and y are in V [ T , and y = x is a 8⇡0 -formula.
Thus, x 2 V can be proved analogously.
Finally, (S5) holds as well, since, by assumption, Consts(S) ✓ Consts(H) ✓
V [ T. t
u
In addition, every skeletal interpretation can be extended to comply with the
constraints imposed by (V,T ) .
6
The relation 2+ b b
H does not necessarily coincide with 2H , as the minimality of 2H is
not enforced in 1 .
172
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
Lemma 3. Given two disjoint sets of constants V ,T and a skeletal represen-
tation S relative to (V, T ), there always exists a Herbrand model H (over L⇡0 )
having S as 8⇡0 -subset.
Proof. Let S be a skeletal representation relative to (V, T ), where V and T are
disjoint sets of constants. We can extend S to a Herbrand model H for (V,T ) .
Initially, we put H = Def S and then we enrich H with new atomic formulae
according to the following rules. If x 2 ⇡ b y to H. Likewise, if
¯ (y) is in S, we add x2
b b
[x, y] 2 z is in S, we add the atoms x2z and y 2z to H. Then we close transitively
H with respect to the 2 b -atoms, i.e., for each sequence of atoms in H of the form
b x2 , x2 2
x1 2 b x 3 , . . . , xn 1 2
b xn ,
we add the atom x1 2 b xn to H.
Next, for every x, y 2 V , if S 6|= x = y and x and y are distinguished in S by a
z 2 V [ T , we add to H the atoms dist(x, y) and distBy(x, y, z) (resp., dist(y, x)
and distBy(y, x, z)), provided that z 2 ⇡ ¯ (x) is in S and z 2 ⇡ ¯ (y) is not in S
(resp., z 2 ⇡ ¯ (y) is in S and z 2 ⇡
¯ (x) is not in S). Otherwise, if x and y are distin-
guished in S by a pair [z, v], with z, v 2 V [T , we add to H the atoms dist⇡ (x, y)
and distBy⇡ (x, y, z, v) (resp., dist⇡ (y, x) and distBy⇡ (y, x, z, v)), provided that
[z, v] 2 x is in S and [z, v] 2 y is not in S (resp., [z, v] 2 y is in S and [z, v] 2 x
is not in S).
In order to show that the set H so obtained is a Herbrand model for (V,T ) ,
(V,T )
we have to prove that H is a Herbrand model for the formulae 1 , 2 , 3 ,
(V,T )
and 4 .
By the very construction process, H satisfies the first four conjuncts of 1 .
In addition, H satisfies also the last conjunct (8x)¬(x2 b x) of 1 . Indeed, if this
were not the case, H would contain an atom of the form z 2 b z, for some z 2 V [T .
But this would be possible only if one of the following situations occurs:
(a) S contains an atom of one of the following three forms
z2⇡
¯ (z), [z, y] 2 z, [x, z] 2 z ,
for some x, y 2 V [ T ;
(b) H contains a sequence of atoms of the form
b x1 , x1 2
z2 b x 2 , . . . , xn 1 2
b xn , xn 2
bz ,
with xi 2 V [ T for 1 i n.
However, case (a) cannot occur, since, by condition (S1), the membership rela-
tion induced by S is acyclic. We show that also case (b) cannot occur, thereby
proving that H cannot contain any atom of the form z 2 b z. Indeed, if (b) were
true, then H would contain a maximal sequence of atoms of the form
b x1 , x1 2
x0 2 b x 2 , . . . , xn 1 2
b xn , xn 2
b xn+1 ,
173
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
where x0 and xn+1 coincide. But then, for each i = 0, 1, . . . , n, S would contain
at least an atom of one of the following types
xi 2 ⇡
¯ (xi+1 ), [xi , w] 2 xi+1 , [w, xi ] 2 xi+1 ,
with w 2 V [ T , and therefore the membership relation 2+
S induced by S would
contain a cycle, contradicting condition (S1).
Summing up, H satisfies also the last conjunct of 1 , and hence it satisfies
the whole formula 1 .
(V,T )
To show that H satisfies 2 and 3 , it is enough to observe that S ✓ H
and that S satisfies conditions (S2) and (S3), respectively.
Finally, since (again) S ✓ H and S satisfies condition (S4), it follows that H
(V,T )
satisfies also the formula 4 , as no new atom of the form x = y can possibly
be introduced into H during its construction.
Hence, in conclusion, H is a Herbrand model for the formula (V,T ) . t
u
As already remarked, the following lemma exploits a semantical correspon-
dence between pair-aware set-theoretical models and Herbrand models of 8⇡0 -
formulae.
Lemma 4. Let V , T be two disjoint sets of constants and let H be a Herbrand
interpretation such that H |= (V,T ) and Consts(H) ✓ V [ T . Let S be the
8⇡0 -subset of H, and let R be the realization of S relative to V , T . Then
H |= ' () R |=s ' ,
for every 8⇡0 -formula ' such that Consts(') ✓ V [ T and Consts D (') ✓ V .
Proof. It will be enough to prove the lemma in the case of simple-prenex 8⇡0 -
formulae, as general 8⇡0 -formulae are just finite conjunctions of simple-prenex
8⇡0 -formulae. Accordingly, in the rest of this proof we will assume that ' is a
simple-prenex 8⇡0 -formula.
We proceed by induction on the quantifier prefix length of '. Preliminarily,
we observe that
H |= () R |=s ,
for each atomic 8⇡0 -formula such that Consts( ) ✓ V [ T (see Lemma 1), so
that the lemma follows easily from propositional logic when ' is quantifier-free.
For the inductive case, let us first assume that ' = (8x 2 ⇡ ¯ (a)) , for some x 2
Vars and a 2 Consts, where is a simple-prenex 8⇡0 -formula with one less quan-
tifier than '. Since R is a realization, we plainly have R ⇡ ¯ (a) = {R b | H |= b 2
¯ (a)}, so that R models correctly (8x 2 ⇡
⇡ ¯ (a)) if and only if it correctly models
all the formulae [x ! b] such that H |= b 2 ⇡ ¯ (a). Observe that, for all the con-
stants b such that H |= b 2 ⇡ ¯ (a), we have Consts D ( [x ! b]) = Consts D ( ) =
Consts D (') \ {a} ✓ V , and Consts( [x ! b]) ✓ Consts( ) [ {b} ✓ Consts(') [
{b} ✓ V [ T , as we have assumed that Consts(') [ Consts(H) ✓ V [ T . Thus
R |=s [x ! b] () H |= [x ! b],
174
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
for each b such that H |= b 2 ⇡
¯ (a), and, consequently,
R |=s (8x 2 ⇡
¯ (a)) () H |= (8x 2 ⇡
¯ (a))
follows by applying the inductive hypothesis to the formulae [x ! b], for all b
such that H |= b 2 ⇡ ¯ (a).
Next, let us consider the case in which ' has the form (8[x, y] 2 a) , with
x, y 2 Vars, a 2 Consts, and a simple-prenex 8⇡0 -formula with one less quan-
tifier than '. In this case we must consider the set R a \ R ⇡ ¯ (a) of the pair
members of R a. But, R a \ R ⇡ ¯ (a) = {R [b, c] | H |= [b, c] 2 a}, by Lemma 1,
and thus R models (8[x, y] 2 a) if and only if it correctly models the formula
[x ! b][y ! c], for all a, b such that H |= [b, c] 2 a. Thus, the thesis follows by
reasoning much as in the previous case, by applying the inductive hypothesis to
the formulae [x ! b][y ! c], for all a, b such that H |= [b, c] 2 a t
u
Finally, the next theorem states that the satisfiability of every 8⇡0 -formula
' can be decided by checking the Herbrand satisfiability of the corresponding
L⇡0 -formula (V,T ) ^ ', thus concluding the verification of the correctness of our
reduction.
Theorem 3. Let ' be a 8⇡0 -formula, let V = Consts('), and let T be any set of
constants disjoint from V such that such that |T | = 2 · |V |. Then ' is satisfiable
if and only if (V,T ) ^ ' is Herbrand-satisfiable.
Proof. To begin with, let us assume that ' is satisfiable. Then, by Theorem 2,
there exists a skeletal representation S (relative to (V, T )) such that its realiza-
tion R relative to (V, T ) is a pair-aware set-theoretical model for '. In addition,
by Lemma 2, there exists a Herbrand interpretation H with S as its 8⇡0 -subset,
which correctly models (V,T ) , and such that Consts(H) = Consts(S). Thus,
H |= ' directly follows from Lemma 4.
Conversely, let H be a Herbrand model for (V,T ) ^ ', and let S be the 8⇡0 -
subset of H. We have Consts(H) ✓ V [ T , as Consts (V,T ) = V [ T and
Consts(') = V . In addition, from Lemma 2 and from H |= (V,T ) , S is a skeletal
representation. Thus, by Lemma 4, the realization of S relative to (V, T ) must
be a model for '. t
u
We conclude this section by observing that, if ' is a 8⇡0,D_ -formula, then
^ ' is a DATALOG_,¬ -formula, as (V,T ) is a DATALOG_,¬ -formula. Thus
(V,T )
the satisfiability problem for 8⇡0,D_ -formulae can be reduced in polynomial time
to the Herbrand satisfiability problem for DATALOG_,¬ -formulae.
Corollary 1. Let ' be a 8⇡0,D_ -formula. Let V = Consts(') and let T be any
set of constants disjoint from V and such that |T | = 2 · |V |. Then ' is set-
theoretically satisfiable if and only if the corresponding DATALOG_,¬ -formula
(V,T )
^ ' is satisfiable, in the sense of Disjunctive Datalog. t
u
175
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
5 Conclusions and Future Works
In this paper we have identified a correspondence between the fragment of set-
theory 8⇡0 and first-order logic (in particular Herbrand logic) by providing a
polynomial-time reduction of 8⇡0 -formulae to formulae in a first-order language,
called L⇡0 , suitable for this purpose. In addition, we have shown that if we limit
ourselves to the Disjunctive Datalog restriction of 8⇡0 called 8⇡0,D_ , then our
reduction maps formulae in this subfragment to DATALOG_,¬ -formulae.
Such correspondence, and its consequences, has to be further investigated.
For instance, applications of techniques and results devised in the context of logic
programming, such as, for example, answer-set programming and negation-as-
failure, to the 8⇡0,D_ subfragment need to be studied. In view of our reduction,
a satisfiability checker for 8⇡0,D_ -formulae can be implemented by reusing some
machinery from logic programming, for example the Disjunctive Datalog system
DLV described in [1].7
We intend to develop analogous correspondences for other decidable frag-
ments of set-theory, such as, for instance, the quantified fragment 8⇡0,2 , whose
decision procedure presented in [2] is based on a reduction to 8⇡0 , and the un-
quantified fragment MLSS⇥ 2,m (see [4]), whose satisfiability problem can be in
turn reduced to the satisfiability problem for 8⇡0,2 .
References
1. Mario Alviano, Wolfgang Faber, Nicola Leone, Simona Perri, Gerald Pfeifer, and
Giorgio Terracina. The Disjunctive Datalog System DLV. In Oege de Moor, Georg
Gottlob, Tim Furche, and Andrew Jon Sellers, editors, Datalog Reloaded - First
International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010. Revised
Selected Papers, volume 6702 of Lecture Notes in Computer Science, pages 282–301.
Springer, 2011.
2. Domenico Cantone and Cristiano Longo. A decidable quantified fragment of set
theory with ordered pairs and some undecidable extensions. In Marco Faella and
Aniello Murano, editors, Proceedings of Third International Symposium on Games,
Automata, Logics and Formal Verification, volume 96 of EPTCS, pages 224–237,
2012.
3. Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo. A Decid-
able Quantified Fragment of Set Theory Involving Ordered Pairs with Applications
to Description Logics. In Marc Bezem, editor, CSL 2011, volume 12 of LIPIcs,
pages 129–143. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.
4. Domenico Cantone, Cristiano Longo, and Marianna Nicolosi Asmundo. A Decision
Procedure for a Two-sorted Extension of Multi-Level Syllogistic with the Cartesian
Product and Some Map Constructs. In Wolfgang Faber and Nicola Leone, editors,
CILC2010 : 25th Italian Conference on Computational Logic, 2010.
5. Domenico Cantone, Eugenio Omodeo, and Alberto Policriti. Set theory for comput-
ing: From decision procedures to declarative programming with sets. Monographs
in Computer Science. Springer-Verlag, New York, NY, USA, 2001.
7
http://www.dlvsystem.com/
176
D. Cantone et al. Herbrand-satisfiability of a Quantified Set-theoretical Fragment
6. Thomas Eiter, Georg Gottlob, and Heikki Mannila. Disjunctive Datalog. ACM
Trans. Database Syst., 22(3):364–418, 1997.
7. Melvin Fitting. First-order logic and automated theorem proving (2nd ed.).
Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1996.
8. Jacques Herbrand. Investigations in proof theory: The properties of true propo-
sitions. In Jean van Heijenoort, editor, From Frege to Gödel: A Source Book in
Mathematical Logic, 1879-1931, Source Books in the History of the Sciences, pages
525–581. Harvard University Press, 1967.
9. Ian Horrocks, Oliver Kutz, and Ulrike Sattler. The Even More Irresistible SROIQ.
In Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and
Reasoning (KR2006), pages 56–67. AAAI Press, 2006.
10. Yevgeny Kazakov. SRIQ and SROIQ are Harder than SHOIQ. In Franz Baader,
Carsten Lutz, and Boris Motik, editors, Proceedings of the 21st International Work-
shop on Description Logics (DL2008), Dresden, Germany, May 13-16, 2008, vol-
ume 353 of CEUR Workshop Proceedings. CEUR-WS.org, 2008.
11. Yiannis Moschovakis. Notes on Set Theory. Springer, second edition, 2005.
12. 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.
177