A Set-Theoretic Approach to Automated Deduction in Graded Modal Logics

1 Introduction

The general theme of this paper is the description of a novel approach to the problem of supporting the automa­ tion of reasoning in a family of knowledge representation formalisms. Such a family is characterized by the fact that its members need to represent and reason about finite quantities, and it includes terminological logics, epistemic logics, universal modalities. van der Hoek and de Rijke have shown that all these languages can be rep­ resented using graded modalities [Fattorosi-Barnaba and DeCaro, 1985] (cf. [Hoek and de Rijke, 1995] for a com­ plete description of this kind of reductions). In this pa­ per, we propose an approach to automated deduction in graded modal logics which is based on a set-theoretic translation method introduced by D'Agostino et al. in [D'Agostino eta/. , 1995] to support derivability in propo­ sitional modal logic.

Most inference systems for modal logic are defined in the style of sequent or tableaux calculi, e.g. [Fitting, 1983; Wansing, 1994] . As an alternative, a number of translation methods for modal logic into classical first­ order logic have been proposed in the literature (for a comprehensive survey, cf. [Ohlbach, 1993]) . Such meth­ ods allow the use of Predicate Calculus mechanical theo­ rem provers to implement modal theorem provers. Com­ pared with the direct approach of finding a proof algorithm for a specific class of modal logics , the transla­ tion methods have the advantage of being independent of the particular modal logic under consideration: a single theorem prover may be used for any translatable modal logic.

In the standard approach, the first-order language C into which the translation is carried out contains a con­ stant r denoting the initial world in the frame, a bi­ nary relation R(x, y) denoting the accessibility relation, and a denumerable number of unary predicates Pi ( x) . The translation function 1r is defined by induction on the structural complexity of the modal formula as follows :

• 1r(Pj,x) =: Pj(x);
• 1r(-, x) commutes with the boolean connectives;
• 1r(DTJ>,x) =: Vy(xRy--+ 1r(1/> ,y)) .

Efficiency concerns have motivated further investiga­ tions on the above (relational) translation method. Such studies (e.g. [Ohlbach , 1991]) suggested a "functional" semantics for modal logic and resulted in a family of more efficient and general translation methods. From the computational point of view, the functional trans­ lation may still cause some problem when using a first­ order theorem prover, due to the presence of equalities in the translation of the axioms. A method for limiting the complexity induced by the introduction of equality using a mixed relational/functional translation is proposed in [Nonnengart, 1993] .

A common feature of all the methods mentioned above is that, in order to be applied directly, the un­ derlying modal logic must have a first-order seman­ tics. All attempts to apply them to logics not hav­ ing a first-order semantics have required ad-hoc tech­ niques. Moreover, if the logic has a first-order seman­ tics, but it is only specified by Hilbert axioms, a pre­ liminary step is necessary to find the corresponding first-order axioms. The question of automatically solv­ ing this last problem has been extensively studied and algorithms have been proposed, e.g. [Benthem, 1985; Gabbay and Ohlbach, 1992].

The above analysis can be easily tailored to the case of graded modalities . The semantics of graded modali­ ties is very natural and intuitive, but it has a disadvantage: the inference systems based on it deal with On and On operators by generating a number of terms that, in general, can be very large. This problem can be over­ come by using a Hilbert-style axiomatic system, which allows one to perform arithmetic symbolic reasoning; in such a case, however , the search space for proving even very simple theorems can grow very much and it is usu­ ally rather unstructured. In view of the previous points, a translational approach to automated reasoning with graded modalities has been considered by Ohlbach et al. (cf. [Ohlbach et a/., 1995]) . Such an approach provides the possibility of using a standard deductive system - thereby guaranteeing symbolic reasoning - for which optimizations and good implementations are available.

