Modal Logic and Set Theory: a Set-Theoretic Interpretation of Modal Logic

Giovanna D’Agostino, Angelo Montanari, and Alberto Policriti

Abstract

In this paper, we describe a novel set-theoretic interpretation of modal logic and show how it allows us to build promising bridges between modal deduction and settheoretic reasoning. More specifically, we describe a translation technique that maps modal formulae into set-theoretic terms, thus making it possible to successfully exploit derivability in first-order set theories to implement derivability in modal logic.

Contents

1 Introduction 2 2 The □-as-℘ translation 3 3 Elicitation of set principles that ensure the faithfulness of the

translation 5 4 Faithfulness of the translation in means of proof 6 5 Capturing full K-derivability 7 6 Translating extended modal logics 7 7 Translating polymodal logics 9

1 Introduction

The mathematical approach to modal logic started at the beginning of this century with the limited purpose of studying formally the notion of necessity. The machinery developed since those pioneering days later demonstrated to be adaptable to a wide variety of fields. Today, there is a plenty of applications— especially in computer science—of methods, tools, and notions introduced in the realm of modal logic. For most computer science applications, efficient support of derivability in modal logic is a key issue.

In this paper, we describe a novel set-theoretic interpretation of modal logic, that was originally proposed in [DMP95] and later developed in [BDMP97, BDMP98], and show how it allowed us to build promising bridges between modal deduction and set-theoretic reasoning. More specifically, we describe a translation technique that maps modal formulae into set-theoretic terms, thus making it possible to successfully exploit the automated theorem-proving machinery for first-order set theories to implement derivability in modal logic. Barwise and Moss described in [BM96] the use of hypersets as a tool to develop modal logic, and some of the steps in the basics of their treatment are similar to those presented here.

We begin by observing that it is not surprising that a mapping from modal formulae to set-theoretic ones exists, as modal logic theories naturally translate into fragments of second-order logic (cf. [Ben85]). Actually, the translation we present in the following can be seen as a technique to tailor axiomatically a fragment of second-order logic in which such a translation can be carried out.

The main goal of the translation is to extend the celebrated set-theoretic interpretation of the propositional connectives ∧, ∨, and ¬ to the □-operator, that is, to the (propositional) modal logic language. In other words, we want to extend to the box operator the correspondence that associates set-intersection to conjunction, set-union to disjunction, and complementation (set-difference) to negation. In the boolean collections used to interpret pure propositional sentences there was no need for a set to be an element of another one; the crucial point of the extension of the interpretation to the modal language is the use of this typical property of the membership relation ∈. It will be necessary to abandon the “flat” collection of sets sufficient to analize true propositional sentences, in favour of more elaborated universes where sets that can be elements of other sets (and possibly non-well-founded). Unfortunately, another very basic characteristic of most universes of sets, namely, the principle of extensionality, does not fit with the translation and hence the set theories adopted here will always be deprived of the corresponding axiom.

The main features of the technique we will describe are the following:

• binary relations will always be represented by the familiar ∈;

• the necessity operator □ is encoded directly as the set-theoretic powerset operator ℘;

• the axiomatic set theory driving the translation is a (significant) parameter of the translation. Such a translation was originally proposed in the context of automated the-

orem proving for modal logic. In this area, translations from modal logics into first-order logic are often used, since they allow one to use very sophisticated and well-performing theorem provers to automatically derive modal logic formulae. From this point of view, the larger the class of translatable logics is, the better. However, the most used translations in the field are the standard one and variations of it, which essentially allow one to translate only the class of first-order complete logics. On the contrary, the proposed translation works for all complete modal logics, regardless of the first-order axiomatizatibility of their semantics. Furthermore, it also works if the modal logic under consideration is specified only by Hilbert axioms. Finally, it can be applied to extended modal logics by tuning the set theory driving the translation in a suitable way.

Throughout the paper we will work exclusively with propositional modal logic. A challenging goal is to design an adaptation of the proposed method to first-order modal logic systems. Some preliminary results on this can be found in [Sla98].

2 The □-as-℘ translation

We begin with a semi-formal description of the set-theoretic translation technique applied to the base case of K. Next we will prove the faithfulness of the translation and we will see how to deal with modal logics extending this minimal system.

