Models for Normal Modal Logics over KR

Takahiro Seki

                            tseki@jaist.ac.jp

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

KR is the system of the logic excluding only ‘paradox of relevance’, which is one of paradoxes of material implication, in classical logic. In KR we can identify relevant negation with classical negation, so it is thought that KR is too closer system to classical logic. This paper examines this fact from a viewpoint introducing modal operator. In semantical study of relevant logic, Routley-Meyer semantics are often used and there are two kinds of models, the one is an unreduced model and the other is a reduced model. In general, there is a limit to apply a reduced model. So we consider when a reduced model can be used.

1 Unreduced Model

In this section, based on [4], we deal with the system of normal modal logics over KR (in below, we call them simply normal logics). And we will prove the completeness for them by using unreduced models.

First of all, we determine the language. The language is as follows: (i) propositional variables p, q, r, ⋯; (ii) logical connectives → (relevant implication), ∧ (and), ∨ (or) and ¬ (negation); (iii) modal operator □; and (iv) auxiliary symbols.

The formulas are defined by the usual way, and they are denoted by the capital letters A, B, C, ⋯ (possibly with subscripts). In below Wff, Prop denote the set of all formulas and that of all propositional variables, respectively, and capital Greeks Σ, Γ, Δ, ⋯ (possibly with prime) denote the non-empty sets of formulas.

First, we define the system KRN of the least normal logic. KRN is defined as follows:

(a) Abbreviation

◇A =^{ab} ¬□¬A

(b) Axioms (A1) A → A (A2) A → ((A → B) → B) (A3) (A → B) → ((B → C) → (A → C)) (A4) (A → (A → B)) → (A → B) (A5) A ∧ B → A (A6) A ∧ B → B (A7) (A → B) ∧ (A → C) → (A → B ∧ C) (A8) A → A ∨ B

(A9) B → A ∨ B
(A10) (A → C) ∧ (B → C) → (A ∨ B → C)
(A11) A ∧ (B ∨ C) → (A ∧ B) ∨ C
(A12) (A → ¬B) → (B → ¬A)
(A13) ¬¬A → A
(A14) A ∧ ¬A → B
(A15) □A ∧ □B → □(A ∧ B)
(A16) □(A → B) → (□A → □B)

(c) Rules of inference

\frac{A → B A}{B}(Modus Ponens)  \frac{A B}{A ∧ B} (Adjunction)  \frac{A}{□A}(Necessitation)

Now we define the typical systems of normal logics. Consider the systems obtained by adding the following formulas as axioms to KRN:

(A17) □A → ◇A ; (A18) □A → A ; (A19) □A → □□A  {(A20) A → □◇A \atop (A21) ◇A → □◇A}

We call the systems KRN.D, KRN.T, KRN.4, KRN.B and KRN.5 are obtained by adding (A17),(A18),(A19),(A20) and (A21) to KRN, respectively. We can combine more than two systems. For example, KRN.T4 is obtained by adding (A18) and (A19) to KRN, or by adding (A19) to KRN.T.

In below L denote any systems of normal logics. We write L ⊢ A if A is a theorem of L. Next we give the semantics of the systems of normal logics in terms of unreduced models, and prove

the soundness for them.

An (unreduced) KRN-frame is a quadruple ⟨O, W, R, S⟩ where (a) W is the set of all worlds, (b) O is the non-empty subset of W, (c) R is a ternary relation on W, and (d) S is a binary relarion on W.

A KRN-frame F = ⟨O, W, R, S⟩ satisfies the following postulates, for all a, b, c, d ∈ W:

(p1) ∃x(x ∈ O & Rxab) ⟺ a = b ; (p2) Raaa ; (p3) Rabc ⟹ Rbac & Racb  (p4) Rabe & Recd ⟹ ∃x(Racx & Rxbd) ; (p5) Rabd & Sdc ⟹ ∃x∃y(Sax & Sby & Rxyc) ; (p6) ∃x(x ∈ O & Sxa) ⟹ a ∈ O

(Unreduced) L-frames are KRN-frame ⟨O, W, R, S⟩ which satisfies adding postulates. Adding postulates are as follows, for all a, b, c ∈ W:

(p7) ∃x(Sax) ; (p8) Saa ; (p9) Sab & Sbc ⟹ Sac  {(p10) Sab ⟹ Sba \atop (p11) Sab & Sac ⟹ Sbc}

We call F a KRN.D-frame, KRN.T-frame, KRN.4-frame, KRN.B-frame and KRN.5-frame, if F is a KRN-frame satisfying the postulate (p7), (p8), (p9), (p10) and (p11), respectively. As in systems, we can combine some of distinct L-frames. For example, if a L-frame F holds postulates (p1) - (p6), (p8) and (p9), then F is called a KRN.T4-frame.

