Alternative Translation Techniques for Propositional and First-Order Modal Logics.
We describe and analyze techniques, other than the standard relational/functional methods, for translating validity problems of modal logics into first-order languages. For propositional modal logics we summarize the &squ;-as-Pow method, a complete and automatic translation into a weak set theory, and then describe an alternative method, which we call i>algebraic, that achieves the same full generality of &squ;-as-Pow but is simpler and computationally more attractive. We also discuss the relationships between the two methods, showing that &squ;-as-Pow generalizes to the first-order case. For first-order modal logics, we describe two extensions, of different degrees of generality, of &squ;-as-Pow to logics of rigid designators and constant domains.
Introduction
Translation techniques have oered valuable aid for the study and development
of theorem provers for non-classical logics, and their nave
use can be ascribed to tradition. The rst systematic study of the relational
translation was carried out within Correspondence Theory (van
Benthem, 1983). In later years further studies of the relational and similar
techniques for computational purposes were initiated ((Ohlbach,
1991; Ohlbach, 1993; Nonnengart, 1993); see also (Ohlbach et al., 2001)
for a comprehensive survey). The eld has revealed itself to be fruitful
and interesting.
The relational translation of a modal
the rst-order formula RT('; x) (it has also been called ST , for \stan-
dard translation", but we will reserve this designation for \set-theoretic
inductively dened by
c
2001 Kluwer Academic Publishers. Printed in the Netherlands.
Alberto Policriti, and Matteo Slanina
Here, each propositional variable p i is mapped one-to-one to a unary
predicate symbol P i . Let RT(') be
If
axiomatizes a frame-complete logic, then
Here  f denotes validity of ' in the logic axiomatized by
, and
denotes classical (in this case second-order) validity. The second-order
quantiers in RT(') can be removed, since they are universal and appear
only as prex to the consequent of an implication. However, the
second-order character of RT(
is, in general, not eliminable, since,
in this case, the second-order (universal) quantication appears in the
antecedent of an implication. This makes the technique inapplicable for
computational purposes, since the target language is highly undecidable
(non-arithmetic, cf. (van Benthem, 1983)). Whenever RT(
can be
proved equivalent to a rst-order formula, the logic axiomatized by
is
said to be rst-order denable and the modal validity problem can be
solved by a rst-order theorem prover. Determining when RT(
a rst-order equivalent is the main topic of correspondence theory. In
some cases it can even be done automatically (e.g. Sahlqvist formulae,
the SCAN procedure (Gabbay and Ohlbach, 1992)). Unfortunately,
not all modal logics have a rst-order (frame) correspondent, and, even
when they do, there is no complete algorithm to nd one. A lot of work
has been done to avoid these di-culties, resulting in some extensions
of the class of tractable logics and, especially, in improved performance
(Nonnengart, 1993; Ohlbach, 1998). In particular, (Ohlbach,
1998) proposed a way to incorporate axioms and rules of Hilbert calculi
into relational translations, thus creating a hybrid system able to deal
with the axioms that cannot directly be captured by the translation.
A dierent perspective on the problem is taken in the approach
proposed in (D'Agostino et al., 1995), where the 2-as-Pow translation
was rst introduced. The novelty of 2-as-Pow lies in the fact that,
instead of determining which modal theories can be mapped into a rst-
order language, a fragment of second-order logic is used as a framework
for the translation. It turns out that the fragment required is very
small and can be specied as a weak rst-order axiomatic set theory.
Under this theory, the resulting translation is sound and complete for all
frame-complete (not only with respect to a rst-order class of frames)
Alternative Translation Techniques for Propositional and First-Order Modal Logics 3
logics. More specically, given a frame-complete logic with axiom
and
a formula ', the 2-as-Pow translation (
is such that
where
is the weak axiomatic set theory that will be dened in Section
2. Several extensions of this method were discussed in subsequent
papers (Montanari and Policriti, 1997a; Montanari and Policriti, 1997b;
van Benthem et al., 1998), including a variation (van Benthem et al.,
1997) that allows for completeness for any logic (not necessarily frame-
complete) and another with strong decidability results (D'Agostino
et al., 1996).
In this paper we systematically present set-theoretic and algebraic
translation techniques that are less restrictive than RT and its vari-
ations, and whose range includes propositional modal logics as well
as an important class of rst-order modal logics. After a short review
of the original 2-as-Pow translation (Section 2), we introduce
a new, very natural, translation method, that we call algebraic. This
algebraic translation, suggested by the algebraic semantics for modal
logics, achieves completeness for all logics in a simpler way than 2-
as-Pow. We point out strong relationships between 2-as-Pow and the
algebraic method, showing a new way to obtain the former from an
algebraic point of view (Section 3). We show that, in a certain sense to
be made precise later, 2-as-Pow and the algebraic translation coincide
at the propositional level. However, no such strong relationship holds
when we try to extend these methods to handle rst-order modal log-
ics: 2-as-Pow can be so extended, but for the algebraic method there
seems to be a signicant stumbling block (unless we allow the target
language of the translation to be second-order, which is unacceptable).
The relational translation and its derivations can be extended, in their
restricted setting, to rst-order modal logics in a fairly straightforward
manner. In Section 4, we collect and organize some results (Montanari
et al., 2000a; Montanari et al., 2000b) on the extension of 2-as-Pow
to the important class of rst-order modal logics of rigid designators
and constant domain, which is signicant given the aforementioned
observations. Section 5 contains some lengthy proofs that would have
broken the continuity of the exposition if put in the main text. We
conclude with some discussion on open problems and possible future
work.
We have tried to use a commonly understood symbolism. Some less
common notations are the ones for logical
syntactic derivation in classical and modal logic;
4 Angelo Montanari, Alberto Policriti, and Matteo Slanina
'Ks syntactic derivation in the modal calculus K s , that is, K
plus the Instantiation Rule;
truth in a model, semantic consequence in classical logic;
truth in a world or model, frame semantic consequence
in modal logic.
2. 2-as-Pow Translation (Propositional Case)
The 2-as-Pow translation, at the propositional level, can be described
as an extension to the 2 operator of the set-theoretic interpretation
of the propositional connectives ^, _, and :. The approach brie
y
described here was rst presented in (D'Agostino et al., 1995) and
subsequently developed in (van Benthem et al., 1997) and (van Benthem
et al., 1998). The key idea is simply to replace the accessibility
relation R of the possible world semantics by the membership relation
2. Accordingly, a world y accessible from x becomes an element of
x, and taking a further step from y via R amounts to moving into y
to inspect one of its elements. This viewpoint allows us to identify a
frame F with its support w. Moreover, since we clearly want all worlds y
accessible from a given world x in a frame w to be themselves elements
of w, it is natural to require that w be a transitive set: w  P(w).
Valuations for propositional variables, i.e. sets of worlds, can now be
identied with worlds themselves. 2-as-Pow is designed in such a way
that the translation '  of a compound formula ' turns out to be the
set
of all worlds where ' is true.
For propositional connectives we simply follow the Boolean tradition
and say that
In order to complete the denition it is su-cient to calculate the Kripke
semantics of the 2 operator replacing R by 2:
which is to say: 2' holds true at x if and only if x is a subset of '  .
This allows us to complete our denition by putting
Alternative Translation Techniques for Propositional and First-Order Modal Logics 5
It is possible to show that the
collection
of the following set-theoretic
principles su-ces for proving the soundness and completeness
of the translation:
z
Dening Trans(w) as w  P(w) it can be shown that
When a modal logic is characterized by a nite collection of Hilbert
axioms, whose conjunction is
, these results generalize to
where
Axiom
(w) stands for 8~x (w
), where ~x is the list of all the variables
in
distinct from w.
Thus when  is frame-complete an exact correspondence between
modal and set-theoretic derivability is guaranteed
It turns out that the
theory
is almost minimal in providing a
formal counterpart to the idea underlying the 2-as-Pow translation.
Let us call MM (an acronym for \Minimal Modal") the theory whose
axioms result from those
of
by replacing x 2 P(y) $ x  y with the
following two theorems of
1 As a technical note, if we were to deal with a logic with an innite axiom set
, we could reformulate the result as follows (use skolemization on w/c and the
Deduction Theorem for rst-order logic to obtain the equivalence):
6 Angelo Montanari, Alberto Policriti, and Matteo Slanina
where u \ v is an abbreviation for u n (u n v). Although MM is even
weaker
than
it can still drive the 2-as-Pow translation. A further
possible simplication would be to eliminate the binary union symbol,
observing that, by exploiting complementation, it can be dened in
terms of set dierence.
Theorem 1 (Completeness of 2-as-Pow). If
'Ks ', then MM
Theorem 2 (Soundness of 2-as-Pow).
If
'.
3. Algebraic Translation (Propositional Case)
The same mental shift that proceeds from relational semantics to the
relational translation enables one to discover the algebraic translation
as a straightforward rewriting of algebraic semantics in syntactic terms.
The basic objects playing the role of Kripke frames are Boolean algebras
with one extra operator (Bull and Segerberg, 1984; Blackburn et al.,
2001).
Denition 3. Consider the rst-order language of Boolean algebras
(with meet u, join t, complementation 0 , bottom element 0, and top
element 1) and an additional operator ' . Dene the theory MA (for
Modal Algebra) to be the rst-order theory of Boolean algebras with
the two additional axioms:
Denition 4. Let us map each propositional symbol p to a distinct
individual variable x p of the target rst-order language and dene
the algebraic translation ' # of a modal formula ' by the following
structural induction:
Alternative Translation Techniques for Propositional and First-Order Modal Logics 7
Based on this denition and following the truth denition of algebraic
semantics, we put
It is straightforward to prove that this translation is sound and complete
for all (nitely axiomatizable) modal logics, since the algebraic
semantics is complete for all logics (in fact, it is equivalent to the general
frame semantics).
Theorem 5. Given a modal logic with axiom
and a formula ',
The algebraic translation converts a validity problem in any modal
logic to a validity problem of rst-order logic, thus permitting the use
of any rst-order theorem prover. As a validity checking method, this
is slower than the use of the relational or functional translation, when
the latter is applicable, but it has the advantage of being a completely
syntactic method and it can turn out to be extremely useful for experimenting
with new logics. 2 A further advantage of this technique
is that it also works, with no modication, for multi-modal logics:
just introduce one ' operator for each of the modalities involved and
augment the underlying theory with a pair of axioms, of the form of (1),
for each of them.
What we are left with after the algebraic translation is a deduction
problem in equational rst-order logic. Tools that deal with such prob-
lems, such as EQP, are available and can be used for modal theorem
proving based on the algebraic translation. Equational problems can be
solved particularly e-ciently when rewriting techniques can be applied.
In the case of modal logic, Foret (Foret, 1992) discovered con
uent
(modulo associativity and commutativity of the Boolean operators)
and terminating rewriting systems for the logics K, D, T, and S5. The
rewriting systems are oriented versions of the equational axioms of
modal algebras and can be seen as a specialized solver for the algebraic
translation of the formulae. For example, Foret's system for K adds the
oriented versions of (1) to Hsiang's system for propositional logic|
an oriented version of the equational theory of Boolean rings with
multiplicative identity (Hsiang, 1982; Hsiang, 1985):
We did some simple experimentation with a raw algebraic translation given to
EQP (McCune, 1997), and were able to prove 31 out of the 72 problems of (Gore
et al., 1997) in seconds (at most a few minutes in a few cases) on a Pentium class
computer.
8 Angelo Montanari, Alberto Policriti, and Matteo Slanina
3.1. Relations with 2-as-Pow.
If one looks at the original formulation of the 2-as-Pow translation,
there is one peculiar feature: the membership symbol 2 does not appear
explicitly. In fact, the translation seems to be expressed in an almost
equational language and looks very much like the algebraic translation.
Moreover, the axioms of MM are strikingly similar to those of modal
algebras.
We will now prove that these remarks have indeed a deep under-
pinning: there is an equational theory of sets, capturing the Boolean
properties
of
and MM , that proves the propositional 2-as-Pow translation
sound and complete. In other words, at the propositional level,
the algebraic and the 2-as-Pow translation are essentially equivalent.
However, as will be shown in the next section, there is no simple way
to lift this equivalence to the rst-order level.
One would be inclined to use, as an equational set theory, a theory
of Boolean algebras. However, we cannot hope to have a complementation
function, since there is no constant for a top element. Hence, we
add a relativized complementation which mimics the behavior of set
dierence. This turns out to be all we need and the following axioms
are su-cient.
Denition 6. We dene the
theory
by the
universal closure of the following axioms:
Intuitively, the rst ten axioms describe a theory of \Boolean algebras
without maximum element". It can be shown that the models of
these axioms are such that the cone of elements below any given element
is a Boolean algebra. This kind of structure is exactly a Boolean ring
in the sense of, e.g., (Jacobson, 1951), that is, an idempotent ring with
no multiplicative null element. This allows us to establish a two-way
correspondence between models
of
and models of MA. Using this
correspondence and the 2-as-Pow translation, which can be applied
directly to the language
of
, we can prove the following equivalence:
Alternative Translation Techniques for Propositional and First-Order Modal Logics 9
Theorem 7. Consider a nitely axiomatizable modal logic, with axiom
, and a modal
Proof. See Section 5.
Corollary 8. If
axiomatizes a frame-complete modal logic, then
Proof.
'Ks ' by soundness and completeness of 2-
as-Pow. By soundness and completeness of the algebraic translation
(Theorem 5),
To conclude apply Theorem 7.
4. 2-as-Pow Translation (First-Order Case)
The analogy between the 2-as-Pow and the algebraic translation does
not lift from the propositional to the rst-order level. An extension
of the algebraic method to rst-order modal logics would necessitate
employing a theory of complete Boolean algebras, which is second-
order, therefore leading again to problems of the same sort as those
mentioned in Section 1. However, we have successfully extended 2-
as-Pow to an important class of rst-order modal logics maintaining
the target language of the translation at the rst-order level. Hence,
2-as-Pow and the semantics it is based on can be seen as genuine generalizations
of the algebraic models; only at the lowest (propositional)
level do the two happen to be equivalent.
Here we describe two extensions of the 2-as-Pow translation method
to the class of rst-order modal logics with rigid designators and xed
domains, known as Q1 systems (see (Garson, 1984; Fitting, 1993; Fitting
and Mendelsohn, 1998)). Informally, the language of such logics is
a rst-order language together with a 2 modality. A model M consists
of a frame hW; Ri (possibly with restrictions dened by an underlying
propositional modal logic) plus a rst-order logic interpretation with
a single domain D, an interpretation FC for constants and one F F
for function symbols, and|the only part that varies with worlds|the
interpretation F P of predicate symbols:
There is a sound and complete calculus for any such logic, obtained
by adding to the propositional calculus for the underlying modal logic
Alberto Policriti, and Matteo Slanina
the axioms and rules of rst-order logic|the Universal Quantier Axiom
schema and the Universal Generalization Rule|and the Barcan
for every formula '(x).
Both translations will be targeted to a two-sorted rst-order logic.
This is done essentially for better understanding and ease of implemen-
tation: in principle everything could be done in a one-sorted language
(see (Slanina, 2001) for details; for a general discussion of the reducibility
of many-sorted to one-sorted logic see also (Davis, 1993)). If L is the
rst-order modal language, we dene L 0 to be a two-sorted language
where the sort term denotes L-terms and the sort set denotes objects
of the translation (possible worlds and sets thereof). The underlying
theory
is modied accordingly, with the third axiom now becoming
8x8y
We call this modied
theory
.
The rst translation (Montanari et al., 2000a) works for the fragment
of the Q1 language where modal operators cannot appear in the
scope of quantiers (below: \locally quantied formulae"). This case
appears often in practice and can be treated using the observation
that sentences can be decomposed into two disjoint parts: one rst-
order, but classical, and the other modal, but propositional. 3 More
precisely, a sentence of this fragment can be written as
are classical rst-order sentences and the
formula we obtain by replacing each ' i by a propositional variable p i ,
for short), is a propositional modal
formula. The simple, but crucial, observation at this point is that
derivability can be split accordingly, as stated in the following lemma.
Lemma 9. There is a nite set  of classical propositional formulae
(over the variables
'g for all  2 ,
and, for all ,
Proof (sketch). Clearly,
3 This is the case, for instance, of Manna and Pnueli's temporal frame-work
(Manna and Pnueli, 1995), where most specications can be conned to this
restricted form of quantication.
Alternative Translation Techniques for Propositional and First-Order Modal Logics 11
Let  be the set of propositional formulae on that are valid
under the substitution fp 1 7! ' g. Then, it is easy to see
that the right-hand side of (2) is equivalent to   (p
nite modulo logical equivalence.
Using the above results, the translation is dened as follows.
Denition 10. As an auxiliary notation, we introduce a transformation
that adds an extra variable (representing a world in a Kripke
frame) to the arguments of each predicate symbol ( ~ t are terms):
Now x a variable w of sort set. The translation (
of a locally
quantied respect to the logic
axiomatized by
, is expressed as follows:
where
Here Axiom 2
(w) and  are the same as in the propositional case, with
all bound variables of sort set.
The adequateness theorems are similar to the ones for the propositional
case:
Theorem 11 (Completeness).
Theorem 12
(Soundness).
Q1 F .
The proofs of these theorems can be found in (Montanari et al.,
2000a). We omit them here, since our next translation is stronger.
The second translation works for the full Q1 language and is developed
along a dierent line.
Alberto Policriti, and Matteo Slanina
Denition 13. The set-theoretic translation (
with respect to the logic with axiom
(a propositional modal
is the formula
Trans(w) and Axiom
(w) are the same as in the propositional case,
while  ' (w) encodes the semantics of quantiers. The notation is as
follows: variables occurring|free or not|in ' are denoted by ~x, which
stands for x are fresh function symbols f for some subformulae
of ' (to be specied below), with signature set term
set. Each term t , with subformula of ', represents the set of worlds
where is true, in the frame w and under variable assignment ~x.
Formally, let be a superset of the set of the variables
appearing in '. Then
are
the free variables in ', with
2.
' (w) is simply the conjunction, over all subformulae   of ', of the
formulae  (w), where  is dened as
(w) => > > > <
if is 8x i  and x
are the free variables in
, with
otherwise.
In analogy to the propositional case, we now have the following
theorems, whose proofs are given in Section 5.
Theorem 14 (Completeness).
Theorem 15
(Soundness).
Example. Let ' be the formula
The superscripts mark the main operator of each of the eight subformulae
of '. Let
be the axiom of seriality,
Alternative Translation Techniques for Propositional and First-Order Modal Logics 13
some freedom of notation (e.g., we use 9 , whose direct translation is
obtained patching the one for 8 in the obvious way), the translation is
the following:
Axiom
5. Proofs
5.1. Proof of Theorem 7.
We only give a sketch of the proof. The interested reader is referred
to (Slanina, 2001) for the details.
\Only if". The proof is by contradiction: assume
that
i.e., by completeness of rst-order
logic,
. This means there
exists a model A
of
E and an assignment  on A such that, putting
a  A P A (a) ;
Let B be the model for MA dened in the obvious way taking as
domain the lower cone of A with supremum a (see (Slanina, 2001) for
details). Each term t in the language
of
E such that any occurrence of
n has w as its left argument can be mapped to a term t 0 in the language
of MA, and the assignment  can be mapped into the assignment  0
on B dened by  0 in such a way that
and
14 Angelo Montanari, Alberto Policriti, and Matteo Slanina
It is then straightforward to prove that B 6 (
\If". The argument is analogous to the \only if" case, proceeding
by contradiction from a model A of MA such that A  ~ 8(
building a model B
of
E such that B 6 (
5.2. Proof of Theorem 14.
We need a preliminary lemma, whose omitted proof directly follows
from Denition 13.
Lemma 16. If there is no free occurrence of x i in ', then there is no
occurrence of x i in t ' (w; ~x).
The proof of the theorem is by induction on the derivation of '.
Propositional Axioms. The proof is exactly the same as the one for
the propositional 2-as-Pow translation (cf. (D'Agostino et al., 1995)).
Universal Quantier Axioms. Let us assume, without loss of gener-
ality, that we are instanciating the variable x 1 and that the other free
variables in
where the substitution fx 1 7! sg is free for x 1 in (x 1 ). Let  be
and
Assume  ' (w) (Trans(w) and Axiom
(w) are not needed in the
proof). We shall prove that w  t ' (w; ~x) by showing that, whenever
From Def. 13, we have that t
that is, taking
the negation out of the quantier,
with  ' (w) (the   (w) conjunct), this implies y 62 f  (w; x
Modus Ponens and Necessitation Rule. Both proofs are basically the
same as those for the propositional case. Refer, again, to (D'Agostino
et al., 1995).
Alternative Translation Techniques for Propositional and First-Order Modal Logics 15
Universal Generalization Rule. Assume the same notation as with the
Universal Quantier Axiom schema. The rule has then the form
does not occur free in '. Let  be the subformula 8x 1 . From
Def. 13, we get
Assume  '!8x 1 (w) (Trans(w) and Axiom
(w) are not needed in
the proof). We shall prove that w  t '!8x 1 (w; ~x) by showing that,
necessarily y 2 f  (w; x
Assume y 2 w and y 2 t ' (w; ~x). By induction hypothesis, w  (w n
contains no occurrence of x 1 ; hence, we can apply classical
Universal Generalization to conclude that
thus, from the conjunct   (w) of the assumption  '!8x 1 (w), that
Barcan Formulae. Let us call
and  the formulae 8x 1 2 respectively, and let
xm be the free variables in  (or, equivalently, in ). Then
Assume  ' (w) and y 2 w. Then
_ 8z: set (z 2 y
_ 8z: set (z 2 y
Alberto Policriti, and Matteo Slanina
The rst equivalence is just the unfolding of the denition of t ' (w; ~x) by
the axioms
of
2 . In the second we dropped the subformula y 2 w from
the conjunct because it is true by assumption, and then we rewrote the
rst disjunct using   (w) and the second using
the
In
the last, we used the denition of  in the left disjunct and   (w) in
the right one.
Now, to show that w  t ' (w; ~x), we take, as above, y 2 w and assume
that the second disjunct of the last line is false, which is equivalent
to
This obviously implies the rst disjunct, thus proving the claim.
5.3. Proof of Theorem 15.
The proof is an adaptation of the technique introduced in the soundness
proof of the propositional case in (D'Agostino et al., 1995). More pre-
cisely, we are going to follow the proof of Theorem 5 of that paper. The
rst part is almost the same and we will state some lemmas without
proof.
Let U be a universe of hypersets satisfying all the axioms of ZF FA
(ZF except the Foundation Axiom) and AFA (see (Aczel, 1988) for
details).
Lemma 17. Let  be an ordinal, V  be the set of all well-founded sets
of rank less than , and U n V  be the universe of all hypersets not
belonging to V  . Then any model for the language
of
2 with domain
set and interpretation function () 0 satisfying
is a model
of
.
Proof. See Lemma 6 of (D'Agostino et al., 1995).
Given a frame (W; R; D), we want to embed it into the universe
suitable . In (D'Agostino et al., 1995), the authors
prove the existence of a labeled decoration  such that the following
lemma holds.
Alternative Translation Techniques for Propositional and First-Order Modal Logics 17
Lemma 18. For each a; b 2 W ,
1. a
2. a  62 V +1 and a  n V aRbg.
Proof. See (ii) and (iii) in Lemma 7 of (D'Agostino et al., 1995).
Now consider an interpretation
an assignment  : f~xg ! D. Moreover, let M be the Q1 model
A model for the language
of
2 can be obtained as follows. First,
take the interpretation for set symbols as dened by the previous
lemmas and let D be the domain for the sort term. Then, interpret
term constant and function symbols as in FC and F F , respectively,
and, for each k-ary relational symbol Q, let f
be equal to
if this set is not empty, and to V +1 otherwise.
Finally, for each universally quantied formula
variables x j 1
be equal to
if this set is not empty, and to V +1 otherwise.
We call this model AM . Furthermore, let W  be equal to fa  j
a 2 Wg. W  62 V +1 because V +1 is transitive and, for each a 2 W ,
a  62 V +1 (Lemma 18).
Lemma 19. We have:
1. for each a 2 W , d
if and only if
a
2. AM   ' (W  ).
Proof. 1. Let The proof is by induction on '.
immediate from the denition of f
induction hypothesis) a
d) or a  2 0 t
d) ,
(for AM is a model
of
d)
d) , (by
denition of t ' ) a  2 0 t
d).
Alberto Policriti, and Matteo Slanina
d)
, (for a  2 0 W  ) a  2 0 W  and a  62 0 t
d) , (for AM
is a model
of
d) , (by denition of t ' )
a
d).
aRb , (by i.h.) for every b 2 W such that aRb, b  2 0 t
d)
d) , (by denition of
(by denition of t ' )
a
d).
immediate from the denitions of f
' and t ' .
2. Assume, without loss of generality, that
be the free variables in '. We are going to prove  ' (W  ). Let
a 2 W and d be arbitrary elements of D. Then a  2 0
f
(by denition of f
' , for every d 1 2 D, a; [x 1 =d (for the
rst part of this lemma) for every d 1 2 D, a
Corollary 20.
if and only if
Proof. Follows directly from Lemma 19 recalling that M Q1 L '
means that M Q1 L 8~x '.
Lemma 21. A modal propositional formula
, over the propositional
variables is valid in the frame (W; R) if and only if, for the
corresponding hyperset W  ,
holds in U n V +1 .
Proof. See Lemma 9 of (D'Agostino et al., 1995).
To conclude the proof of Theorem 15, let us suppose that
4 By Lemma 16, all the d's beyond the m-th do not count in the interpretation.
Alternative Translation Techniques for Propositional and First-Order Modal Logics 19
be a model based on a frame in which
is valid (a Q1-L model). From Lemma 21 it follows that Axiom 2
is true in AM , and from the second part of Lemma 19 the same follows
for  ' (W ). Furthermore, it is easy to prove that Trans(W  ) holds
as well. Since AM is a model
of
and, by hypothesis, the formula
8~x: term W   0 t
is true in AM , it follows from Corollary 20
that M Q1 L '.
6. Conclusions and Open Questions
All the results presented in this paper uniformly rewrite the deduction
problem for various families of modal logics into deduction problems
with some form of set-theoretic
avor. The main contributions are the
proposal of an equational theory capable of driving the translation at
the propositional level and the extension of the 2-as-Pow translation
technique to a signicant class of rst-order modal logics.
A systematic study of set-theoretic translation techniques for different
kinds of rst-order modal logics could be carried out starting
from the ideas presented here. In this paper, we deliberately conned
ourselves to one of the most signicant classes. Moreover, we did not
consider the extension of the algebraic method to the rst-order case:
although we did not see any particular obstacle in principle, its development
would almost certainly have called for the introduction of
a very ad-hoc (two-sorted, non-equational) extension of the theory of
Boolean rings, thus stripping the method of its elegance (which was the
main motivation for its use in the propositional case).
All of the results mentioned call for specialized techniques explicitly
designed for deduction in such theories
as
or, better yet, able
to exploit the syntactic features of the formulae obtained from the
translation. Preliminary work in this direction is presented in (Piazza
and Policriti, 2000), where a tableaux-based decision procedure for a
class of formulae in which the resulting formulae can be embedded is
presented. Other related results can be found in (Cantone and Zarba,
2000; Cantone et al., 2001).
A further step toward the applicability of the results presented could
be obtained via a higher level of integration of the set-theoretic translation
with more classical techniques. For example, it would be interesting
to study the possibility of separating the rst-order denable portions
of a logic (for which more e-cient techniques are often available) from
contexts in which the 2-as-Pow is the only available translation. In this
context, we mention as an open problem, the question of precisely char-
20 Angelo Montanari, Alberto Policriti, and Matteo Slanina
acterizing the expressive power of locally quantied rst-order modal
logics (cf. Lemma 9).
Finally, another research task, related to the quest for specialized
techniques designed to be coupled with the translations presented here,
is the search for reduction orders and rewriting systems to be used in
automated engines for testing derivability in the
theory
introduced
in Section 3.

Acknowledgments

We wish to thank prof. Martin Davis for a careful proof-reading of the
nal draft of this paper.



--R


Modal Logic and Classical Logic.


Modal Logic

Set Theory for Computing.
From Decision Procedures to Declarative Programming with Sets








Handbook of Philosophical Logic






Journal of Arti
Lectures in Abstract Algebra
Temporal Veri
'EQP 0.9c User's Guide'.






Journal of Logic and Computation 1(5)

Bulletin of the IGPL 1(1)





Technical Report 07/01
--TR
first-order modal logics;computable set theories;translation methods