We will use in the following a fairly standard syntax for propositional modal logic, consisting of propositional variables (or letters) P_{1}, P_{2}, …, logical connectives ∧, ¬, and the modal operator □. Derived symbols, to be used as abbreviations, will be ◇ (defined as ¬□¬) and ∨. Well-formed formulae are defined as usual, exploiting the □ operator as a unary operator.

The so-called standard translation of a modal formula θ(P_{1}, …, P_{n}) is the first-order formula ST (θ)(x, P_{1}, …, P_{n}), where P_{1}, …, P_{n} are set variables corresponding to propositional letters P_{1}, …, P_{n}, defined as follows:

• ST (P_{i}) = P_{i}(x_{0});

• ST (ϕ ∨ ψ) = ST (ϕ) ∨ ST (ϕ);

• ST (¬ϕ) = ¬ST (ϕ);

• ST (□ϕ) = ∀y (x_{0}Ry → ST (ϕ)(y|x_{0})),

where y does not occur in ST (ϕ) and y|x_{0} denotes uniform substitution of y for x_{0}. The closed standard translation \overline{ST} (ϕ) of a modal formula ϕ is defined as the second-order sentence ∀P_{1} … ∀P_{n}∀x ST (ϕ), and it is easy to see that

ψ ⊧_{f} φ if and only if \overline{ST} (ψ) ⊧ \overline{ST} (φ),

where the ⊧ on the right-hand side denotes second-order logical consequence.

The basic idea of the set-theoretic translation is simply to replace the accessibility relation R of the Kripke semantics with the membership relation ∈. A world v accessible from w becomes an element of w and a further step from v, using the accessibility relation R, will amount to looking into v in order to reach for one of its elements. Other interesting consequences are the following:

1. worlds, frames, and valuations of propositionals variables become simply sets (of worlds);

2. a frame F can be identified with its support W, being the accessibility relation implicitly defined as the membership relation on W.

Moreover, since we clearly want that all worlds v accessible from a given world w in a frame W turn out to be themselves elements of W, it is natural to require that all frames are transitive sets.

As a valuation for a propositional variable is nothing but a set of worlds, the standard definition of ⊧ will allow us to associate a set of worlds to each propositional formula. This set, inductively defined on the structural complexity of the formula, will be the collection of those worlds in the frame in which the formula holds. Let us denote by ⋆ our map from modal formulae to settheoretic terms and by x a variable used to denote the set W of all possible worlds. The term P_{i}^{⋆} will denote the set of worlds at which the propositional variable P_{i} holds and, in general, the set φ^{⋆} of worlds at which a formula φ evaluates to true is inductively defined starting with the following familiar rules for propositional connectives:

\begin{aligned}( φ ∧ ψ)^{⋆} & =_{Def} & φ^{⋆} ∩ ψ^{⋆}; \\ ( ¬φ)^{⋆} & =_{Def} & x \ φ^{⋆}. \end{aligned}

In order to complete the definition, we must deal with formulae of the form □φ. It turns out that the definition of ⋆ on such formulae is entirely forced by the Kripke semantics of □ together with our assumption that the accessibility relation R is replaced by ∈. In fact:

w ⊧ □φ if and only if ∀v(w R v →v ⊧ φ),

and hence, replacing R by ∋, inductively we obtain

w ⊧ □φ if and only if ∀v (v ∈ w →v ∈ φ^{⋆}),

which is to say that □φ holds true at w if and only if w is a subset of φ^{⋆}. This allows us to complete our definition by putting

( □φ)^{⋆} =_{Def} ℘( φ^{⋆}).

At this point the relation ⊧ can be entirely superseded by the membership relation ∈.

If we let the P_{i}^{⋆}’s and x be (pairwise distinct) set variables, ⋆ is a syntactic translation mapping modal formulae into set-theoretic terms written in a language endowed with the symbols ∩, \, and ℘. From now on such a translation will be called □-as-℘ translation (box-as-powerset translation).

Let y_{1}, …, y_{n} (y⃗, fom now on) denote the set variables P_{i}^{⋆} introduced in φ^{⋆}. By applying the □-as-℘ translation, the fact that a formula φ is satisfied in the frame W with respect to a given valuation P_{1}, ..., P_{n}, amounts to say that the substitution of W for x and of P_{i} for y_{i} satisfies x ⊆ φ^{⋆}(x, y⃗). To say that a formula φ is satisfied in W corresponds to saying that ∀y⃗(x ⊆ φ^{⋆}(x, y⃗)). Finally, the fact that φ is valid is stated as ∀x, y⃗(x ⊆ φ^{⋆}(x, y⃗))).