We call a quintuple ⟨O, W, R, S, v⟩ L-model on a frame ⟨O, W, R, S⟩ (in below, simply L-model), where ⟨O, W, R, S⟩ is a L-frame and v : Prop×W → {t, f} is called a valuation. For a given model ⟨O, W, R, S, v⟩, the relation a ⊧ A for a ∈ W and A ∈ Wff is defined inductively as follows:

i. for any p ∈ Prop, a ⊧ p iff v(p, a) = t

ii. a ⊧ A ∧ B iff a ⊧ A and a ⊧ B

iii. a ⊧ A ∨ B iff a ⊧ A or a ⊧ B

iv. a ⊧ A → B iff ∀x∀y(Raxy & x ⊧ A ⇒ y ⊧ B)
v. a ⊧ ¬A iff a |̸= A
vi. a ⊧ □A iff ∀x(Sax ⇒ x ⊧ A).

By the abbreviation and an interpretation defined above, a ⊧ ◇A iff ∃x(Sax & x ⊧ A). We say that A is L-valid, if x ⊧ A for every x ∈ O in any L-model ⟨O, W, R, S, v⟩.

Theorem 1 (Soundness of L) For any L, if A is a theorem of L, then A is L-valid.

Finally, we prove the completeness for the systems of normal logics. Basically we follows the method in section 4.6 of [8]. To prove the completeness, the following notions play a key role:

• Let Σ ≠ Wff and Δ ≠ Wff. Then (i) L ⊢ Σ → Δ iff there exist A_{1}, ⋯, A_{m} ∈ Σ(m > 0) and B_{1}, ⋯, B_{n} ∈ Δ(n > 0) such that L ⊢ A_{1} ∧ ⋯ ∧ A_{m} → B_{1} ∨ ⋯ ∨ B_{n}, and (ii) (Σ, Δ) is a L-pair iff (a) L ⊬ Σ → Δ and (b) Σ ∪ Δ = Wff.

• Σ is a L-theory iff (a) if A, B ∈ Σ then A ∧ B ∈ Σ and (b) if L ⊢ A → B and A ∈ Σ, then B ∈ Σ.

• Let Σ be a L-theory. Then (i) Σ is regular iff Σ contains all theorems of L, and (ii) Σ is maximal iff either A ∈ Σ or ¬A ∈ Σ and both do not hold for all A ∈ Wff

• Let Σ, Γ, Δ be L-theories. Then (i) RΣΓΔ iff if A → B ∈ Σ and A ∈ Γ then B ∈ Δ, and (ii) SΣΓ iff if □A ∈ Σ then A ∈ Γ.

Note that SΣΓ iff if A ∈ Γ then ◇A ∈ Σ.

To show the completeness, we see the unreduced case in [8], though there are slight differences in some terminologies and we must replace the part of ‘prime’ by ‘maximal’. Here we pick up the following lemma which does not appear in [8].

Lemma 2 If Σ is a maximal L-theory such that □C ∉ Σ, then there exist maximal L-theory Γ′ such that SΣΓ′ and C ∉ Γ′.

Then it is established that there exists a regular maximal L-theory Π such that A ∉ Π whenever L ⊬ A. Then we construct a canonical L-model ⟨O′, W′, R′, S′, v′⟩ as follows: (1) W′ is the set of all maximal L-theories; (2) O′ is the set of all regular maximal L-theories; (3) R′ is a ternary relation R restricted on W′; (4) S′ is a binary relation S restricted on W′; (5) v′ is defined by v′(p, Σ) = t iff p ∈ Σ, for all p ∈ Prop and Σ ∈ W′.

Theorem 3 (Completeness of L) If A is L-valid, then A is a theorem of L.

2 Reduced Model

In this section, we consider a reduced model. First we define the system KR4 in order to use a reduced model. The system KR4 is the corresponding system of modal logic over KR to NR in [7] or R4 in [5], which are the systems of modal logics over R. Though NR and R4 are different systems, adding A ∧ ¬A → B as an axiom to them, the result systems are equivalent.

KR4 is obtained from KRN.T4 by adding an axiom

(A□) if A is an axiom, then so is □A

instead of eleminating (Necessitation).

If A is a theorem of KR4, we write KR4 ⊢ A.

Next we consider a reduced model and give the semantics of KR4 and prove the soundness for it. A KR4-frame is a quadruple ⟨0, W_{r}, R_{r}, S_{r}⟩ where (a_{r}) W_{r} is the set of all worlds, (b_{r}) 0 ∈ W_{r} is

called a base world, (c_{r}) R_{r} is a ternary relation on W_{r}, and (d_{r}) S_{r} is a binary relation on W_{r}, and satisfies the following postulates, for all a, b, c, d ∈ W_{r}:

