Marek Nasieniewski Andrzej Pietruszczak
A Method of Generating Modal Logics Defining Ja´ skowski’s Discussive Logic D2
Abstract. Ja´skowski’s discussive logic D2 was formulated with the help of the modal logic S5 as follows (see [7, 8]): A ∈ D2 iff ♦A• ∈ S5, where (−)• is a translation of discussive formulae from Ford into the modal language. We say that a modal logic L defines D2 iff D2 = {A ∈ Ford : ♦A• ∈ L}. In [14] and [10] were respectively presented the weakest normal and the weakest regular logic which (†): have the same theses beginning with ‘♦’ as S5. Of course, all logics fulfilling the above condition, define D2 . In [10] it was prowed that in the cases of logics closed under congruence the following holds: defining D2 is equivalent to having the property (†). In this paper we show that this equivalence holds also for all modal logics which are closed under replacement of tautological equivalents (rte-logics). We give a general method which, for any class of modal logics determined by a set of joint axioms and rules, generates in the given class the weakest logic having the property (†). Thus, for the class of all modal logics we obtain the weakest modal logic which owns this property. On the other hand, applying the method to various classes of modal logics: rte-logics, congruential, monotonic, regular and normal, we obtain the weakest in a given class logic defining D2 . Keywords: Ja´skowski’s discussive logic D2 , generating modal logics defining D2 .
1.
Introduction
The logic D2 is defined as a set of discussive formulae of a certain kind. These formulae are formed in the standard way from propositional letters: ‘p’, ‘q’, ‘p0 ’, ‘p1 ’, ‘p2 ’, . . . ; truth-value operators: ‘¬’ and ‘∨’ (negation and disjunction); discussive connectives: ‘∧d ’, ‘→d ’, ‘↔d ’ (conjunction, implication and equivalence); and brackets. Let Ford be the set of all these formulae. In Appendix A we recall some basic notions and chosen facts concerning modal logic. Let Form be the set of all modal formulae. The logic D2 was formulated with the help of the modal logic S5 as follows: D2 := { A ∈ Ford : ♦A• ∈ S5 } ,
Special Issue: The Legacy of Newton da Costa Edited by Daniele Mundici and Itala M. Loffredo D’Ottaviano
Studia Logica (2011) 97: 161–182 DOI: 10.1007/s11225-010-9302-2
© Springer 2010
162
M. Nasieniewski and A. Pietruszczak
where (−)• is a translation of discussive formulae into the modal language, i.e., the function −• from Ford into Form such that: 1. (a)• = a, for any propositional letter a, 2. for any A, B ∈ Ford : (a) (b) (c) (d) (e)
(¬ A)• = ¬ A• , (A ∨ B)• = A• ∨ B • , (A ∧ B)• = A• ∧ ♦B • , (A →d B)• = ♦A• → B • , (A ↔d B)• = (♦A• → B • ) ∧ ♦(♦B • → A• ).
We say that a modal logic L defines D2 iff D2 = {A ∈ Ford : ♦A• ∈ L}. It is known that also other modal logics define D2 . We see that while expressing logic D2 we refer to modal logics which (†): have the same theses beginning with ‘♦’ as S5. Let S5 be the set of all these logics, i.e., L ∈ S5
iff
∀A∈Form (♦A ∈ L ⇐⇒ ♦A ∈ S5).
It is obvious that: Fact 1.1. If L ∈ S5, then L defines D2 . Observe that for all rte-logics (i.e. logics closed under replacement of tautological equivalents) the following holds: defining of D2 is equivalent to having the property (†). Fact 1.2. For any rte-logic L: L defines D2 iff L ∈ S5.1 Proof. “⇒” Let L be any rte-logic defining D2 . We define a function (−)◦ from Form into Ford which “un-modalizes” every modal formula: 1. (a)◦ = a, for any propositional letter a, 2. for any A, B ∈ Form : (a) (b) (c) (d) 1
(¬ A)◦ = ¬ A◦ , (A ∨ B)◦ = A◦ ∨ B ◦ , (A ∧ B)◦ = ¬(¬ A◦ ∨ ¬ B ◦ ), (A → B)◦ = ¬ A◦ ∨ B ◦ ,
In [10] an analogous fact was proved in the case of modal logics which are closed under congruence rule. The proof given in the present paper is a slight modification of the proof of [10, Corollary 3.1].
A Method of Generating Modal Logics Defining D2
(e) (f) (g)
163
(A ↔ B)◦ = ¬(¬(¬ A◦ ∨ B ◦ ) ∨ ¬(¬ B ◦ ∨ A◦ )), (♦A)◦ = (p ∨ ¬ p) ∧d A◦ , (A)◦ = ¬ A◦ →d ¬(p ∨ ¬ p).
Notice that for any A, B ∈ Form we have the following equalities: (¬ A)◦• = ¬ A◦• , (A ∨ B)◦• = A◦• ∨ B ◦• , (A ∧ B)◦• = ¬(¬ A◦• ∨ ¬ B ◦• ), (A → B)◦• = ¬ A◦• ∨ B ◦• , (A ↔ B)◦• = ¬(¬(¬ A◦• ∨ B ◦• ) ∨ ¬(¬ B ◦• ∨ A◦• )), (♦A)◦• = (p ∨ ¬ p) ∧ ♦A◦• , (A)◦• = ♦ ¬ A◦• → ¬(p ∨ ¬ p). Moreover for any A, B ∈ Form , § ∈ {¬, ♦} and ∗ ∈ {∧, ∨, →, ↔} the following formulae belong to PL: (§A)◦• ↔ §A◦• ◦•
(A ∗ B)
◦•
(A)
◦•
() ◦•
↔ (A ∗ B ) ↔ ¬ ♦ ¬ A◦•
Therefore for any A, B, C ∈ Form : ◦•
C ↔ C[(§A) /§A◦• ] ∈ L , ◦•
C ↔ C[(A∗B) /(A◦• ∗B ◦• ) ] ∈ L , ◦•
C ↔ C[(A) /¬ ♦ ¬ A◦• ] ∈ L . Thus, for any formulae A1 , . . . , An , C we obtain: C ◦• ∈ L iff C[A1 /¬ ♦ ¬ A1 , . . . , An /¬ ♦ ¬ An ] ∈ L , since for every propositional letter a we have a◦• = a. Hence we get: C ◦• ∈ L iff C ∈ L ,
()
because we can replace every occurrence of ‘¬ ♦ ¬’ by ‘’ (see Remark 2, p. 177). Finally for any A ∈ Form we obtain: ♦A ∈ L iff (by ()) (♦A)◦• ∈ L iff (by ()) ♦A◦• ∈ L iff (since L defines D2 ) A◦ ∈ D2 iff ♦A◦• ∈ S5 iff (by () and ()) ♦A ∈ S5. So L ∈ S5.
164
M. Nasieniewski and A. Pietruszczak
The logic S4 belongs to S5 (see [6]). Thus, to define D2 one can use weaker than S5 modal logics. In [14] the smallest normal logic in S5 was indicated. This logic, denoted by S5M , was defined in [14] as the smallest normal logic containing (P),2 ♦(5) and ♦(T), and closed under the following rule:3 ♦♦A (cut ) ♦A Of course, since S5M ∈ S5, so S5M defines D2 , by Fact 1.2. Moreover, Fact 1.3 ([14, 10]). S5M is the smallest normal logic in S5; so S5M is the smallest normal logic defining D2 . In [10] it was observed that one can drop two out of the three axioms of the original formulation of S5M . In [11] it was also given another axiomatization of the logic S5M , having one specific axiom and a rule (cut ). In [3, 9] one can find axiomatizations without any specific rules, having two specific axioms, instead. Below we summarize these results. Fact 1.4 ([3, 9, 10, 11]). S5M is the smallest normal logic which: (i) contains ♦(T) and “semi-4” p → ♦p
(4s )
i.e. S5M = K4s ⊕ ♦(T); (ii) contains (5c ) and (4s ), i.e. S5M = K5c 4s ; (iii) contains ♦(T) and is closed under (cut ); ). (iv) contains (5c ) and is closed under (cut In [10] it was proved that while defining the logic D2 one can use a modal logic even weaker than S5M . It was shown that rS5M —the smallest regular logic defining D2 —is the regular version of the logic S5M in the axiomatization from Fact 1.4iii. Thus, we put: rS5M := the smallest regular logic containing ♦(T) that is closed under (cut ). We recall: 2
By Lemma A.9, in all regular logics (and so in normal ones) formulae (P) and (D) are equivalent. The smallest normal logic containing (D) (equivalently (P)) is denoted by ‘KD’ or simply by ‘D’. Thus, of course KD ⊆ S5M . 3 In [14, 10, 11, 13] this rule was denoted by ‘RM21 ’.
A Method of Generating Modal Logics Defining D2
165
Fact 1.5 ([10, 12]). (i) The logic rS5M is not normal. Thus, rS5M S5M . (ii) (D), (P) ∈ C5c rS5M . (iii) ♦(5) ∈ rS5M , so also ♦PL ⊆ rS5M . (iv) rS5M is the smallest regular logic in S5; so rS5M is the smallest regular logic defining D2 . In [11] other three axiomatizations of rS5M were given: two of them without the rule (cut ) and one containing that rule. Four mentioned axiomatizations of the logic rS5M are counterparts of four axiomatizations of the logic S5M recalled in Fact 1.4. These results are enclosed below. Fact 1.6 ([11]). rS5M is the smallest regular logic which: (i) contains ♦(T) and (4s ), i.e. rS5M = C4s ⊕ ♦(T); (ii) contains (5c ) and (4s ), i.e. rS5M = C5c 4s ; (iii) contains (5c ) and is closed under (cut ). It is obvious that: Fact 1.7 ([10]). For any modal logic L: if rS5M ⊆ L ⊆ S5, then L ∈ S5. The mutual location of modal logics connected to the logic D2 is summarized in Section 4. We will show that the logic S5 is an upper bound of all logics from S5 which are closed under congruence (cgr). Fact 1.8. If L is a congruential logic from S5, then L ⊆ S5.4 This fact follows from two lemmas below. Lemma 1.9. For any L ∈ S5: L ⊆ S5 iff L is closed under (poss-nec). Proof. Let L ∈ S5. “⇒” If A ∈ L ⊆ S5, then ♦A ∈ S5, by Lemma A.6. So also ♦A ∈ L. “⇐” If L is closed under (poss-nec) and A ∈ L, then ♦A ∈ L. So ♦A ∈ S5. Hence A ∈ S5, by Lemma A.6. Lemma 1.10. Every congruential logic from S5 is closed under (poss-nec). Proof. (PN) belongs to any congruential logic from S5, because (PN) ∈ S5, by Lemma A.6. So we use Lemma A.4. 4
In [3] (resp. [10]) was proved an analogical fact for normal (resp. regular) logics from S5 .
166
M. Nasieniewski and A. Pietruszczak
By facts 1.2 and 1.8 we have: Fact 1.11. If L is a congruential logic defining D2 then L ⊆ S5. Let X be a set of modal logics which are determined by some set AX of specific axioms and some set RX of specific rules, i.e. X is the set of all modal logics which include AX and are closed under all rules from RX . In the next section we give a general method which generates the weakest element in S5 ∩ X. Thus, for the set of all modal logics (AX = ∅ = RX ) we obtain the weakest logic in S5. Moreover, by Fact 1.2, if X consists of rte-logics, then the obtained weakest logic in S5 ∩ X is also the weakest logic in X defining D2 . In subsequent sections, we apply the method for the case of various sets of modal logics: rte-, cm-, congruential, monotonic, regular and normal logics.
2.
A general method of generating logics defining D2
For any Φ ⊆ Form let ♦Φ := {♦A : A ∈ Φ}, and for any rule R on Form we define the following rule R♦ on Form : R♦ := {♦A1 , . . . , ♦An , ♦B : A1 , . . . , An , B ∈ R} For any set of rules R on Form we put: R♦ := { R♦ : R ∈ R }. Since (sb)♦ ⊆ (sb) we obtain Lemma 2.1. All sets closed under (sb) are closed under (sb)♦ . So all modal logics are closed under (sb)♦ . Lemma 2.2. Let R be a rule such that S5 is closed under R. Then all logics from S5 are closed under the rule R♦ . Proof. Let L ∈ S5, ♦Ai , . . . , ♦An ∈ L and ♦Ai , . . . , ♦An , ♦B ∈ R♦ . Then ♦Ai , . . . , ♦An ∈ S5. Hence Ai , . . . , An ∈ S5, by Lemma A.6. Since Ai , . . . , An , B ∈ R and S5 is closed under R, so B ∈ S5. Therefore ♦B ∈ S5, again by Lemma A.6. Thus, also ♦B ∈ L. Corollary 2.3. All logics from S5 are closed under the rules (mp)♦ , ♦ (mon)♦ , (nec)♦ and (cut ) , i.e., they are closed, respectively, under the following rules: ♦A
♦(A → B) ♦B
♦(A → B) ♦(A → B)
♦A ♦A
♦♦♦A ♦♦A
A Method of Generating Modal Logics Defining D2
167
Proof. S5 is closed under (mp), (mon), (nec) and (cut ). Therefore, by Lemma 2.2, we obtain the required thesis. Now, we notice: Lemma 2.4. If L ∈ S5 and L ⊆ S5, then ♦L ⊆
S5.
Proof. Let L be any logic in S5. If ♦A ∈ ♦L then A ∈ L. By Lemma 1.9, L is closed under (poss-nec). Hence ♦A ∈ L ⊆ S5. So also ♦A ∈ L . Assume that A ⊆ Form and let R be a set of rules on Form . We say that the pair A, R is an axiomatization of a modal Logic L iff L is the smallest set including A, being closed under all rules from R. Then for any A ∈ Form : A ∈ L iff there exists a sequence A1 , . . . , An = A in which for any i n, either Ai ∈ A, or there are R ∈ R, m < n, j1 , . . . , jm < i such that Aj1 , . . . , Ajm , Ai ∈ R. Lemma 2.5. Let A, R be any axiomatization of a modal logic L. Let L∗ be any modal logic such that ♦A ⊆ L∗ and L∗ is closed under all rules from R♦ . Then ♦L ⊆ L∗ , i.e. for any A ∈ L: ♦A ∈ L∗ . Proof. Let A ∈ L. By the induction on the length of the proof, relative to the axiomatization A, R, we show that ♦A ∈ L∗ . Consider the case n = 1: we have that A1 ∈ A, so ♦A1 ∈ ♦A ⊆ L∗ . Assume that n > 1: If An ∈ A, then we reason as above. If Aj1 , . . . , Ajm , An ∈ R, for some R ∈ R, then by the inductive hypothesis we have ♦Aj1 , . . . , ♦Ajm ∈ L∗ . So ♦An ∈ L∗ , since by assumption L∗ is closed under the rule R♦. Theorem 2.6. Let L ∈ S5 and A, R be an axiomatization of L such that A ⊆ S5 and S5 is closed under all rules from R. Let L♦ be the smallest modal logic including ♦A and closed under all rules from R♦ and ♦♦A ♦A Then (i) L♦ ∈ S5, (ii) L♦ = S5; so L♦ is the smallest logic in S5.5 5
Notice that for any A and R, there is the logic L♦ .
(cut♦♦ ) ♦
168
M. Nasieniewski and A. Pietruszczak
Proof. First, we prove that L♦ ⊆ S5. Notice that S5 ⊆ S5, since S5 ∈ S5. So S5 = {L ∈ S5 : L ⊆ S5}. By Lemma 2.4, for any L ∈ S5 such that L ⊆ S5 we have ♦A ⊆ L . Moreover, by Lemma 2.2, L is closed under all rules from R♦ . Also L is closed under (cut♦♦ ), since ♦ by Lemma A.7, S5 is closed under this rule. Of course, also PL∪(rep ) ⊆ L and L is closed under the rules (mp) and (sb). So L♦ ⊆ L . (i) Since L♦ ⊆ L ⊆ S5, so if ♦A ∈ L♦ , then ♦A ∈ S5. Reversely, if ♦A ∈ S5, then ♦A ∈ L, so ♦♦A ∈ L♦ , by Lemma 2.5. Therefore, ), ♦A ∈ L♦ . Thus, L♦ ∈ S5. by the rule (cut♦♦ ♦ (ii) We have that L♦ ⊆ S5 ⊆ L♦ . The logic L♦ indicated in Theorem 2.6 is independent from the choice of a logic L and from its axiomatization. Using this theorem we can take for example any L such that rS5M ⊆ L ⊆ S5, and any its axiomatization.6 In each case we obtain the smallest logic in S5. Let us denote this logic by aS5M (“absolute” one). Thus—selecting for example the standard axiomatization of S5—we obtain that aS5M is the smallest modal logic which • includes the set ♦Taut, • contains the formulae ♦(df ♦), ♦(K), ♦(T) and ♦(5), ).7 • and is closed under the rules (mp)♦ , (nec)♦ and (cut♦♦ ♦ We also have the following widening of Theorem 2.6. Theorem 2.7. Let L ∈ S5 and L ∈ X, where X is a set of all modal logics including a given set of formulae AX and closed under all rules from some set RX . Let A, R be an axiomatization of L such that A ⊆ S5 and S5 is closed under all rules from R. Let L♦ X be the smallest modal logic including )}. Then AX ∪ ♦A and closed under all rules from RX ∪ R♦ ∪ {(cut♦♦ ♦ ∩ X, (i) L♦ X ∈ S5 ♦ = (S5 (ii) L♦ ∩ X); so LX is the smallest logic in S5 ∩ X. X Proof. As we observed, S5 ⊆ S5. So (S5 ∩ X) = {L ∈ S5 ∩ X : L ⊆ S5}. By Lemma 2.4, for any L from S5 ∩ X such that L ⊆ S5 we have ♦A ⊆ L , so also ♦AX ∪ PL ∪ (rep ) ⊆ L . Moreover, by 6
For any such logic which is additionally closed under (rep), one can take in its axiomatization just the axiom (df ♦) instead of the set of formulae (rep ). 7 In the axiomatization of the logic aS5M there is no need to use the rule (sb)♦ , since all logics are closed under the rule (sb) (see Lemma 2.1). Besides, let us notice that by Lemma 2.5, since (rep ) ⊆ S5, the logic aS5M includes the set ♦(rep ).
A Method of Generating Modal Logics Defining D2
169
assumption and lemmas A.7 and 2.2, L is closed under allrules from R♦ ∪ ♦ ), (mp), (sb)}. So L♦ (S5 ∩ X). RX ∪ {(cut♦♦ ♦ X ⊆ L . Hence LX ⊆ (i) As in the proof of Theorem 2.6, we obtain that L♦ X ∈ S5 ∩ X. ♦ ♦ (ii) We have LX ⊆ (S5 ∩ X) ⊆ LX . If in the above theorem X is for example the set of all regular logics, we can take as L logics S5, S5M or rS5M together with their axiomatizations recalled in Section 1. In each case we obtain the smallest logic in S5 ∩ X. Of course, if in Theorem 2.7, X is the set of all modal logics (AX = ♦ = aS5M . Moreover, by Fact 1.2, if all members ∅ = RX ), then L♦ X = L of X are rte-logics, then the obtained weakest logic in S5 ∩ X is also the weakest logic in X defining D2 . Thus, if X is the set of all congruential (resp. monotonic) modal logics, then L♦ X is the smallest congruential (resp. monotonic) logic defining D2 . Moreover, by Theorem 2.7 and Fact 1.3 (resp. Fact 1.5iii), if X is the set of all normal (resp. regular) logics, then S5♦ X = = the smallest regular the smallest normal logic in S5 = S5M (resp. S5♦ X logic in S5 = rS5M ).
3.
Simplifications of axiomatizations of generated logics
We apply Theorem 2.7 to give axiomatizations of the smallest logic defining D2 respectively in the set of rte-, cm-, congruential, monotonic, regular and normal logics. We will also show that one can drop from these axiomatizations some of axioms or rules. 3.1.
The case of rte-logics
If in Theorem 2.7, X is the set of all rte-logics, then we can assume that AX = (repPL ) and RX = ∅. We can take as L logics S5, S5M and rS5M , and any their axiomatizations. In each case we obtain the smallest rte-logic in S5, so also the smallest rte-logic defining D2 . Let us denote it by rteS5M . Further on by the standard axiomatization of the logic S5 we mean the collection consisting of axioms Taut, (df ♦), (K), (T) and (5), and rules (mp), (sb) and (nec). Now applying the standard axiomatization of S5 we obtain that rteS5M is the smallest rte-logic which • contains the formulae (PN), ♦(df ♦), ♦(K), ♦(T) and ♦(5), • and is closed under the rules (mp)♦ , (nec)♦ and (cut♦♦ ). ♦
170
M. Nasieniewski and A. Pietruszczak
Indeed, let L be the smallest rte-logic fulfilling the two above conditions. Then for any A ∈ PL: (PN) ↔ ♦A ∈ L, since (p → p) ↔ A ∈ PL. So ♦A ∈ L. Thus, ♦PL ⊆ L = rteS5M . Of course, taking other axiomatizations of S5 we can obtain different axiomatizations of rteS5M . Moreover, using logics S5M and rS5M , and their axiomatizations we can obtain further axiomatizations of rteS5M . Observe that Fact 3.1. The formula ¬ ♦ ¬ p → p
(∗)
does not belong to aS5M . So aS5M rteS5M . Proof. Let v be a valuation from Form into the set {0, 1} such that: v preserves classical truth conditions for classical constants; v(p) = 0; v(♦A) = 1 iff ♦A ∈ S5; and for any A, C ∈ Form : v(C) = v(C[¬ ¬ A /♦A ]).8 We prove that v(aS5M ) = {1}. We can consider aS5M as being axiomatized by PL, (rep ), ♦PL, all substitutions of formulae ♦(df ♦), ♦(K), ♦(T) and ♦(5), and ). It is easy to prove by induction on rules (mp), (mp)♦ , (nec)♦ and (cut♦♦ ♦ the length of the proof, relative to the chosen axiomatization, that all theses of aS5M are mapped by v on 1. We use the following facts (see lemmas A.6 and A.7): (i) for any axiom A, v(A) = 1; (ii) aS5M ⊆ S5; (iii) S5 is closed ); (iv) for rules (mp), (mp)♦ , (nec)♦ under (mp)♦ , (nec)♦ and (cut♦♦ ♦ ♦♦ and (cut♦ ): if all premisses are mapped on 1, then a conclusion is also mapped on 1. However v(♦ ¬ p) = 0, thus (∗) does not belong to aS5M . 3.2.
The case of cm-logics
If in Theorem 2.7, X is the set of all cm-logics, then we can assume that AX = (repPL ) ∪ {(K), (N)} and RX = ∅. We can again take as L, logics S5, S5M , and rS5M , together with their different axiomatizations. In each case we obtain the smallest cm-logic in S5, so also the smallest cm-logics defining D2 . We denote it by cmS5M . Notice that, selecting the standard axiomatization of S5, we have that cmS5M is the smallest cm-logic which • contains the formulae (PN), ♦(df ♦), ♦(K), ♦(T) and ♦(5), ). • and is closed under the rules (mp)♦ , (nec)♦ and (cut♦♦ ♦ For formulae having other forms one can take whatever as the value of v. However, / S5. by given restrictions we have that for any A ∈ Form : v( ¬ A) = 1 iff ♦A ∈ 8
A Method of Generating Modal Logics Defining D2
171
Observe that Fact 3.2. rteS5M has no thesis of the form B. So rteS5M cmS5M . Proof. Let v : Form −→ {0, 1} be a valuation which preserves classical truth conditions for classical constants, where for any A in Form : v(♦A) = 1 and v(A) = 0. We have that v(rteS5M ) = {1}. Indeed, we can consider rteS5M as being axiomatized by PL, (rep ), (repPL ), all substitutions of formulae (PN), ♦(df ♦), ♦(K), ♦(T) and ♦(5), and rules (mp), ). As in the proof of Fact 3.1, we show that all (mp)♦ , (nec)♦ and (cut♦♦ ♦ theses of rteS5M are mapped on 1 by v. Thus, B ∈ / rteS5M , for every B ∈ Form . 3.3.
The case of congruential logics
If in Theorem 2.7, X is the set of congruential logics, then we can assume that AX = ∅ and RX = {(cgr)}. Once again applying as L different logics and their axiomatizations we obtain the smallest congruential logic in S5, i.e., the smallest congruential logic defining D2 . This time we denote it by eS5M . If we take the standard axiomatization of S5 we obtain that eS5M is the smallest congruential logic which • contains ♦(K), ♦(T) and ♦(5) and (PN) (or ♦(df ♦)), • and is closed under rules (mp)♦ and (cut♦♦ ). ♦ Indeed, let L be the smallest congruential logic fulfilling the two above conditions. Since ‘p → p’, (df ♦) and (PN) (or ♦(df ♦)) belong to L, so by lemmas A.3 and A.4, L is closed under (poss-nec); so ♦PL ⊆ L and ♦(df ♦) ∈ L. Moreover, if ♦A ∈ L, then ♦♦A ∈ L, by (poss-nec). Hence, by ♦(5) and (mp)♦ , we obtain that ♦A ∈ L. So L is closed under (nec)♦ . Thus, L = eS5M . Of course, taking different axiomatizations of S5 one can obtain other axiomatizations of eS5M . Similarly using S5M and rS5M , and their formulations one can give further reformulations of eS5M . For example, eS5M is the smallest congruential logic which • contains ♦(K), ♦(4s ), ♦(5c ) and (PN) (or ♦(df ♦)), ). • and is closed under rules (mp)♦ , (mon)♦ and (cut♦♦ ♦ Fact 3.3. (i) eS5M has no thesis of the form B. Consequently, eS5M is not a cm-logic and cmS5M eS5M .
172
M. Nasieniewski and A. Pietruszczak
(ii) The formula ♦(p → p) ↔ (p → p)
(∗∗)
does not belong to cmS5M . Thus, the logics rteS5M and cmS5M are not congruential, eS5M cmS5M and rteS5M eS5M . Proof. (i) Taking in Theorem 2.7 L = rS5M (for AX = ∅ and RX = {(cgr)}), we obtain that eS5M ⊆ rS5M , but rS5M has no thesis of the form B (see [10]). (ii) Let v : Form −→ {0, 1} be a valuation which preserves classical truth conditions for classical constants, where for any A ∈ Form : 1 if A ∈ PL 0 if ¬ A ∈ PL v(A) = v(♦A) = 0 otherwise. 1 otherwise. We prove that v(cmS5M ) = {1}. We can consider cmS5M as being axiomatized by PL, (rep ), (repPL ), all substitutions of formulae (K), (N), (PN), ♦(df ♦), ♦(K), ♦(T) ). It is easy and ♦(5), and rules (mp), (mp)♦ , (nec)♦ and (cut♦♦ ♦ to prove by induction on the length of the proof, relative to the chosen axiomatization, that all theses of cmS5M are mapped on 1 by v. We use the following two facts: for any axiom A, v(A) = 1; for rules (mp), (mp)♦ , ): if all premisses are mapped on 1, then a conclusion is (nec)♦ and (cut♦♦ ♦ also mapped on 1. Thus, (∗∗) ∈ / cmS5M . However (∗∗) ∈ eS5M , since (PN) ↔ (p → p) M belongs to eS5 . Thus, eS5M cmS5M . Moreover, (∗∗) ∈ / rteS5M , since rteS5M ⊆ cmS5M . Therefore we have that rteS5M eS5M . 3.4.
The case of monotonic logics
If in Theorem 2.7, X is the set of monotonic logics, then we can assume that AX = ∅ and RX = {(mon)}. Once again taking as L different logics and their axiomatizations we always obtain the smallest monotonic logic in S5, i.e., the smallest monotonic logic defining D2 . We denote it by mS5M . We obtain that mS5M is the smallest monotonic logic which • contains ♦(K), ♦(T) and ♦(5), ). • and is closed under rules (mp)♦ and (cut♦♦ ♦ Indeed, let L be the smallest monotonic logic fulfilling the two above conditions. Then, by Lemma A.8, we obtain that (PN) ∈ L. Hence, by
A Method of Generating Modal Logics Defining D2
173
Lemma A.4, L is closed under (poss-nec); so ♦PL ⊆ L and ♦(df ♦) ∈ L. Besides, L is closed under (nec)♦ , as in the case of congruential logics. So L = mS5M . Taking different axiomatizations of S5, S5M and rS5M one can obtain other axiomatizations of mS5M . For example, mS5M is the smallest monotonic logic which contains ♦(K), ♦(4s ) and ♦(5c ), and is closed ). under rules (mp)♦ , (mon)♦ and (cut♦♦ ♦ Fact 3.4. The logic eS5M is not monotonic; so eS5M mS5M . Proof. Let v : Form −→ {0, 1} be a valuation which preserves classical truth conditions for classical constants and such that for any A in Form : ⎧ ⎧ ⎪ 1 if ♦A ∈ S5 ⎪ ⎨ ⎨0 if ♦ ¬ A ∈ S5 v(♦A) = 1 if ¬ A ∈ S5 v(A) = 0 if A ∈ S5 ⎪ ⎪ ⎩ ⎩ 0 otherwise. 1 otherwise. We prove that v(eS5M ) = {1}. We can consider eS5M as being axiomatized by PL, all substitutions of formulae (df ), (PN), ♦(K), ♦(T) and ♦(5), and rules (mp), ). We prove by induction on the length of the (cgr ), (mp)♦ and (cut♦♦ ♦ proof, relative to the chosen axiomatization, that all theses of eS5M are mapped by v on 1. We use the following facts (see lemmas A.6 and A.7): (i) for any axiom A, v(A) = 1; (ii) eS5M ⊆ S5; (iii) S5 is closed under (mp)♦ , ); (iv) for rules (mp), (mp)♦ , (cut♦♦ ) and (cgr ): if all (cgr ) and (cut♦♦ ♦ ♦ premisses are mapped on 1, then a conclusion is mapped on 1, too. Ad (iv), the case of (cgr ): Suppose that in a given proof C1 , . . . , Cn (for the chosen axiomatization) we obtain Cj = ♦A → ♦B from Ci = A ↔ B by (cgr ), for some i < j n and A, B ∈ Form . Then A ↔ B, ♦A → ♦B ∈ eS5M ⊆ S5. We show that v(♦A → ♦B) = 1. Indeed, if v(♦A) = 1, then either ♦A ∈ S5 or ¬ A ∈ S5. In the first case, ♦B ∈ S5; so v(♦B) = 1. In the second case, ¬ B ∈ S5, since ¬ A ↔ ¬ B ∈ S5. So also v(♦B) = 1. Now notice that (p ∧ ¬ p) → q ∈ Taut ⊆ eS5M , v(♦(p ∧ ¬ p)) = 1 and v(♦q) = 0. So v(♦(p ∧ ¬ p) → ♦q) = 0 and ♦(p ∧ ¬ p) → ♦q ∈ / eS5M . M Thus, eS5 is not monotonic. 3.5.
The case of regular logics
If in Theorem 2.7, X is the set of regular logics, AX = {(K)} and RX = {(mon)}, then we obtain the smallest regular logic in S5, i.e., the smallest regular logic defining D2 . We denote it by S5♦ r .
174
M. Nasieniewski and A. Pietruszczak
Notice that—for the standard axiomatization of S5—we obtain that S5♦ r is the smallest regular logic which • contains ♦(T) and ♦(5), ). • and is closed under rules (mp)♦ and (cut♦♦ ♦ Indeed, let L be the smallest regular logic fulfilling the two above conditions. Then, by Lemma A.8, we obtain that (PN) ∈ L. Hence, by Lemma A.4, L is closed under (poss-nec); so ♦PL ⊆ L and ♦(df ♦), ♦(K) ∈ L. Besides similarly as in the case of congruential logics, L is closed under (nec)♦ . So L = rS5M . M 9 By Theorem 2.7 and Fact 1.5iii we obtain that S5♦ r = rS5 . Fact 3.5. The formula ♦(p ∨ ¬ p) → (♦p ∨ ♦ ¬ p)
(+)
does not belong to mS5M . Thus, the logic mS5M is not regular ; thereofere mS5M rS5M . Proof. Let v : Form −→ {0, 1} be a valuation which preserves classical truth conditions for classical constants and such that for any A in Form : 1 if ♦A ∈ S5 0 if ♦ ¬ A ∈ S5 v(♦A) = v(A) = 0 otherwise. 1 otherwise. Similarly as in the proof of Fact 3.4 we show that v(mS5M ) = {1}. Now notice that v(♦(p∨¬ p)) = 1 and v(♦p) = 0 = v(♦ ¬ p). So v(+) = 0 and (+) ∈ / mS5M . Thus, mS5M is not regular. 3.6.
The case of normal logics
For X being the set of all normal logics, AX = {(K)} and RX = {(nec)}, applying Theorem 2.7 we obtain S5♦ n —the smallest normal logic in S5, i.e., the smallest normal logic defining D2 . For the standard axiomatization of S5—as in the case of regular logics— we obtain that S5♦ n is the smallest normal logic which • contains ♦(T) and ♦(5), Notice that in [10, pp. 202–203] it was proved that ♦(5) ∈ rS5M and rS5M is ); so S5♦ ⊆ rS5M . Of course, the reverse inclusion can closed under (mp)♦ and (cut♦♦ r ♦ be shown elementarily. 9
A Method of Generating Modal Logics Defining D2
175
). • and is closed under rules (mp)♦ and (cut♦♦ ♦ M By Theorem 2.7 and Fact 1.3 we have that S5♦ n = S5 . M As it was shown in [10, Fact 3.1] the logic rS5 is not normal; so rS5M S5M (see the proof of Fact 3.2).
4.
Summarization
To conclude our considerations it is useful to situate obtained logics among other modal logics connected with D2 (see Figure 1).10 We know that KD4 = K5c 4 and CD4 = C5c 4. Therefore since S5M (resp. rS5M ) is the smallest normal (resp. regular) logic containing (5c ) and closed under (cut ), thus M M KD4 (resp. CD4) is located above S5 (resp. rS5 ) As in [12], we also mention T∗ — the smallest normal logic containing (T) and ♦(5), and closed under (cut ) (see [14]). In [2, 3] it was proved that T∗ is the smallest normal logic which contains (T) and (4s ), i.e. T∗ = KT4s . Hence S5M is contained also in T∗. To draw Figure 1 we also use the following: / KD; so KD K4s and CD C4s . Fact 4.1 ([12]). (i) (4s ) ∈ (ii) ♦(T) ∈ / KD; so KD K ⊕ ♦(T) and CD C2 ⊕ ♦(T) . / K ⊕ ♦(T); so K ⊕ ♦(T) K5c and C2 ⊕ ♦(T) C5c . (iii) (5c ) ∈ / CT4s ; so CT4s CN1 T4s = CF ∩ KT4s and rS5M = C5c 4s (iv) (N1 ) ∈ CN1 5c 4s = CF ∩ S5M .
A.
Some facts from modal logic
As in [4] modal formulae are formed in the standard way from propositional letters: ‘p’, ‘q’, ‘p0 ’, ‘p1 ’, ‘p2 ’, . . . ; truth-value operators: ‘¬’, ‘∨’, ‘∧’, ‘→’, and ‘↔’ (connectives of negation, disjunction, conjunction, material implication and material equivalence, respectively); modal operators: the necessity sign ‘’ and the possibility sign ‘♦’; and brackets. By Form we denote the set of modal formulae. Of course, the set Form includes the set of all classical formulae (without ‘’ and ‘♦’); let Taut be the set of all classical tautologies. Besides, for any A, B, C ∈ Form , let C[A /B ] be any formula that results from C by replacing one or more occurrences of A, in C, by B. Modal logics are certain sets of formulae. As in [1, 5], we define a modal logic as any set L of modal formulae satisfying following conditions: 10
We want to expend a figure from [12], thus we need a recapitulation of facts presented elsewhere (also see [12]).
176
M. Nasieniewski and A. Pietruszczak S5
E5 (= CF ∩ S5)
KD45
S4
CD45(1) KD4
CT4 (= CF ∩ S4)
KT4s
CD4 S5M
CF ∩ KT4s
T CT4s CF ∩ S5M
K5c
CT M
rS5 K4s
C5c
K ⊕ ♦(T) M
mS5
C4s
C2 ⊕ ♦(T)
eS5M
cmS5M KD
rteS5M
CD
aS5M
Figure 1. Some known logics connected with D2 among chosen normal and regular logics.
• Taut ⊆ L, • L includes the following set of formulae
C[¬ ¬ A /♦A ] ↔ C : A, C ∈ Form
.
(rep )
• L is closed under the following two rules: modus ponens for ‘→’: A
A→B A
(mp)
A Method of Generating Modal Logics Defining D2
177
and uniform substitution:
A (sb) sA where s A is the result of uniform substitution of formulae for propositional letters in A.
Of course, by (sb), every modal logic includes the set PL of modal formulae which are instances of classical tautologies (i.e. instances of elements of Taut). Besides, the set (rep ) is closed on (sb). All members of a logic are called its theses. By (rep ), every modal logic has the following thesis: ♦p ↔ ¬ ¬ p (df ♦) Remark 1. In [1, 5] the symbol ‘♦’ is only an abbreviation of ‘¬ ¬’. In the present paper ‘♦’ is a primary symbol, thus we have to add the set of axioms (rep ). The use of this set corresponds to the applying of formula (df ♦) as a definition together with the definitional rule. Formulae from (rep ) allow to replace one or more occurrences of ‘¬ ¬’ with ‘♦’ and vice versa. Lemma A.1. A modal logic contains the formula: p → p
(T)
p → ♦p
(T )
iff it contains its dual version:
We say that a modal logic L is rte-logic iff L is closed under replacement of tautological equivalents, i.e., for any A, B, C ∈ Form if A ↔ B ∈ PL and C ∈ L, then C[A /B ] ∈ L.
(rte)
A modal logic is rte-logic iff it includes the following set
C[A /B ] ↔ C : A, B, C ∈ Form and A ↔ B ∈ PL .
(repPL )
Similarly as in the case of (rep ) also (repPL ) is closed on (sb). Remark 2. In any thesis of any rte-logic we can replace one or more occurrences of ‘¬ ¬’ (resp. ‘ ¬’, ‘¬ ’, ‘¬ ♦ ¬’, ‘¬ ♦’, ‘♦ ¬’) by ‘♦’ (resp. ‘¬ ♦’, ‘♦ ¬’,‘’, ‘ ¬’, ‘¬ ’) and vice versa. Thus, every rte-logic has the following thesis p ↔ ¬ ♦ ¬ p (df )
178
M. Nasieniewski and A. Pietruszczak
Lemma A.2. A rte-logic contains the following formulae: (p → q) → (p → q)
(K)
(p ∧ q) ↔ (p ∧ q)
(R)
p → p
(4)
♦p → p
(B)
♦p → p
(5)
p → ♦p
(5c )
iff it contains, respectively, theirs dual versions: (p → q) → (♦p → ♦q)
(K )
♦(p ∨ q) ↔ (♦p ∨ ♦q)
(R )
♦♦p → ♦p
(4 )
p → ♦p
(B )
♦p → ♦p
(5 )
♦p → ♦p
(5c )
In [1] a modal logic is called classical modal 11 (cm-logic for short) iff it is rte-logic which contains (K) and (p → p)
(N)
Thus, all cm-logics include the set PL := {T : T ∈ PL}. We say that a modal logic is congruential iff it is closed under the congruence rule A↔B (cgr) A ↔ B A modal logic is congruential iff it is closed under replacement A↔B ↔C
C[A /B ]
(rep)
iff it is closed under the following rule A↔B A → B 11
(cgr )
In [10, 11, 13], following a custom from [4], the expression ‘classical modal’ was referred to congruential logics (please see further).
A Method of Generating Modal Logics Defining D2
179
iff it contains (df ) and is closed under the following rule A↔B ♦A → ♦B
(cgr )
Of course, every modal logic closed under (rep) is also closed under (repPL ), so every congruential logic is rte-logic. Besides (N), we use the following formulae ♦(p → p)
(P)
♦(p → p)
(PN)
Lemma A.3. For any congruential logic L the following conditions are equivalent: (a) L has a pair of theses of the form B and B (resp. ♦B, ♦B), (b) L has a thesis of the form T (resp. ♦T , ♦T ), where T ∈ PL, (c) L contains (N) (resp. (P), (PN)). Lemma A.4. If a congruential logic contains (N) (resp. (P), (PN)), then it is closed under the necessity (resp. possibility, possibility-necessity) rule: A A A ♦A A ♦A
(nec) (poss) (poss-nec)
Lemma A.5. If a congruential logic has theses (5) and either • a theses of the form ♦B, or • (T), then it closed under the rule (nec). It is known (cf. e.g. [4]) that while defining congruential logics one uses (df ♦) instead of (rep ), i.e., treats them as subsets of Form which contain Taut and (df ♦), that are closed under rules (mp), (sb) and (cgr).12 We can also consider quite week modal logics in which we use (df ♦) instead of (rep ). In some logics the symbol ‘♦’ has not to behave as an abbreviation of ‘¬ ¬’, although we can have there the thesis (df ) (cf. remarks 1 and 2). For example, the formula ‘♦p ↔ ¬ ¬ p’ has not to be a thesis of such logics. 12
180
M. Nasieniewski and A. Pietruszczak
Lemma A.6. Let L be any modal logic closed under (nec), containing (T) and (5). Then for any A ∈ Form : A ∈ L iff ♦A ∈ L. Lemma A.7. Let L be any modal logic containing (T), (5), (5 ), (4) and (4 ). Then for any sequences of modal operators M and M , and any A ∈ Form : M♦A ∈ L iff ♦A ∈ L iff M ♦A ∈ L. We say that a modal logic is monotonic iff it is closed under the monotonicity rule: A→B (mon) A → B A modal logic is monotonic iff it contains (df ) and is closed under the dual form of (mon): A→B (mon ) ♦A → ♦B Every monotonic logic is closed under (rep). Lemma A.8. For any monotonic logic the following conditions are equivalent: (a) it has at least one thesis of the form B (resp. ♦B, ♦B), (b) it contains (N) (resp. (P), (PN)). We say that a modal logic is regular iff it is closed under the regularity rule: A∧B→C (reg) A ∧ B → C A modal logic is regular iff it contains (K) and is closed under (mon) iff it contains (R) and is closed under (cgr). Every regular logic has the theses (R ) and ♦(p → q) ↔ (p → ♦q) (R♦ ) By (R♦ ) we obtain Lemma A.9. For any regular logic the following conditions are equivalent: (a) it has at least one thesis of the form ♦B, (b) it contains (P), (c) it contains the following formula p → ♦p
(D)
A Method of Generating Modal Logics Defining D2
181
A modal logic is normal iff it contains (K) and is closed under (nec) iff it is regular and contains (N) iff it contains (N) and (K) and is closed under (cgr). Thus, all normal logics are cm-logics. Let K (resp. C2) be the smallest normal (resp. regular) modal logic. Using names of the above formulae, to simplify notation of normal logics we apply the Lemmon code KX1 . . . Xn (resp. CX1 . . . Xn ) to denote the smallest normal (resp. regular) logic containing the formulae (X1 ), . . . , (Xn ) (see [1, 4, 15]). Besides, let for any formula A ∈ Form , KX1 . . . Xn ⊕ A (resp. CX1 . . . Xn ⊕ A) be the smallest normal (resp. regular) logic which includes KX1 . . . Xn (resp. CX1 . . . Xn ) and contains A. We will use a formula ♦(p ∧ ¬ p) (F) The regular logic CF is called falsum. We have ♦A ∈ CF, for any A ∈ Form . We standardly put T := KT, S4 := KT4 and S5 := KT5 = KT4B = KD4B = KD5B. As it is known, T S4 S5, CD5 = KD5, CD45 = KD45 and CT5 = KT5 =: S5. Thus, to avoid “normalization” of regular logics one have to use some special formulae. We adopt a convention from [15, p. 206] and for any formula (X) we put (X(1)) := (p → p) → (X). Notice that in all monotonic logics, any formula of the form A → B is equivalent to (p → p) → (A → B). Thus, the formulae (T), (D), (4) and (5c ) are equivalent on the basis of every monotonic logic respectively to (T(1)), (D(1)), (4(1)) and (5c (1)). Lemma A.10 ([15, vol. II, ch. IV, Corollary 2.4]). CN1 X1 (1) . . . Xn (1) = CF ∩ KX1 . . . Xn , where (p → p) → (p → p)
(N1 )
In [15] Segerberg puts E5 := CN1 T4B(1). So E5 = CF∩KT4B = CF∩S5, by Lemma A.10. Notice that E5 = CT4B(1), since (N1 ) is an instance of (4). We have also E5 = CN1 T5(1) and E5 = CF ∩ KT4B = CF ∩ KD4B = CD4B(1).13 Moreover, notice that CD45(1) = CN1 D45(1) = CF ∩ KD45. References [1] Bull, R. A., and K. Segerberg, ‘Basic modal logic’, in M. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, vol. II, D. D. Reidel Publishing Company, Dordrecht, 1984, pp. 1–88. 13
In [15] Segerberg also puts D5 := CN1 D4B(1) = CD4B(1). So we have D5 = E5.
182
M. Nasieniewski and A. Pietruszczak
[2] Blaszczuk, J. J., and W. Dziobiak, ‘Remarks on Perzanowski’s modal system’, Bulletin of the Section of Logic 4: 57–64, 1975. [3] Blaszczuk, J. J., and W. Dziobiak, ‘Modal logics connected with systems S4n of Soboci´ nski’, Studia Logica 36: 151–175, 1977. [4] Chellas, B. F., Modal Logic. An Introduction, Cambridge University Press, Cambridge, 1980. [5] Chellas, B. F., and K. Segerberg, ‘Modal logics in the vicinity of S1’, Notre Dame Journal of Formal Logic 37: 1–24, 1996. [6] Furmanowski, T., ‘Remarks on discussive propositional calculus’, Studia Logica 34: 39–43, 1975. [7] Ja´skowski, S., ‘Rachunek zda´ n dla system´ ow dedukcyjnych sprzecznych’, Studia Societatis Scientiarum Torunensis, Sect. A, I(5): 57–77, 1948. The first English version: ‘Propositional calculus for contradictory deductive systems’, Studia Logica 24: 143– 157, 1969. The second English version: ‘A propositional calculus for inconsistent deductive systems’, Logic and Logical Philosophy 7: 35–56, 1999. [8] Ja´skowski, S., ‘O koniunkcji dyskusyjnej w rachunku zda´ n dla system´ ow dedukcyjnych sprzecznych’, Studia Societatis Scientiarum Torunensis, Sect. A, I(8): 171– 172, 1949. The English version: ‘On the discussive conjunction in the propositional calculus for inconsistent deductive systems’, Logic and Logical Philosophy 7: 57–59, 1999. [9] Nasieniewski, M., ‘A comparison of two approaches to parainconsistency: Flemish and Polish’, Logic and Logical Philosophy 9: 47–74, 2002. [10] Nasieniewski, M., and A. Pietruszczak, ‘The weakest regular modal logic defining Ja´skowski’s logic D2 ’, Bulletin of the Section of Logic 37(3/4): 197–210, 2008. [11] Nasieniewski, M., and A. Pietruszczak, ‘New axiomatizations of the weakest regular modal logic defining Ja´skowski’s logic D2 ’, Bulletin of the Section of Logic 38(1/2): 45–50, 2009. [12] Nasieniewski, M., and A. Pietruszczak, ‘Semantics for regular logics connected with Ja´skowski’s discussive logic D2 ’, Bulletin of the Section of Logic 38(3/4): 173– 187, 2009. [13] Nasieniewski, M., and A. Pietruszczak, ‘On modal logics defining Ja´skowski’s D2 -consequence’. Accepted for the publication in the collection of papers presented during the Fourth World Congress of Paraconsistency, Melbourne, July 13–18, 2008. [14] Perzanowski, J., ‘On M-fragments and L-fragments of normal modal propositional logics’, Reports on Mathematical Logic 5: 63–72, 1975. [15] Segerberg, K., An Essay in Classical Modal Logic, vol. I and vol. II, Uppsala 1971.
Marek Nasieniewski and Andrzej Pietruszczak Department of Logic Nicolaus Copernicus University ul. Asnyka 2, 87-100 Toru´ n, Poland {mnasien,pietrusz}@uni.torun.pl