Our next task is now to provide a system of set-theoretic axioms which allows us to use the previously defined ⋆ in order to prove modal theorems.

3 Elicitation of set principles that ensure the faithfulness of the translation

In order to isolate the principles governing the membership relation in this area, the first fact that must be taken into account is the following: ∈ cannot have properties that cannot be guaranteed also for a generic accessibility relation R. Hence ∈ can be neither acyclic nor extensional, and our “minimalist” approach to axiomatic set theory becomes a necessity in this context. The axiomatic set theory that will be introduced for our purpose (to be called Ω) is extremely simple: its axioms are, essentially, the definitions of the set-theoretic operators employed in the □-as-℘ translation.

\begin{matrix}x ∈ y ∪ z & ↔ & x ∈ y ∨ x ∈ z; \\ x ∈ y \ z & ↔ & x ∈ y ∧ x ∉ z; \\ x ⊆ y & ↔ & ∀z(z ∈ x→z ∈ y); \\ x ∈ ℘(y) & ↔ & x ⊆ y. \end{matrix}

The key feature of the above introduced theory Ω is its (quasi) minimality in providing a formal counterpart to the idea underlying the □-as-℘ translation. This fact is expressed by the following two results, to be proved below:

\begin{aligned}⊢_{K} φ & ⇒ & Ω ⊢ ∀ x( Tr( x)→∀ y⃗ ( x ⊆ φ^{⋆}(x, y⃗) ) ), \\ ⊧_{f} φ & ⇐ & Ω ⊢ ∀ x( Tr( x)→∀ y⃗ ( x ⊆ φ^{⋆}(x, y⃗) ) ). \end{aligned}

where Tr( x) stands for ∀y(y ∈ x → y ⊆ x) (transitivity of x).

When a modal theory is given by a set of Hilbert’s axioms, whose conjunction we denote by ψ, the above results become:

\begin{aligned}ψ ⊢_{K} φ & ⇒ & Ω ⊢ ∀ x( Tr( x) ∧ ∀z⃗ ( x ⊆ ψ^{⋆}(x, z⃗) )→∀ y⃗ ( x ⊆ φ^{⋆}(x, y⃗) ) ), \\ ψ ⊧_{f} φ & ⇐ & Ω ⊢ ∀ x( Tr( x) ∧ ∀z⃗ ( x ⊆ ψ^{⋆}(x, z⃗) )→∀ y⃗ ( x ⊆ φ^{⋆}(x, y⃗) ) ). \end{aligned}

Moreover, if ψ turns out to be frame-complete (cf. [Ben85]), the two above results guarantee an exact correspondence between modal and set-theoretic derivability. In such cases, the following holds:

ψ ⊢_{K} φ ⇔ Ω ⊢ ∀ x( Tr( x) ∧ ∀z⃗ ( x ⊆ ψ^{⋆}(x, z⃗) )→( ∀ y⃗ ( x ⊆ φ^{⋆}(x, y⃗) ) ).

The above formulation suggests another possible reading of the effect of the □-as-℘ translation: when applied, it provides a form of deduction theorem for modal logics modulo the underlying set theory Ω.

As a matter of fact, Ω is not the minimal set theory capable of driving the □-as-℘ translation. The weaker theory MM (Minimal Modal) obtained by replacing the axiom defining ℘ by the following two theorems of Ω:

\begin{aligned}x ⊆ y & → & ℘( x) ⊆ ℘( y); \\ ℘( x ∩ y) & ⊆ & ℘( x) ∩ ℘( y), \end{aligned}

is the minimal set theory that can be used to drive the translation.

We conclude this section with a comment on the following quotation from Bledsoe:

“ The author was one of the researchers working on resolution type systems who “made the switch”. It was in trying to prove a rather simple theorem in set theory by paramodulation and resolution, where the program was experiencing a great deal of difficulty, that we became convinced that we were on the wrong track. ”

( W. W. Bledsoe, 1977 )

The “rather simple theorem in set theory” was the following:

℘(x) ∩ ℘(y) = ℘(x ∩ y),

which one could observe, in view of the capabilities of the theory MM, to be not-so-simple.

4 Faithfulness of the translation in means of proof

The faithfulness of the □-as-℘ translation was originally proved in [DMP95] by using tools of non-well-founded set theory. The proof consists of two steps. First we show that, whenever a modal formula φ is derivable from a modal formula ψ in K, the theory Ω derives the translating sentence relating φ^{⋆} and ψ^{⋆}: we call this fact completeness of the translation. Subsequently we show the soundness of the translation, namely, that whenever Ω shows the translating sentence relating φ^{⋆} and ψ^{⋆}, the formula ψ is a frame logical-consequence of φ.

Theorem 1 (Completeness of □-as-℘)

ψ ⊢_{K} φ ⇒ Ω ⊢ ∀ x( Tr( x) ∧ ∀z⃗ ( x ⊆ ψ^{⋆}(x, z⃗) )→∀ y⃗ ( x ⊆ φ^{⋆}(x, y⃗) ) ).

The proof is by induction on the length of a derivation in K. It is rather straightforward, except for some care to be taken in order to cope with the lack of estensionality in Ω. As an example, the commutativity of set union A ∪ B = B ∪ A can not be assumed in models of Ω. Nevertheless, the proof can be carried out on the weaker condition that A ∪ B ⊆ B ∪ A ∧ B ∪ A ⊆ A ∪ B, which holds in every model of Ω.

Theorem 2 (Soundness of □-as-℘)

ψ ⊧_{f} φ ⇐ Ω ⊢ ∀ x( Tr( x) ∧ ∀z⃗ ( x ⊆ ψ^{⋆}(x, z⃗) )→∀ y⃗ ( x ⊆ φ^{⋆}(x, y⃗) ) ).

For any given frame (W, R), the soundness proof essentially builds a corresponding Ω-model, such that the frame is a transitive element x of the model and R is mimicked by ∈. Since R can contain “cycles”, we need a non-well-founded universe. The Ω-model can be built in such a way that, for all modal formulae ϕ, ϕ is valid in (W, R) if and only if ∀z⃗(x ⊆ ϕ^{⋆}(x, z⃗)) holds in the model (cf. [DMP95]).

A simpler proof of the completeness and soundness of the □-as-℘ translation, based on a comparison between the standard translation and the □-as-℘ translation, was given in [BDMP97].

5 Capturing full K-derivability

In this section, we show how the □-as-℘ translation can be adapted to capture the so-called general frame semantics. Our starting point is the notion of general frame and its adequacy to capture the modal deduction in K. A general frame is a pair (F, W), where F is a frame and W is a set of subsets of W, which is closed under the boolean operations of union, complementation with respect to W, and □(X) = {w ∈ W : ∀v (wRv → v ∈ X)}. Validity in general frames is defined as for frames, except for the fact that we only consider valuations such that the set of worlds at which a given propositional variable holds belongs to W. Logical consequence in general frames (ψ ⊧_{gf} φ) is defined accordingly. For all modal formulae ψ, φ, we have

ψ ⊢_{K} φ if and only if ψ ⊧_{gf} φ.

In order to deal with the general frame semantics, we introduce in the translating formula a new variable y denoting a set of possible valuations (closed under the set-theoretic counterparts of standard modal operations). Formally, let Cl(y, x) be the conjunction of the following formulae:

• ∀z (z ∈ y → ℘(z) ∩ x ∈ y);

• ∀z (z ∈ y → x \ z ∈ y);

• ∀zu (z ∈ y ∧ u ∈ y → z ∪ u ∈ y).

We also modify the translation of □ as follows:

(□ϕ)^{∗} = ℘(ϕ^{∗}) ∩ x.

It is not difficult to prove (cf. [BDMP97] for details) that, for all modal formulae ψ, φ, the following holds:

ψ ⊢_{K} φ ⇔ Ω ⊢ ∀xy (Tr(x) ∧ Cl(y, x) ∧ ∀x⃗ ∈ y (x ⊆ ψ^{∗}(x, x⃗)) →
∀x⃗ ∈ y (x ⊆ φ^{∗}(x, x⃗))).

6 Translating extended modal logics

The technique presented in the previous paragraphs can be exploited to translate a number of other modal formalisms. In this and the next section we will briefly survey some meaningful cases.

On the ground of the translation for general frame semantics, we will show that playing with the underlying axiomatic set-theory, a number of extended modal logics can be translated into set theory along the lines of the □-as-℘ translation. It will be interesting to note how a known and extremely important set theory, the theory of the constructible sets (with minor variations), will come into play.

The first extended modal logic to which we can extend our translation technique is logical consequence in general frames closed under L_{0}-definition. In order to define such a kind of logical consequence, we need to introduce a weak system of second order logic called L_{2}. Let (the language of) L_{2} be a secondorder language containing a binary predicate R and equality. In [Ben79], axiomatic theories for deduction in the L_{2}-language are introduced. In particular, a system of weak second-order logic is defined by means of a suitable form of substitution. Let an L_{0}-formula be an L_{2}-formula without occurrences of second-order quantifiers. Given an L_{2}-formula α and an L_{0}-formula γ(x), denote by α(γ|P) the L_{2}-formula obtained from α by replacing the occurrences of P(u) in which the P is free in α by γ(u|x) (after changing bound variables as necessary [Ben79]). L_{0}-substitution is expressed by the following schema, where α is an L_{2}-formula and γ is an L_{0}-formula:

∀Pα → α(γ|P).

Weak second-order logic contains a set of axioms which is complete for first-order predicate logic plus L_{0}-substitution. It is possible to show that weak second-order logic is a non-conservative extension of K, namely, ψ ⊧_{K} φ → \overline{ST} (ψ) ⊧_{L_{2}} \overline{ST} (φ), but there exist ψ and φ such that \overline{ST} (ψ) ⊧_{L_{2}} \overline{ST} (φ) and ψ |̸=_{K} φ [Ben79]. A semantic counterpart of deducibility in weak second-order logic can be obtained by means of closure under L_{0}-definitions in general frames. A general frame (F, W) is closed under L_{0}-definitions if, for all L_{0}-formulae γ, with free world-variables x, x_{1}, …, x_{n} and free set-variables X_{1}, …, X_{m}, and for all w_{1}, …, w_{n} ∈ W and A_{1}, …, A_{m} ∈ W, the set {w ∈ W : F ⊧ γ(w, w_{1}, …, w_{n}, A_{1}, …, A_{m})} belongs to W. Given two L_{0}-sentences α and β, it holds that α ⊧_{L_{2}} β if and only if for all general frames (F, W) closed under L_{0}-definitions, if (F, W) ⊧ α, then (F, W) ⊧ β.

The set theory underlying the translation will be a theory whose axioms are closely related to the so-called Gödel operations for defining the constructible universe. Among all possible approaches, we choose a weaker version of the one proposed by Barwise in [Bar75] with the aim of stating our results for a theory as weak as possible. We introduce functions defining the singleton operator, suitable cartesian products (×, ×_{=}, ×_{∈}), together with the associated projections (Dom, Rng), plus some operations allowing us to manipulate argument positions in ordered sequences (C_{1}, C_{2}). Let us call Ω_{c} the resulting theory. Its language consists of =, ∈, and ⊆ as predicate symbols, {}, Dom, and Rng as unary functional symbols, and ∪, \, ×, ×_{∈}, ×_{=}, C_{1}, and C_{2} as binary functional symbols. The axioms for Ω_{c} are the identity axioms and the axioms, already in Ω, describing ⊆, ∪, and \ in terms of ∈ (cf. Section 2), plus the axioms defining {}, ×, ×_{∈}, ×_{=}, Dom, Rng, C_{1}, and C_{2}, listed below:

t ∈ {x} ↔ t = x;
t ∈ x × y ↔ ∃a ∈ x∃b ∈ y (t = ⟨a, b⟩);
t ∈ x ×_{∈} y ↔ ∃a ∈ x∃b ∈ y (t = ⟨a, b⟩ ∧ a ∈ b);
t ∈ x ×_{=} y ↔ ∃a ∈ x∃b ∈ y (t = ⟨a, b⟩ ∧ a = b));
t ∈ Dom(x) ↔ ∃s (⟨t, s⟩ ∈ x);
t ∈ Rng(x) ↔ ∃s (⟨s, t⟩ ∈ x);
t ∈ C_{1}(x, y) ↔ ∃a∃b∃c (⟨a, b⟩ ∈ x ∧ c ∈ y ∧ t = ⟨a, ⟨b, c⟩⟩);
t ∈ C_{2}(x, y) ↔ ∃a∃b∃c (⟨a, c⟩ ∈ x ∧ b ∈ y ∧ t = ⟨a, ⟨b, c⟩⟩),