(pr1) ∃x(S_{r}0x & R_{r}xab) ⟺ a = b (pr2) R_{r}aaa (pr3) R_{r}abc ⟹ R_{r}acb (pr4) R_{r}abe & R_{r}ecd ⟹ ∃x(R_{r}acx & R_{r}xbd)

(pr5) R_{r}abd & S_{r}dc ⟹ ∃x∃y(S_{r}ax & S_{r}by & R_{r}xyc)
(pr6) S_{r}aa
(pr7) S_{r}ab & S_{r}bc ⟹ S_{r}ac

We call a quintuple ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩ KR4-model on a frame ⟨0, W_{r}, R_{r}, S_{r}⟩ (in below, simply KR4model), where ⟨0, W_{r}, R_{r}, S_{r}⟩ is a KR4-frame and v_{r} : Prop × W_{r} → {t, f} is called a valuation. For a given KR4-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩, the relation a ⊧ A for a ∈ W_{r} and A ∈ Wff is defined by the same way in section 1.

We say that A is KR4-valid, if 0 ⊧ A for all KR4-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩.

Theorem 4 (Soundness) If A is a theorem of KR4, then A is KR4-valid.

Finally we prove the completeness theorem for KR4. We prove it by using the style of [8] based on the argument in [7] or [5].

First we give several notions in order to prove the completeness theorem. Note that there are slight differences between in section 1 and in this section. The key notions are as follows.

• Let Σ ≠ Wff and Δ ≠ Wff. Then (i) KR4 ⊢ Σ → Δ iff there exist A_{1}, ⋯, A_{m} ∈ Σ(m > 0) and B_{1}, ⋯, B_{n} ∈ Δ(n > 0) such that KR4 ⊢ □(A_{1} ∧ ⋯ ∧ A_{m} → B_{1} ∨ ⋯ ∨ B_{n}), and (ii) (Σ, Δ) is a KR4-pair iff (a) KR4 ⊬ Σ → Δ and (b) Σ ∪ Δ = Wff.

• Σ is a KR4-theory iff (a) if A, B ∈ Σ then A ∧ B ∈ Σ and (b) if KR4 ⊢ □(A → B) and A ∈ Σ, then B ∈ Σ.

• Let Σ be a KR4-theory. Then (i) Σ is regular, iff Σ contains all theorems of KR4, and (ii) Σ is maximal, iff either A ∈ Σ or ¬A ∈ Σ and both do not hold for all A ∈ Wff.

Let Π be a regular maximal KR4-theory.

• Let Σ ≠ Wff and Δ ≠ Wff. Then (i) Π ⊢ Σ → Δ iff there exist A_{1}, ⋯, A_{m} ∈ Σ(m > 0) and B_{1}, ⋯, B_{n} ∈ Δ(n > 0) such that □(A_{1} ∧ ⋯ ∧ A_{m} → B_{1} ∨ ⋯ ∨ B_{n}) ∈ Π, and (ii) (Σ, Δ) is a Π-pair iff (a) Π ⊬ Σ → Δ and (b) Σ ∪ Δ = Wff.

• Σ is a Π-theory iff (a) if A, B ∈ Σ then A ∧ B ∈ Σ and (b) if □(A → B) ∈ Π and A ∈ Σ, then B ∈ Σ.

• A Π-theory Σ is maximal, iff either A ∈ Σ or ¬A ∈ Σ and both do not hold for all A ∈ Wff.

• Let Σ, Γ, Δ be Π-theories. Then (i) RΣΓΔ iff if A → B ∈ Σ and A ∈ Γ then B ∈ Δ, and (ii) SΣΓ iff if □A ∈ Σ then A ∈ Γ.

To show the completeness, we see the reduced case in [8], though there are slight differences in some terminologies and we must replace the part of ‘prime’ by ‘maximal’. Here we pick up the following lemma which does not appear in [8].

Lemma 5 If Σ is a maximal Π-theory such that □C ∉ Σ, then there exist maximal Π-theory Γ′ such that SΣΓ′ and C ∉ Γ′.

Then it is established that there exists a regular maximal KR4-theory Π such that A ∉ Π whenever KR4 ⊬ A. Using this Π, we construct a canonical model ⟨0′, W′_{r}, R′_{r}, S′_{r}, v′_{r}⟩ as follows: (1’) 0′ = Π; (2’) W′_{r} is the set of all maximal Π-theories; (3’) R′_{r} is a ternary relation R restricted on W′_{r}; (4’) S′_{r} is a binary relation S restricted on W′_{r}; (5’) v′_{r} is defined by v′_{r}(p, Σ) = t iff p ∈ Σ, for all p ∈ Prop and Σ ∈ W′_{r},

Theorem 6 (Completeness) If A is KR4-valid, then A is a theorem of KR4.

