A Sahlqvist Theorem for Relevant Modal Logics

Takahiro Seki

                            tseki@jaist.ac.jp

School of Information Science, Japan Advanced Institute of Science and Technology

1 Introduction

Kripke-completeness of every classical modal logic with Sahlqvist formulas is one of the basic general results on completeness of classical modal logics. This paper shows a Sahlqvist theorem for modal logic over the relevant logic R in terms of Routley-Meyer semantics. Our completeness result covers most of completeness results of relevant modal logics so far. It is shown that usual Sahlqvist theorem for classical modal logics can be obtained as a special case of our theorem.

Below, &, ⇒, ⇔, ∀ and ∃ are used to denote respectively conjunction, implication, equivalence, universal and existential quantifiers in the metalanguage. Further, Prop and Wff denote the set of all propositional variables and formulas, respectively.

2 Preliminaries

A regular relevant modal logic over R (a regular logic over R, for short) is a logic obtained from R by adding the axioms

□A ∧ □B → □(A ∧ B) ◇(A ∨ B) → ◇A ∨ ◇B

and the rules of inference

\frac{A → B A}{B}  \frac{A B}{A ∧ B}  \frac{A → B}{□A → □B}  \frac{A → B}{◇A → ◇B} .

The least regular logic over R is called R.C_{□◇} . In the following, we assume that L denotes any regular logic over R.

Our models are obtained by extending the enlarged R-model in the sense of [5]. An R.C_{□◇} -frame is a 7-tuple ⟨O, W, R, S_{□} , S_{◇} ,^{∗} , u⟩, where W is a non-empty set of all worlds, O is a non-empty subset of W, R is a ternary relation on W, S_{□} and S_{◇} are binary relations on W, ^{∗} is an unary operation on W and u, called the universal world, is a element of W. An R.C_{□◇} -frame ⟨O, W, R, S_{□} , S_{◇} ,^{∗} , u⟩ satisfies first order sentences in the predicates O, R, S_{□} , S_{◇} , ^{∗} and the constant u which are omitted in this paper.

We call a pair ⟨𝔉, V ⟩ an R.C_{□◇} -model on an R.C_{□◇} -frame 𝔉 = ⟨O, W, R, S_{□} , S_{◇} ,^{∗} , u⟩ (we simply say an R.C_{□◇} -model), where 𝔉 is an R.C_{□◇} -frame and V is a mapping from Prop to 2^{W}, called a valuation on 𝔉, which satisfies that for all a, b ∈ W and all p ∈ Prop, u ∈ V (p) and a ≤ b & a ∈ V (p) ⇒ b ∈ V (p).

Given an R.C_{□◇} -model ⟨O, W, R, S_{□} , S_{◇} ,^{∗} , u, V ⟩, for a ∈ W and A ∈ Wff, a relation ⊧ between W and Wff is defined inductively as follows:

i. for any p ∈ Prop, a ⊧ p iff a ∈ V (p)
ii. a ⊧ A ∧ B iff a ⊧ A & a ⊧ B
iii. a ⊧ A ∨ B iff a ⊧ A or a ⊧ B
iv. a ⊧ A → B iff ∀b, c(Rabc & b ⊧ A ⇒ c ⊧ B)
v. a ⊧∼ A iff a^{∗} |̸= A
vi. a ⊧ □A iff ∀b(S_{□} ab ⇒ b ⊧ A)
vii. a ⊧ ◇A iff ∃b(S_{◇} ab & b ⊧ A).

We say that a formula A is valid in an R.C_{□◇} -frame ⟨O, W, R, S_{□} , S_{◇} ,^{∗} , u⟩ if a ⊧ A for every world a ∈ O in every R.C_{□◇} -model ⟨O, W, R, S_{□} , S_{◇} ,^{∗} , u, V ⟩. By the method of using canonical model, we can show that R.C_{□◇} is complete with respect to the class of all R.C_{□◇} -frames.

An R.C_{□◇} -frame in which all thorems of L are valid is called an L-frame. In general, any regular logic L over R is not necessary complete with respect to the class of all L-frames.

On the other hand, the Lindenbaum’s method guarantees completeness of any regular logic L over R in terms of L-matrices which are modal extensions of Font-Rodríguez’s R-matrices. With the idea of frames, we want to make L complete with respect to frames as well as matrices. Then we consider the restriction of valuation on an L-frame. For realizing this, we introduce the notion of general frames.

A general L-frame is an 8-tuple 𝔉 = ⟨O, W, R, S_{□} , S_{◇} ,^{∗} , u, P ⟩, where ⟨O, W, R, S_{□} , S_{◇} ,^{∗} , u⟩, written by κ𝔉, is an L-frame and P is called a set of possible values in 𝔉 (whose definitions are omitted in this paper).

