In the last decades, several fragments of set theory have been studied in the context of the so-called Computable Set Theory. In general, 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 Neumann standard cumulative hierarchy of sets, i.e., the class consisting of all the pure sets. Because of this, theoretical results and various machinery 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 decision procedure to reduce the satisfiability problem for the fragment 8 ⇡0 to the problem of Herbrand satisfiability for a first-order language extending it. In addition, it turns out that such reduction maps formulae of the Disjunctive Datalog subset of 8 ⇡0 into Disjunctive Datalog programs.
The quantified fragment of set-theory 8 ⇡0 (see [
In general, the semantics of set-theoretical languages (see [
V0 = ; V +1 = P(V ) , for each ordinal
V = Sµ< Vµ , for each limit ordinal
V = S 2 On 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 theoretical results and machinery developed in the context of first-order logic for settheoretical matters is not straightforward.
In this paper we show that these diculties 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. [
It turns out that these formulae ' can be considered as DATALOG_ ,¬ programs. 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 [
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 ecient reasoning and query engine for the very expressive representation language DLh8 ⇡0 i; on the other hand, it allows 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 Disjunctive 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 denumerably 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
(8 x1) . . . (8 xn) , 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 (8 x1) . . . (8 xn) by (8 x1, . . . , 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 (8 x1, . . . , 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 (8 x). 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 quantifiers can easily be expressed by universally quantified prenex formulae, by way of the following equivalence: (8 x1, . . . , xn|P (x1, . . . , xm)) ⌘ (8 x1, . . . , 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 (8 x). 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 26 ⌃ .
First-order interpretations, whose universe is Consts and such that each constant 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 Herbrand 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 conjunctions of universally quantified prenex sentences, as stated in the following theorem.
Theorem 1. Let ' be a finite conjunction of universally quantified prenex sentences. 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. tu
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. 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 (8 x1) . . . (8 xn)(' ! ) , where ' (the rule body ) is a conjunction of literals, (the rule head ) is a disjunction 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 embedded in DATALOG_ ,¬ rules and formulae. Indeed, let us consider a closed formula of the form (8 x1, . . . , 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 remarked above, (1) is equivalent to the closed formula which, in its turn, is equivalent to the closed formula (8 x1, . . . , xn)(P (x1, . . . , xm) ! (' ! (8 x1, . . . , xn)((P (x1, . . . , xm) ^ ' ) ! )), ).
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 [
⌫ 2 ⇡¯(µ), [⌫, ⌫ 0] 2 µ, ⌫ = µ 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 µ expresses 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: (8 x1 2 ⇡¯(a1)) . . . (8 xn 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 (2) (3) closed simple-prenex 8 ⇡0 -formulae. The collection of the domain constants of a 8 ⇡0 formula ' , which we denote with ConstsD(' ), consists of the domain constants of all of its conjuncts.
Semantics of the language 8 ⇡0 is based on the von Neumann standard cumulative 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, v0) | u0 2 u ^ v0 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, v0 2 V : 1. ⇡ (u, v) = ⇡ (u0, v0) () 2. u ⇥ (⇡ ) v is a set in V.
u = u0 ^ v = v0,
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; – I⇡¯(x) = {u 2 Ix | (8 v1, v2)(I[v1, v2] 6= u)}, for all x 2 Vars [ Consts.
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 settheoretical 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 [
The definition of skeletal representation adopted in this paper di↵ers slightly
from the one presented in [
In the following definition, we shall make use of the membership closure relation 2 S+ of a set S of atomic 8 ⇡0 -formulae. This is the minimal transitive relation on Consts(S) such that, for a, b, c 2 Consts(S), we have + b, and –– iiff SS ||== [aa2, b]⇡¯2 (b)c tthheenn aa 22 SS+ c and b 2 S+ 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 . tu
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 [
⇡ 0(u, v) = Def {u, {u, v}} ⇡ n+1(u, v) = Def {⇡ n(u, v)} , for u, v 2 V .
Definition 2 (Realization [
R x = Def {R y | S |= y 2 ⇡¯(x)} [ {R [y, z] | S |= [y, z] 2 x} R ti = Def {R y | S |= y 2 ⇡¯(ti)} [ {R [y, z] | S |= [y, z] 2 ti} [
{{k + 1, k, i}} ,
where h = |V | + |T | and k = |V | · (|V | + |T | + 3).5
for all u, v 2 V
for x 2 V
for ti 2 T
tu
5 We are assuming that integers are represented a` la von Neumann, namely 0 =Def ;
and, recursively, n + 1 =Def n [ { n}.
The following lemma is a direct consequence of Definition 2 and of Lemma 2 in
[
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; – R a 2 R ⇡¯(b) i↵ S |= a 2 ⇡¯(b); – R [a, b] 2 R c i↵ S |= [a, b] 2 c. tu
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 [
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 ' . tu
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 realization 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 (8 x1 2 ⇡¯(a1)) . . . (8 xn 2 ⇡¯(an))(8 [y1, z1] 2 b1) . . . (8 [ym, zm] 2 bm) , (4) such that has the form 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.
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 2b, P =, P ⇡¯ , dist, dist⇡
ternary P [,], distBy 4-ary distBy⇡
Next, we define a polynomial-time reduction ' 7! ' from 8 ⇡0 -formulae into L⇡0 -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 2b will be used to model the transitive closure 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 distinguished 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 settheoretic 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 interpretation 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 representation relative to (V, T ), and – 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 ) = Def 1 ^ 2 ^ (V,T ) 3 ^ (V,T ), 4 where 1 = Def (8 x, y)(x 2 ⇡¯(y) ! x2by) ^ (8 x, y)([x, y] 2 z ! x2bz) ^ (8 x, y)([x, y] 2 z ! y2bz) ^ (8 x, y, z)(x2by ^ y2bz ! x2bz) ^ (8 x)¬(x2bx) ^ (8 x, y) dist⇡ (x, y) ! W
z,v2 V [ T ^ (8 x, y, z) distBy(x, y, z) ! (z 2 ⇡¯(x) ^ ¬ (z 2 ⇡¯(y))) ^ (8 x, y, z, v) distBy⇡ (x, y, z, v) ! ([z, v] 2 x ^ ¬ ([z, v] 2 y)) distBy⇡ (x, y, z, v) _ distBy⇡ (y, x, z, v) ! (V,T ) = Def 4
V x2 V [ T,t2 T,x6=t
¬(x = t).
It can be easily verified that (V,T ) is a DATALOG_ ,¬-formula. The subformulae 1, 2, (3V,T ), and (4V,T ) formalize the conditions (S1), (S2), (S3), and (S4) of Definition 1, as clarified by the following lemma. 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 (2bVH,T )=.H{e[nac,eb], |2 HS+ |=muas2bt bb}eisacayccylicclica,s awseHll, models correctly the conjunct 1 of as required by Condition (S1), since 2 S+✓ 2bH.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 (8 x, y, z)(x 2 ⇡¯(y) ^ x = z ! z 2 ⇡¯(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 that H is a model for (3V,T ). 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 z 2 ⇡¯(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 must model the conjunct ¬(x = y) of (4V,T ). 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 (8 x)(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 . tu
In addition, every skeletal interpretation can be extended to comply with the constraints imposed by (V,T ). 6 The relation 2 +H does not necessarily coincide with 2bH, as the minimality of 2bH is not enforced in 1. Lemma 3. Given two disjoint sets of constants V ,T and a skeletal representation 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 ⇡¯(y) is in S, we add x2by to H. Likewise, if [x, y] 2 z is in S, we add the atoms x2bz and y2bz to H. Then we close transitively H with respect to the 2b-atoms, i.e., for each sequence of atoms in H of the form x12bx2, x22bx3, . . . , xn 12bxn , we add the atom x12bxn 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 distinguished 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 and (4V,T ).
By the very construction process, H satisfies the first four conjuncts of 1. In addition, H satisfies also the last conjunct (8 x)¬(x2bx) of 1. Indeed, if this were not the case, H would contain an atom of the form z2bz, 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
z 2 ⇡¯(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
z2bx1, x12bx2, . . . , xn 12bxn, xn2bz , with xi 2 V [ T for 1 i n.
However, case (a) cannot occur, since, by condition (S1), the membership relation induced by S is acyclic. We show that also case (b) cannot occur, thereby proving that H cannot contain any atom of the form z2bz. Indeed, if (b) were true, then H would contain a maximal sequence of atoms of the form x02bx1, x12bx2, . . . , xn 12bxn, xn2bxn+1 , 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.
To show that H satisfies 2 and (3V,T ), 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 satisfies also the formula (4V,T ), 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 ). tu As already remarked, the following lemma exploits a semantical correspondence 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 ConstsD(' ) ✓ 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 ' = (8 x 2 ⇡¯(a)) , for some x 2 Vars and a 2 Consts, where is a simple-prenex 8 ⇡0 -formula with one less quantifier than ' . Since R is a realization, we plainly have R ⇡¯(a) = {R b | H |= b 2 ⇡¯(a)}, so that R models correctly (8 x 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 constants b such that H |= b 2 ⇡¯(a), we have ConstsD( [x ! b]) = ConstsD( ) = ConstsD(' ) \ {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], for each b such that H |= b 2 ⇡¯(a), and, consequently,
R |=s (8 x 2 ⇡¯(a))
() H | = (8 x 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 quantifier 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 tu
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 realization 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 ' . tu
We conclude this section by observing that, if ' is a 8 ⇡0,D_ -formula, then (V,T ) ^ ' is a DATALOG_ ,¬-formula, as (V,T ) is a DATALOG_ ,¬-formula. Thus 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 settheoretically satisfiable if and only if the corresponding DATALOG_ ,¬-formula (V,T ) ^ ' is satisfiable, in the sense of Disjunctive Datalog. tu
Conclusions and Future Works In this paper we have identified a correspondence between the fragment of settheory 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-asfailure, 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 [
We intend to develop analogous correspondences for other decidable
fragments of set-theory, such as, for instance, the quantified fragment 8 ⇡0,2, whose
decision procedure presented in [