3 Unreduced Models and Reduced Models

In this section we consider the relationship between unreduced models, dealt with sections 1, and reduced models, dealt with section 2. Generally, unreduced models can be applied wider than reduced models. We shall see that unreduced models can be translated into reduced models in special case.

The following fact holds:

Lemma 7 For any A ∈ Wff, KRN.T4 ⊢ A iff KR4 ⊢ A.

Hence KR4 can be regarded the same system as KRN.T4, so KR4 is a normal logic. So a KR4frame can be said a (reduced) KRN.T4-frame.

As in [5], there is a way to construct an unreduced frame from a reduced frame in the argument of the soundness of R4. However, this method cannot be applied to the argument of the completeness. So we consider the generalized method to obtain an unreduced model from a reduced model.

In this paper, there is a reduced model only for KR4. We shall consider constructing an unreduced KR4-model from a reduced KR4-model. Note that an unreduced KR4-model can be identified an unreduced KRN.T4-model by Lemma 7.

There is most difference between the postulates (p1) and (p5) in an unreduced KRN.T4-frame and the postulates (p’1) in a reduced KR4-frame. Though (p3) and (p’3) are different, they can be identified because the postulate Rabc ⟹ Rbac can be derived in a KR4-frame. To construct an unreduced KRN.T4-model ⟨O, W, R, S, v⟩ from a reduced KR4-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩, we define a translation σ from a reduced KR4-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩ into an unreduced KRN.T4-model ⟨O, W, R, S, v⟩ as follows, for a, b, c ∈ W_{r}:

• W = {σ(x) | x ∈ W_{r}} • O = {σ(x) | S_{r}0x} • Rσ(a)σ(b)σ(c) iff R_{r}abc

• Sσ(a)σ(b) iff S_{r}ab

• v(p, σ(a)) = v_{r}(p, a), for all p ∈ Prop.

Lemma 8 ⟨O, W, R, S, v⟩ defined above is an unreduced KRN.T4-frame.

For the converse, there are some restrictions to make a reduced model. We can use a reduced model only if the system of the normal logic can be derived the following formula:

(A18) □A → A  and  (A19) □A → □□A.

L_{T4} denotes the system of normal logics in which (A18) and (A19) can be derived. For example, we can take KRN.T4 and KRN.T5 as L_{T4}.

Using L_{T4}, we can say as follows: for any L_{T4}, there is a reduced model for L_{T4}.

In order to construct a reduced L_{T4}-model from an unreduced L_{T4}-model, we introduce the translation τ from an unreduced L_{T4}-model ⟨O, W, R, S, v⟩ into a reduced L_{T4}-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩ as follows, for a, b, c ∈ W:

• W_{r} = {τ(x) | x ∈ W } • for all x ∈ O, τ(x) = 0 • R_{r}τ(a)τ(b)τ(c) iff Rabc

• S_{r}τ(a)τ(b) iff Sab
• v_{r}(p, τ(a)) = v(p, a), for all p ∈ Prop.

Lemma 9 ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩ defined above is L_{T4}-model.

Note that L_{T4} has (Necessitation) as the rule of inference. From Lemma 7 and Lemma 9, we show the method constructing a reduced L_{T4}-model from an unreduced L_{T4}-model as follows:

1. Eliminate (Necessitation) from L_{T4} and add the following axiom to axioms of L_{T4}:

if A is an axiom, then so is □A.

2. Construct a reduced L_{T4}-model ⟨0, W_{r}, R_{r}, S_{r}, v_{r}⟩ from an unreduced L_{T4}-model ⟨O, W, R, S, v⟩ by using the translation τ defined above.

When we enjoy the completeness by using a reduced L_{T4}-model, we should argue the same way as in section 2.

The argument in this section can be applied to normal logics over R. Therefore this fact give us the information about the relationship between an unreduced model, investigated in [4], and a reduced model, investigated in [7].

References

[1] A.R.Anderson and N.D.Belnap Jr., Entailment: The Logic of Relevance and Necessity, Vol.I, Princeton University Press, 1975.

[2] A.R.Anderson, N.D.Belnap Jr. and J.M.Dunn, Entailment: The Logic of Relevance and Necessity, Vol.II, Princeton University Press, 1992.

[3] B.F.Chellas, Modal Logic: an Introduction, Cambridge University Press, 1980.

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

[5] E.D.Mares and R.K.Meyer, ‘The semantics of R4’, Journal of Philosophical Logic 22, 1993, pp.95-110.

[6] R.K.Meyer and R.Routley, ‘Classical relevant logics I’, Studia Logica 32, 1973, pp.51-68.

[7] R.Routley and R.K.Meyer, ‘The semantics of entailment II’, Journal of Philosophical Logic 1, 1972, pp.53-73.

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