where ⟨x, y⟩ is the usual a shorthand for {{x}} ∪ {{x} ∪ {y}}. Inductively, we denote by ⟨x_{1}, …, x_{n}⟩ the pair ⟨x_{1}, ⟨x_{2}, …, x_{n}⟩⟩.

The theory Ω_{c} differs from the classical approach to constructible sets (cf. [Ber37]) mainly in the following points: (i) we do not introduce classes; (ii) we do not introduce the axioms of choice, infinity, replacement, and powerset, since they are not needed; (iii) we do not introduce any form of extensionality, since our aim is to use the membership relation to mimic the accessibility relation in frames; (iv) the existence of singletons replaces the existence of pairs, and binary union replaces (the stronger) unary union.

The translation function (·)^{∗} is the same as that given in Section 2, except for the □ operator. This is obviously the case, because we do not have ℘ among the symbols in the language of Ω_{c}. Moreover, Tr(x) disappears from the antecedent of the translated sentence.

To understand these changes, it can be easily checked that, in the case of Ω, it would have made no difference to work with (□ϕ)^{∗} defined either as ℘(ϕ^{∗}) or as ℘(ϕ^{∗}) ∩ x (cf. Section 2). Actually, we chose the first alternative only to maintain the translated terms simpler. It is also easy to see that ℘(ϕ^{∗}) ∩ x = {y ∈ x : y ∩ x ⊆ ϕ^{∗}}, whenever x is transitive; as a matter of fact, we will see that the set {y ∈ x : y ∩ x ⊆ ϕ^{∗}} can always be used to translate □ϕ (even in the case in which x is not transitive). Finally, since the following holds:

{y ∈ x : y ∩ x ⊆ ϕ^{∗}} = x \ Rng((x \ ϕ^{∗}) ×_{∈} x),

we put:

(□ϕ)^{∗} = x \ Rng((x \ ϕ^{∗}) ×_{∈} x).

It can be proved (see [BDMP98]) that the above translation is sound and complete, that is, for any pair of modal formulae ψ, φ:

L_{2} ⊧ \overline{ST} (ψ) → \overline{ST} (φ) ⇔ Ω_{c} ⊧ ∀x(∀z⃗ (x ⊆ ψ^{∗}(x, z⃗)) → ∀z⃗ (x ⊆ φ^{∗}(x, z⃗))).

Other extensions of the technique capable to deal with new modal operators are possible: in [BDMP98] the modal logic of inequality [Rij92], the so-called irreflexivity rule [Gab81], and minimal tense logic [Bur84] are considered and, for each of them, an extension of the translation together with a subtheory of Ω_{c} sufficient to drive the translation are introduced.

7 Translating polymodal logics

In this section, we generalize the □-as-℘ translation to polymodal logics. Our approach can be seen as a (completely symmetric) set-theoretic version of Thomason’s technique to reduce frame validity in tense logic to that in modal logic [Tho74, Tho75].

The main problem is to map a polymodal frame, consisting of a set U endowed with k accessibility relations ◁_{1}, …, ◁_{k}, with k > 1, into a set provided with the membership relation only. We solved this problem by first providing polymodal logics with an alternative semantics (p-semantics) that transforms the plurality of accessibility relations ◁_{1}, …, ◁_{k} into a single accessibility relation R together with k subsets U_{1}, …, U_{k} of U.

Definition 1 A p-frame F is a (k+2)-tuple (U, U_{1}, …, U_{k}, R), where U, U_{1}, …, U_{k} are sets and R is a binary relation on U ∪ U_{1} ∪ … ∪ U_{k}, such that, for all u, v, t in U ∪ U_{1} ∪ … ∪ U_{k}, if u ∈ U, uRv and vRt, then t ∈ U (we will denote this property by Tr^{2}(U)).

A p-valuation assigns a truth value to propositional variables only at worlds belonging to U. Formally, a p-valuation ⊧_{p} is a subset of U × Φ, where Φ is the set of propositional variables.