In this paper , we exploit an alternative translation method whose basic idea is to map modal formulae into set-theoretic terms. Such a method works for all normal complete finitely axiomatizable modal logics, regardless of the first-order axiomatizability of their semantics. It also works if the modal logic under consideration is only specified by Hilbert axioms . Furthermore, it can be eas­ ily generalized to polymodal logics with finitely many modalities [D'Agostino et a/., 1995].

Even though graded modal logics can be seen as poly­ modal logics ([Ohlbach et a/., 1995]), the set-theoretic translation method cannot be applied directly, because the number of modalities involved in their translation is infinite. In the following, we show how to adapt the set­ theoretic translation for polymodal logics with finitely many modalities to encompass an infinite number of ac­ cessibility relations (each one corresponding to a differ­ ent "grade") . As a matter of fact, graded modal logics are treated as a special case of a more general technique able to deal with polymodal logics with infinitely many modalities .

2 Graded modal logics

Graded modal logics have been introduced in the 60's by Goble [Goble, 1970], who proposed a logic with a fixed number of modalities, each one associated with a natural number and representing a different degree of necessity. As an example, the formula Nnt.p 1\ Nmt/J, with m > n , espresses the fact that both <p and t/J are necessary, but t/J is more necessary than t.p. This approach has been later generalized by Fine ( cf. [Fine, 1972]) who, inspired by Tarskian numerical quantifiers, introduced modal op­ erators associated with natural numbers: the so-called graded modal operators Dn and On, with n E IN. Fi­ nally, in the 80's, Fattorosi-Barnaba, De Caro, and Cer­ rato provided sound and complete axiomatizations of graded modal logics , together with some interesting de­ cidability results [Fattorosi-Barnaba and De Caro, 1985; DeCaro, 1988; Cerrato, 1990; 1992] .

Graded modal logics allow one to express conditions on the number of objects satisfying a given property such as: "at least n elements (satisfying relation R) have property y" . Formally, the basic system of graded modal logic K is an extension of K obtained by adding graded modalities . The language of K is obtained from the stan­ dard language of pure modal logic by substituting Dn and On (n E IN) forD and 0. Formulae of I< are:

where p, q, . .. stand for propositional letters, and modal formulae are defined inductively as usual.

It is convenient to define the following abbreviation:

whose intuitive meaning is that <p holds at exactly n R­ accessible worlds.

I< is a normal modal logic with respect to D0 , and it is characterized by the following axioms ( cf. [Fattorosi­ Barnaba and DeCaro, 1985]) :

and by the rules of modus ponens , substitution and ne­ cessitation:

The semantics of I< is given in terms of Kripke frames . In particular, the satisfiability relation is defined as usual over atomic formulae and boolean connectives, while the clauses for graded modalities are the following ones:

It is worth noting that the standard modal operators D and 0 corr~ond to 0 0 and 0 0 , respectively, thereby showing that I< is an extension of I< .

It can be showed that I< is sound and complete with respect to the class of all Kripke frames.

THEOREM 2.1 For any formula <p E Form(!\, <ll), it holds that

Soundness is proved by induction on the structural complexity of <p, while completeness is proved by using an argument a Ia Henkin.

The soundness and completeness proof given for I< can be immediately generalized to deal with all those graded modal logics whose accessibili~ relat~n either excludes pairwise distant worlds (e.g. I<, D, T) or is transitive (e.g. all systems of graded modal logic over 55) . In order to prove the completeness of the remaining graded modal logics, it is necessary to work with a weakened notion of canonical model (cf. [Cerrato, 1990]) .

3 A set-theoretic translation method

In [D'Agostino et al., 1995] D'Agostino et al. proposed a set-theoretic translation method (0-as-Pow translation, from now on) to execute modal logics. The main idea underlying the 0-as-Pow translation is to formalize the notion of validity in Kripke frames by a set-theoretic for­ mula that is provable in the underlying set theory if and only if the original formula is modally derivable. Accord­ ing to the 0-as-Pow translation, any Kripke frame is the set of its worlds and any world in a frame is the set of those worlds accessible from it. The theory driving the translation is a very weak, finitely (first-order) axiom­ atizable set theory, called n [D'Agostino et al. , 1995], whose axioms, in the language with relational symbols E and ~' and functional symbols U, \, and Pow, are:

A peculiarity of the technique is the weakness of the the­ ory n: it consists of only four axioms describing the most rudimentary and basic among the operators of naive set theory. In particular, notice that neither the extension­ ality axiom nor the axiom of foundation are in n. Given a modal formula </J( P1, ... , Pn), its translation is defined as the set-theoretic term <P* ( x, x1 , ... , xn), with variables x,x1, ... ,xn, built using U,\, and Pow. Intuitively, the term <P*(x, x1, ... , Xn) represents the set of those worlds (in the frame x) in which the formula <P holds. The in­ ductive definition of <P* ( x, x1, ... , Xn) is the following:

• P;* = x;;
• (</JV1/;)* =</J*U1/;*;
• e (·</J)* =X\ </J*;
• (0</J)* = Pow(<P*) .

For all modal formulae </J, 1/J, the following results hold, showing, respectively, the completeness and the sound­ ness of the translation [D'Agostino et al., 1995]:

n 'r Vx(Trans(x)I\Vz(x ~ <P*(x, Z))---+ Vz(x ~ 1/;*(x, Z))), and

where Trans(x) stands for Vy (y E x ---+ y ~ x) . It is immediate to see that, for frame-complete theories , the above translation .captures exactly the notion of K,- derivability. ·

3.1 Polymodal logics with finitely many modalities

In [D'Agostino et al., 1995], D'Agostino et al. also show how to generalize the 0-as-Pow translation to polymodal logics . The basic idea is to mimic a polymodal frame, provided with finitely many accessibility relations, with a set, provided with the membership relation only. To this end, D'Agostino et al. defined an alternative seman­ tics for polymodallogic, called p-semantics, that replaces the plurality of accessibility relations <11 , .. . , <lk by a sin­ gle accessibility relation R and k copies U1 , ... , Uk of the universe U. The p-semantics is formally defined as follows.

DEFINITION 3.1 A p-frame :F is a (k + 2)-tuple (U,U1, ... ,Uk,R), where U,U1,, .. , Uk are sets and R is a binary relation On u U U1 U ... U uk I SUCh that, for all u,v,t in U U U1 U . .. U Uk, ifu E U, uRv and vRt, then t E U (we will denote this property by Trans 2 (U)).

The intuition behind the notion of p-frame is the fol­ lowing one. Consider two worlds w, w' E U such that w <1; w' in the original polymodal frame. Since only one accessibility relation is available in p-frames, we cannot directly access w' from w (via R) anymore. However, we can follow a two-step path: first we move to (the unique) w; E U; R-accessible from w; then we move from w; to w' via R.

A p-valuation FP is a subset of U x 4>, where 4> is the set of propositional variables . In the case of boolean combinations, the p-valuation Fp may be lifted to the set of all polymodal formulae in the canonical fashion. In the case of 0;, with i = 1, ... , k, for all u E U we put

A polymodal formula <P is p-valid in a p-frame (U, ul, ... , uk, R) if and only if for all p-valuations FP and all worlds u E U, u FP <P holds.

The link between polymodal frames and p-frames is formally expressed by the following theorem [D'Agostino et al., 1995]:

THEOREM 3.2 If 1/;, <P are polymodal formulae, then 1/J F= <P if and only if <P is p-valid in all p-frames in which 1/J is p-valid.

A set-theoretic counterpart of p-frames can be easily given in the standard way. As far as the t ranslation of the modal operators is concerned, on the ground of the definition of FP> the set-theoretic semantics of 0;¢ becomes:

where x = x U Yl U ... U Yk.

THEOREM 3.3 Let H be a k-dimensional polymodal logic extending K ® ... ® K with the axiom schema 1/J(cxj,, ... , CXjm) . For any polymodal formula </J , (soundness)

(completeness)

where AxiomH(x,yl,··· ,Yk) is Vfi(x ~ '1/;*(x,yl, ... ,yk>fi))), andTrans 2 (x) standsfor'Vy'Vz (y E z l\ z Ex---+ y ~ x), that is, x ~ Pow(Pow(x)) .

4 Translating graded modalities

The general scheme followed for applying the set theo­ retic translation is the one suggested by [Ohlbach et al., 1995]: a two-step translation that first transforms graded modal logic into a polymodal logic with infinitely many modalities , and then reduces derivability in such a poly­ modal logic to derivability in a suitable first-order set theory.

A graded modal logic expresses properties of different (infinitely many) modalities which are all referring to the same accessibility relation. In other words, infinitely many Kripke semantics are provided over the same ac­ cessibility relation scheme. The task of the first step of the translation is that of rewriting the semantics of a graded modal logic in such a way to introduce a dif­ ferent accessibility relation for each different modality. Once this step has been performed, the next task is to generalize the existing translation for polymodal logics with finitely many modalities, to the case of infinitely many ones.

The advantange of using the 0-as-Pow translation is its ability of dealing with non-first-order axiomatizable polymodal logics . This fact has two important conse­ quences: on the one hand, it allows one to naturally translate the polymodal counterpart of I< (I< E), which is indeed non-first-order axiomatizable; on the other hand, it can be applied to non-first-order axiomatizable log­ ics over I< . A further advantage is the fact that the technique introduced is very general and can in fact be employed to translate polymodal logics with infinitely many modalities .

4.1 Polymodal logics with infinitely many modalities

According to Kripke semantics, a I<-formula of the form On<p is true at a given world x of a frame :F = (W, R) if and only if there exists Y ~ R( x) of cardinality greater than n and such that <p is true at any world y E Y.

An alternative interpretation for I< can be obtained introducing a new class of worlds, denoted by Wy, repre­ senting sets of accessible worlds (Wy ~ Pow(W)). The single accessibility relation R can now be replaced by the denumerable set of relations {Rn : n E IN} , where Rn associates a given world x with those elements of Wy having cardinality greater than n . A further accessibil­ ity relation E will be used to associate a given element of Wy with its elements. The situation is described by the following picture:

The alternative semantics described above suggests the introduction of the following modal logi_c I< E. The language of I< E is obtained from that of I< by substi­ tuting (n) , [n], <>, and 0 for <>n and On. Formulae are defined as usual, and denoted by:

The intuitive meaning of the newly introduced symbols is the following:

(n)<p is true at a given world if and only if there exists an Rn-accessible world where <p holds;

O<p is true at a given world if and only if there exists an E-accessible world where <p holds.

It is immediate to see that <>nP and Onp correspond to (n)Op and [n]Op, respectively. Clearly, on the ground of this definition, I< E can turn out much more expressive than I< , since one can combine the modal operators of I< E arbitrarily.

DEFINITION 4.1 Axioms and rules of I<E are the following:

Nl propositional logic axioms together with modus po­ nens;

N2 the axioms of I< for [n] and 0:

The presence of axioms N1-N3 ensures the possibility to give a semantics to I< E simply considering it as a particular polymodal lo1>ic.

It can be shown ( cf. [Ohlbach et al., 1995]) that I< E is not first-order axiomatizable.

The next question to answer is relative to the sound­ ness and completeness of I< E with respect to the chosen semantics. The soundness of I< E can be easily estab­ lished. As for completeness, a partial result can be ob­ tained making use of the following translation function :

DEFINITION 4.2 Let II : C.(K,<I!)--+ C.(KE,<I!) be the function that maps formulae of/{ in formulae of/{ E according to the following rules:

The above translation function is sound and complete ( cf. [Ohlbach et al., 1995]):

From the above result, we derive the completeness of /{ E for the fr~ment of the language consisting of the · translation of /{-formulae (cf. [Ohlbach et al., 1995]) :

THEOREM 4.4 For any formula <p E C.(K,<I!)

The above theorem guarantees the possibility of us­ ing the system /{ E as an intermediate system for the translation described in the next section.

4.2 The set-theoretic translation of graded modal logics

The logic /{ E can be seen as the extension of a normal modal logic Kf[, where n is the set of accessibility re­ lations {Ri : i E IN} U {E}, with the axiom 'l1 = N4 !\ . . . !\ N8. From a general point of view, the problem we want to solve is to design a (set-theoretic) translation method that can be applied to a logic if extending /{­ with a (possibly non-first-order) axiom 1/>(Pj,, .. . , Pim): /{ E will thus be considered as a particular case in which tP(Pju · · · ,Pjm) is '11.

A frame for if is a structure :F = (W, {Ri};eJNE ), where INE stands for IN U {E} . Since fi is a polymodal logic with infinitely many modalities, in order to apply the set-theoretic translation method is necessary to de­ fine a semantics that allows us to consider only one ac­ cessibility relation, to be interpreted by the membership relation E. The fact that we must deal with infinitely many modalities implies that we cannot use the tech­ nique introduced in [D'Agostino et al., 1995]. The key definition for the proposed semantics is the following no­ tion of p-frame.

DEFINITION 4.5

Given a frame :F = (W, {Rn}neJNE) for if, a p-frame is a pair (S, R), where:

• S = WUU;e;INE U;UINE, where the U; 's are pairwise distinct coptes of W ;
• R is a binary relation on S such that
• Vw E W, t E S\(WUINE) , xES (wRt!\tRx--+ x E W U INE);
• Vw E W, i E INE it is not the case that wRi and 3t E S \ (W U INE) (wRt !\ tRi);
• 'VwEW,t,u,ES\(WUINE),i'EINE (wRt!\ wRu !\ tRi !\uRi--+ t = u);
• zv. 'Vt E S\(WUINE),i,j E INE (tRi!\tRj--+ i = j).

For example, the elements x1, . .. , x4 below are those in relation Ri with w. The element t of U; is introduced to simulate such a relation, and the element i is used to determine the index of the relation.

As for the semantics described in the case of finitely many modalities, a p-valuation ~P is a subset W x <I! assigning truth values to propositional variables at W­ worlds only. The extension of FP to all if-formulae is inductively defined as follows :

w ~P [i]<p if and only if Vt( wRt !\ tRi --+ Vv(tRv !\ v ::f i--+ v ~p <p)) .

The following results guarantee that the proposed se­ mantics can be safely used in place of the usual one:

LEMMA 4.6 Given a p-frame (S, R) , there exists a frame (W, {R;};EINE) in which are valid all the formulae p-valid in ( S, R) .

LEMMA 4.7 For any frame (W, {Ri};eiNE), there ex­ ists a p-frame (S, R) in which are p-valid all the formulae valid in (W, { Ri heiNE) .

Any p-frame for fi can be embedded in a model of a suitable set theory in such a way that W is a set , and any w E W is mapped in a set of elements of w; 's for i E IN E . Any w; is of the form w; = { v : w R; v} U { i} .

The transhttion for propositir nal letters and boolean connectives is defined as usual:

The translation of the different modalities must be given according to the p-semantics and replacing the accessi­ bility relation by the membership relation:

'from which it can_ be ~ily checked that the translation of [i]<p, fori E ~;'~ust be defined as follows :

'

Let IT be the sub-theory of the theory De introduced in [Benthem et al. , 1995] and defined as follows:

The following two theorems state the completeness and the soundness of the proposed translation with re­ spect to IT:

THEOREM 4.8 (Completeness) For any modal formula cp E C(Kn:) we have that

where Trans 2 (x, y) stands for the conjunction of the clauses on R introduced in the definition of p-frame, and Axiomj[(x, y) is the translation of the formula consisting of the conjunction of the axioms of fi .

THEOREM 4.9 (Soundness) For any modal for­ mula cp E C(Kn:)

Once we have defined the set-theoretic translation in the context of a generic extension fi of Kn:, the result for K E follows as a special case:

.where Axiom:KE(x, y) is the translation of '11, namely Vz(x ~ 'll*(x, y, Z)) .

Notice that the soundness of the translation is stated with respect to the validity in K E, since we do not have the completeness of K E with respect to derivabil­ ity. However, using the translation function II we can prove the following theorem:

THEOREM 4.10 For any formula cp E C(K) we have that:

5 Conclusions and further directions

In this paper, we generalized the 0-as-Pow translation, proposed by D'Agostino et al. in [D'Agostino et al., 1995], to apply it to graded modal logic. The result­ ing method allows us to support automated reasoning in a large class of knowledge representation formalisms that can be reduced to graded modal logic. It can actu­ ally be applied to polymodal logics with infinitely many modalities. Indeed, there are no axioms in the underly­ ing set theory constraining the behavior of the different modalities; such a behavior is governed by (the trans­ lation of) the axioms of the considered polymodallogic. As an example, it can be exploited to execute two-sorted metric temporal logics [Montanari and de Rijke, 1995], provided that they are reinterpreted as (a special kind of) propositional dynamic logics .