The definition of L-models on general L-frames is the same as that on L-frames, except that V is a mapping from Prop to P. With the help of duality theory, we can see that any regular logic L over R is complete with respect to the class of all general L-frames.

We say that a general L-frame is called descriptive if it is isomorphic to its bidual. D denotes the class of descriptive L-frames and let κD = {κ𝔉 | 𝔉 ∈ D}. We put D^{⋆} = D ∪ κD. Then we say that

• L is D-complete (κD-complete) if A is a theorem of L whenever it is valid in every L-frame in D (in κD).

• L is D^{⋆}-elementary if there exists a set Φ of first-order sentences in the predicates O, R, S_{□} , S_{◇} , ^{∗} and the constant u such that for every 𝔉 ∈ D^{⋆}, 𝔉 is an L-frame iff 𝔉 satisfies each sentence in Φ.

Theorem 1 Let L be any regular logic over R. Then L is D-complete. Further, if L is D^{⋆}-elementary, then it is κD-complete.

3 A Sahlqvist theorem

In this section, we mention a Sahlqvist theorem for relevant modal logics. First of all, we give the definition of Sahlqvist formulas. Below, □^{n}A denotes \underbrace{□ ⋯ □}_{n} A.

• A modal formula A is positive if A contain only ∧, ∨, □ and ◇ as connectives.

• A modal formula of the form □^{m_{1}}p_{1}∧⋯∧□^{m_{k}}p_{k} with not necessarily distinct propositional variables p_{1}, ⋯, p_{k} is called a strongly positive formula.

• A given formula A is negative (in a regular logic L over R) if A is equivalent to ∼ B for a positive formula B in L.

• A modal formula A is untied (in L) if it can be constructed from negative formulas (in L) and strongly positive formulas using only ∧ and ◇.

• A modal formula A is Sahlqvist (in L) if it is equivalent in L to a conjunction of formulas of the form □^{k}(B → C), where k ≥ 0, B is untied in L and C is positive.

Theorem 2 Let L be regular logic over R. For any Sahlqvist formula A, there exists a first order sentence ϕ(a) in the predicates O, R, S_{□} , S_{◇} ,^{∗} and the constant u having a as its only free variable and such that the following holds for every L-frame 𝔉 ∈ D^{⋆} and every a ∈ W,

(𝔉, a) ⊧ A iff 𝔉 satisfies ϕ(a),

where (𝔉, a) ⊧ A means that a ⊧ A under any valuation on 𝔉.

Theorem 3 Let L_{0} be a D^{⋆}-elementary regular logic over R, and L be a logic obtained from L_{0} by adding a set of Sahlqvist formulas as axioms. Then L is D^{⋆}-elementary, and hence κD-complete.

We can see that Theorem 3 covers all completeness results of relevant modal logics in [2], [3] and [4]. Thus, we can apply Theorem 3 to any logic obtained from one of these logics by adding a set of Sahlqvist formulas as axioms.

Moreover, the classical modal logic K is a D^{⋆}-elementary extension of R.C_{□◇} . K is obtained from R.C_{□◇} by adding the axioms A → (B → A), □(A → B) → (□A → □B), ◇A ↔∼ □ ∼ A, and the rule of necessitation. In fact, to obtain frames for K, it suffices to add the frame postulates to those of general R.C_{□◇} -frames ⟨O, W, R, S_{□} , S_{◇} ,^{∗} , u, P ⟩ (see Section 5.5 of [5]), which can be represented by first order sentences in the predicates O, R, S_{□} , S_{◇} ,^{∗} and the constant u. As long as we neglect a element u, frames for K thus obtained are exactly usual Kripke frames for K. Therefore, Theorem 3 covers Sahlqvist theorem for classical modal logics.

References

[1] A.Chagrov and M.Zakharyaschev, Modal Logic, Clarendon Press, Oxford, 1997.

[2] A.Fuhrmann, ‘Models for relevant modal logics’, Studia Logica 49 (1990), 501-514.

[3] E.D.Mares, ‘The semantic completeness of RK’, Reports on Mathematical Logic 26 (1992), 3-10.

[4] E.D.Mares, ‘Classically complete modal relevant logics’, Mathematical Logic Quarterly 39 (1993), 165-177.

[5] R.Routley, V.Plumwood, R.K.Meyer and R.T.Brady, Relevant Logics and Their Rivals I, Ridgeview Publishing Company, Atascadero, 1982.

[6] H.Sahlqvist, ‘Completeness and correspondence in the first and second order semantics for modal logic’, in S.Kanger, editor, Proceedings of the third Scandinavian logic symposium, pages 110-143, North-Holland, Amsterdam, 1975.

[7] T.Seki, A Semantical Study of Relevant Modal Logics, PhD thesis, submitted, 2002.