In the case of boolean combinations, the p-valuation ⊧_{p} may be lifted to the set of all polymodal formulae in the canonical fashion. In the case of □_{i}, with i = 1, …, k, for all u ∈ U we put

u ⊧_{p} □_{i}ϕ ⇔ ∀v(uRv ∧ v ∈ U_{i} → ∀t(vRt → t ⊧_{p} ϕ)).

Definition 2 A polymodal formula ϕ is p-valid in a p-frame (U, U_{1}, …, U_{k}, R) if and only if for all p-valuations ⊧_{p} and all worlds u ∈ U, u ⊧_{p} ϕ holds.

On the basis of the above definitions, the following lemma holds:

Lemma 1 Given a p-frame (U, U_{1}, …, U_{k}, R), there exists a classical polymodal frame (U, ◁_{1}, …, ◁_{k}), based on the set U, that validates all and only the formulae ϕ which are p-valid in (U, U_{1}, …, U_{k}, R) and, for every classical polymodal frame (U, ◁_{1}, …, ◁_{k}), there exists a p-frame (U, U_{1}, …, U_{k}, R) that p-validates exactly the formulae which are valid in (U, ◁_{1}, …, ◁_{k}).

Lemma 1 guarantees that any p-frame F = (U, U_{1}, …, U_{k}, R) can be reduced to a p-frame F′ = (U, U′_{1}, …, U′_{k}, R′) such that U, U′_{1}, …, U′_{k} are pairwise disjoint. ¿From them, we have:

Theorem 3 If ψ, φ are polymodal formulae, then

ψ ⊧ φ ⇔ φ is p-valid in all p-frames in which ψ is p-valid.

We are now ready to introduce the translation for polymodal logics. As in the soundness proof for the monomodal case, we interpret any p-frame (U, U_{1}, …, U_{k}, R) as a (k + 1)-tuple U^{∗}, U_{1}^{∗}, …, U_{k}^{∗} of “sets” in a particular Ω-model such that, for all elements t^{∗} of the model which are ∈-related to U^{∗} ∪ U_{1}^{∗} ∪ … ∪ U_{k}^{∗}, we have t^{∗} = {s^{∗} : tRs}.

As in the monomodal case, every p-valuation of P_{1}, …, P_{n} on the p-frame is interpreted in terms of n subsets P_{1}^{∗}, …, P_{n}^{∗} of U^{∗}. Moreover, for each polymodal formula ϕ, we define its translation as a term ϕ^{∗}(x, y_{1}, …, y_{k}, x_{1}, …, x_{n}) such that, for all u ∈ U,

u ⊧_{p} ϕ ⇔ u^{∗} ∈ ϕ^{∗}(U^{∗}, U_{1}^{∗}, …, U_{k}^{∗}, P_{1}^{∗}, … P_{n}^{∗}).

Under this constraint, the definition of the translation of □_{i}ϕ directly follows from the definition of ⊧_{p} (and induction):

(□_{i}ϕ)^{∗} ≡ ℘(((x ∪ y_{1} ∪ … ∪ y_{k}) \ y_{i}) ∪ ℘(ϕ^{∗})).

The following theorems state the soundness and completeness of the translation method for polymodal logics (cf. [DMP95]).

Theorem 4 (Soundness) Let H be a k-dimensional polymodal logic extending K ⊗…⊗K with the axiom schema ψ(α_{j_{1}}, …, α_{j_{m}}). For any polymodal formula φ involving n propositional variables P_{1}, …, P_{n},

\begin{aligned}Ω & ⊧ & ∀x∀y_{1} … ∀y_{k}(Tr^{2}(x) ∧ Ax_{H}(x, y_{1}, …, y_{k}) → \\ & & ∀x_{1} … ∀x_{n}(x ⊆ φ^{∗}(x, y_{1}, …, y_{k}, x_{1}, …, x_{n}))) & ⇒ & ψ ⊧_{f} φ, \end{aligned}

where Ax_{H}(x, y_{1}, …, y_{k}) is ∀x_{1} … ∀x_{m}(x ⊆ ψ^{∗}(x, y_{1}, …, y_{k}, x_{1}, …, x_{m}))), and Tr^{2}(x) stands for ∀y∀z (y ∈ z ∧ z ∈ x → y ⊆ x), that is, x ⊆ ℘(℘(x)).

Theorem 5 (Completeness) Let H be a k-dimensional polymodal logic extending K ⊗ … ⊗ K by means of the axiom schema ψ(α_{j_{1}}, …, α_{j_{m}}). For each polymodal formula φ involving n propositional variables P_{1}, …, P_{n},

\begin{aligned}⊢_{H} φ & ⇒ & Ω & ⊧ & ∀x∀y_{1} … ∀y_{k}(T r^{2}(x) ∧ Ax_{H}(x, y_{1}, …, y_{k}) → \\ & & & & ∀x_{1} … ∀x_{n}(x ⊆ φ^{∗}(x, y_{1}, …, y_{k}, x_{1}, …, x_{n}))) \end{aligned}

As in the case of monomodal logics, if H is complete, then, by Theorems 4 and 5, modal derivability of a given formula in H is equivalent to first-order derivability of the translated formula in Ω.

In [MP97b], we showed how to adapt the □-as-℘ translation for polymodal logics with finitely many modalities to encompass the infinite number of accessibility relations of graded modal logics. This allows us to support automated reasoning in a large family of knowledge representation formalisms, including terminological logics, epistemic logics, and universal modalities, which can be represented using graded modalities. In [MP97a], we showed how the □-as-℘ translation can also be applied to metric temporal logics, by first providing a PDL-like reformulation of metric temporal logics and, then, by interpreting them as polymodal logics with an infinite number of accessibility relations, each one corresponding to a different temporal displacement. As a matter of fact, graded modal logics and metric temporal logics are treated as a special case of a more general technique able to deal with polymodal logics with infinitely many modalities.

References

[Bar75] J. Barwise. Admissible sets and structures. Springer Verlag,, 1975.

[BM96] J. Barwise and L. Moss. Vicious Circles. CSLI Publications Notes, vol. 60, Stanford, 1996.

[BDMP97] J. F. A. K. van Benthem, G. D’Agostino, A. Montanari, and A. Policriti. Modal deduction in second-order logic and set theory-I. Journal of Logic and Computation, 7(2):251–265, 1997.

[BDMP98] J. F. A. K. van Benthem, G. D’Agostino, A. Montanari, and A. Policriti. Modal deduction in second-order logic and set theory-II. Studia Logica, 60(3):387–420, 1998.

[Ben79] J. F. A. K. van Benthem. Syntactic aspects of modal incompleteness theorems. Theoria, 45:67–81, 1979.

[Ben85] J. F. A. K. van Benthem. Modal Logic and Classical Logic. Bibliopolis and Atlantics Heights, 1985.

[Ber37] P. Bernays. A system of axiomatic set theory. Part I. Journal of Symbolic Logic, 2:65–77, 1937.

[Bur84] J.P. Burgess. Basic tense logic. In D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II, pages 89–133. D. Reidel, Dordrecht-Holland, 1984.

[DMP95] G. D’Agostino, A. Montanari, and A. Policriti. A set-theoretic translation method for polymodal logics. Journal of Automated Reasoning, 15:317–337, 1995.

[Gab81] D. M. Gabbay. An irreflexivity lemma with applications to axiomatizations of conditions on tense frames. In U. Mönnich, editor, Aspects of Philosophical Logic, pages 67–89. D. Reidel, Dordrecht-Holland, 1981.

[MP97a] A. Montanari and A. Policriti. Executing metric temporal logic. In Proceedings of the IJCAI97 Workshop on Programming in Temporal and Non Classical Logics, Nagoya, Japan, 1997.

[MP97b] A. Montanari and A. Policriti. A set-theoretic approach to automated deduction in graded modal logics. In Proceedings of the International Joint Conference on Artificial Intellicence, IJCAI97, Nagoya, Japan, 1997.

[Rij92] M. de Rijke. The modal logic of inequality. Journal of Symbolic Logic, 57:566–584, 1992.

[Sla98] M. Slanina. Sistemi di traduzione e implementazione per logiche modali. Tesi di laurea dell’Università degli studi di Udine, 1998.

[Tho74] S. K. Thomason. Reduction of tense logic to modal logic I. Journal of Symbolic, 39(3):549–551, 1974.

[Tho75] S. K. Thomason. Reduction of tense logic to modal logic II. Theoria, 41:154–169, 1975.