On Modal Logics Defining Jaśkowski’s D₂-Consequence

Abstract

Jaśkowski’s logic D ₂ (as a set of formulae) was formulated with the help of the modal logic S5 (see Jaśkowski, Stud Soc Sci Torun I(5):57–77, 1948; Stud Soc Sci Torun I(8):171–172, 1949). In Furmanowski (Stud Log 34:39–43, 1975), Perzanowski (Rep Math Log 5:63–72, 1975), Nasieniewski and Pietruszczak (Bull Sect Logic 37(3–4):197–210, 2008) it was shown that to define D ₂ one can use normal and regular logics weaker than S5. In his paper Jaśkowski used a deducibility relation which we will denote by⊢ _{D 2} and which fulfilled the following condition: A ₁,…,A _n ⊢; _{D 2} B iff $\ulcorner \lozenge {A}_{1}^{\bullet }\rightarrow (\ldots \rightarrow (\lozenge {A}_{n}^{\bullet }\rightarrow \lozenge {B}^{\bullet })\ldots \,)\urcorner \in \mathbf{S5}$, where (−)^∙ is a translation of discussive formulae into the modal language. We indicate the weakest normal and the weakest regular modal logic which define D ₂ -consequence.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

The basic features of notions of deductive and deductive discussive systems used by Jaśkowski are as follows (see Jaśkowski 1948, p. 61 and Jaśkowski 1999, pp. 37–38).

• By theses of a deductive system Jaśkowski meant all expressions asserted within it, i.e. axioms and theorems deduced from them or proved in a specific way for a given system.

• A deductive system is based on a certain logic iff the set of its theses is closed under modus ponens rule with respect to theorems of the logic.

• A deductive system is overcomplete iff the set of its theses is equal to the set of all meaningful expressions of the language.

• A deductive system is inconsistent iff among its theses there are two theses such that one of them is the negation of the other.

• Usually, theses of a deductive system are formally expressed theorems of some consistent theory.

• If there is no assumption that theses of a deductive system express opinions which do not contradict each other, then such a system is called discussive.

Jaśkowski’s aim was to formulate a logic, which when applied to inconsistent systems would not generally entail overcompleteness.

Jaśkowski gave an example of the way in which theses of discussive systems can be generated by referring to a discussion. Decisive for such a choice was the fact that during a discussion inconsistent voices can appear, however, we are not inclined to deduce every thesis from them.

One can treat voices appearing explicitly in the discussion as preceded by the following restriction: “according to the opinion of one of the participants of the discussion”, which formally one can express by preceding the given statement with: ‘it is possible that’. If we take a position of an external observer (i.e. someone that does not take part in a discussion) all voices appearing in a discussion are only possible. It is so, since a person who is not involved in the discussion has every right to treat particular voices in disbelief or to dissociate from discussants’ statements. For the same reason, also conclusions following from explicitly expressed statements in a discussion are only possible. Conclusions one can treat as implicitly included into a discussion, since a given discussion consists not only of voices explicitly expressed, but also statements concluded from them. Summarizing, explicit voices, as well as their conclusions, are treated as theses of a discussive system.

Since the above pattern requires use of a modal language, one has to choose some specific modal logic. Jaśkowski himself chose the logic S5.

It is obvious that one needs to consider the language of full sentential logic, since otherwise one would have to treat all sentences as atomic ones, and it would not be possible to analyze logical deducibility based on the meaning of logical sentential constants.

In the present paper, ‘p’ and ‘q’ are propositional letters, used to built formulae (both discussive and modal). Capital Latin letters ‘A’, ‘B’ and ‘C’ (with or without subscripts) are metavariables for formulae, a Greek letter ‘Π’ is a metavariable for sets of formulae, while small Latin latter ‘a’ is a metavariable for propositional letters. Besides, following Jaśkowski’s custom, Gothic letters are used to denote instances of concrete sentences of the natural language.

Jaśkowski observed that while formulating a discussive system one can not treat the implication ‘ → ’ as a material one, since sets of theses of discussive systems would not be closed under the modus ponens rule:

$$\frac{{ \mathfrak{P}\rightarrow \mathfrak{Q} \atop \mathfrak{P}} } {\mathfrak{Q}}$$

[…] out of the two theses one of which is

$$\mathfrak{P} \rightarrow \mathfrak{Q}\,,$$

and thus states: “it is possible that if $\mathfrak{P}$, then $\mathfrak{Q}$”, and the other is

$$\mathfrak{P}\,,$$

and thus states: “it is possible that $\mathfrak{P}$”, it does not follow that “it is possible that $\mathfrak{Q}$”, so that the thesis

$$\mathfrak{Q}\,,$$

does not follow intuitively, as the rule of modus ponens requires. (Jaśkowski 1999, p. 43, see also Jaśkowski 1948, p. 66)

Jaśkowski meant that the formula:

$$\lozenge (p \rightarrow q) \rightarrow (\lozenge p \rightarrow \lozenge q)$$

is not a thesis of S5. Thus, not for all sentences $\mathfrak{P}$ and $\mathfrak{Q}$, the following sentence

$$\lozenge (\mathfrak{P} \rightarrow \mathfrak{Q}) \rightarrow (\lozenge \mathfrak{P} \rightarrow \lozenge \mathfrak{Q})$$

is a substitution of a logical thesis.

As an appropriate implication to be used in the formulation of a discussive logic Jaśkowski chose a discussive one. We will denote it by ‘ → ^d’. In the formal language Jaśkowski defined a formula

$$p{\rightarrow }^{\mathrm{d}}q$$

by

$$\lozenge p \rightarrow q\,.$$

Jaśkowski intuitively understood it in the following way: “if anyone states that p, then q” (Jaśkowski 1999, p. 44, see also Jaśkowski 1948, p. 67).

In the same frgment, Jaśkowski pointed to the fact that:

In every discussive system two theses, one of the form:

$$\mathfrak{P}{\rightarrow }^{\mathrm{d}}\mathfrak{Q}\,,$$

and the other of the form:

$$\mathfrak{P}\,,$$

entail the thesis

$$\mathfrak{Q}\,,$$

and that on the strength of the theorem

$$\lozenge (\lozenge p \rightarrow q) \rightarrow (\lozenge p \rightarrow \lozenge q). $$

(M2 1)

Thus, such an understanding of the implication ensures that sets of theses of deductive systems are closed under the modus ponens rule.

A discussive equivalence (notation: ‘p ↔ ^d q’) Jaśkowski defined as:

$$(\lozenge p \rightarrow q) \wedge (\lozenge q \rightarrow \lozenge p).$$

In Jaśkowski (1948), (see also Jaśkowski (1969)), three classical connectives are used: negation (‘ ¬’), disjunction (‘ ∨ ’) and conjunction (‘ ∧ ’). Moreover, a discussive conjunction ‘ ∧ ^​d’, was introduced in Jaśkowski (1949). Any sentence of the form ‘p ∧ ^​d q’ expresses a statement: “p and it is possible that q”, i.e. formally: ‘p ∧ ◊ q’. Notice that in Jaśkowski (1949) the classical conjunction was not dropped from the language of discussive systems.

Dwuwartościowy dyskusyjny rachunek zdań oznaczony jako D₂ można wzbogacić definiuja̧c koniunkcjȩ dyskusyjna̧ Kd. [In English: The two-valued discussive propositional calculus denoted as D₂ can be enriched with a definition of the discussive conjunction ∧ ^​d]. (Jaśkowski 1949, p. 171, Jaśkowski (1999a), p. 57)

The question arises: what is the natural interpretation of the classical conjunction in the context of discussive systems? It seems that the classical conjunction can be used to “glue” particular statements of a given participant of the discussion. For example, if a given participant expresses two statements $\mathfrak{P}$ and $\mathfrak{Q}$ then she/he asserts $\ulcorner \mathfrak{P} \wedge \mathfrak{Q}\urcorner$, i.e. taking the external point of view we have in the modal language $\ulcorner \lozenge ({\mathfrak{P}}^{\bullet }\wedge {\mathfrak{Q}}^{\bullet })\urcorner$, where ( − )^∙ is the appropriate translation of discussive connectives which can appear within $\mathfrak{P}$ and $\mathfrak{Q}$. On the other hand discussive conjunction is usually meant as a tool adequate to express the status of a given discussion from the point of view of a given participant of the discussion. Thus, if we have assertions $\mathfrak{P}$ and $\mathfrak{Q}$ made by two participants, then the appearance of these two statements—taking the point of view of the first participant—can be expressed as follows: $\ulcorner \mathfrak{P}{\wedge }^{\!\mathrm{d}}\mathfrak{Q}\urcorner$. From the external point of view such a statement becomes $\ulcorner \lozenge ({\mathfrak{P}}^{\bullet }\wedge \lozenge {\mathfrak{Q}}^{\bullet })\urcorner$, which in the logic S5 is equivalent to $\ulcorner \lozenge {\mathfrak{P}}^{\bullet }\wedge \lozenge {\mathfrak{Q}}^{\bullet }\urcorner$. We obtain the same formula if we start with the consideration of the point of view of the second participant. Indeed, we have the discussive record of the discussion from the point of view of the second participant: $\ulcorner \mathfrak{Q}{\wedge }^{\!\mathrm{d}}\mathfrak{P}\urcorner$, while the external point of view of this statement becomes: $\ulcorner \lozenge ({\mathfrak{Q}}^{\bullet }\wedge \lozenge {\mathfrak{P}}^{\bullet })\urcorner$, equivalently on the basis of S5 we have $\ulcorner \lozenge {\mathfrak{Q}}^{\bullet }\wedge \lozenge {\mathfrak{P}}^{\bullet }\urcorner$.

Of course we are not interested only in the < < external description > > of a given discussion, but also whether $\mathfrak{Q}$ discussively follows from given statements ${\mathfrak{P}}_{1},\ldots ,{\mathfrak{P}}_{n}$ of n participants (n > 0). Using modal translations and the usual understanding of deduction in modal logics we inquire whether the following statements (equivalent by the positive logic):

• (a) $(\lozenge {\mathfrak{P}}_{1}^{\bullet }\wedge \cdots \wedge \lozenge {\mathfrak{P}}_{n}^{\bullet }) \rightarrow \lozenge {\mathfrak{Q}}^{\bullet }$,

• (b) $\lozenge {\mathfrak{P}}_{1}^{\bullet }\rightarrow (\ldots \rightarrow (\lozenge {\mathfrak{P}}_{n}^{\bullet }\rightarrow \lozenge {\mathfrak{Q}}^{\bullet })\ldots )$

are valid in S5.¹ Equivalently we can look into the problem of validity of the following sentences in the discussive logic:

• (a)d $({\mathfrak{P}}_{1}{\wedge }^{\!\mathrm{d}}\cdots {\wedge }^{\!\mathrm{d}}{\mathfrak{P}}_{n}){\rightarrow }^{\mathrm{d}}\mathfrak{Q}$,

• (b)d ${\mathfrak{P}}_{1}{\rightarrow }^{\mathrm{d}}(\ldots {\rightarrow }^{\mathrm{d}}({\mathfrak{P}}_{n}{\rightarrow }^{\mathrm{d}}\mathfrak{Q})\ldots )$.²

In both cases (a)^d and (b)^d—using the logic S5—we obtain the equivalent translations of sentences into the modal language. We have to remember that in the case of validity in the discussive logic the translation obtained has to be preceded by ‘ ◊ ’, since from the point of view of an external observer the sentences (a)^d and (b)^d are only possible. Thus indeed (a) and (b) are the modal counterparts of (a)^d and (b)^d, respectively.

As it is known the formula (a), resp. (b), is valid in S5 iff there is a finite sequence beginning with sentences $\ulcorner \lozenge {\mathfrak{P}}_{1}^{\bullet }\urcorner ,\ldots ,\ulcorner \lozenge {\mathfrak{P}}_{n}^{\bullet }\urcorner$, and ending with $\ulcorner \lozenge {\mathfrak{Q}}^{\bullet }\urcorner$, where the other elements (as well as $\ulcorner \lozenge {\mathfrak{Q}}^{\bullet }\urcorner$) are either theses of S5 and/or are sentences obtained from some sentences preceding in the sequence obtained by modus ponens.

The main aim of our paper is to find the smallest normal logic and the smallest regular logic which could be used instead of S5. For these logics it is not enough to have the same theses beginning with ‘ ◊ ’ as S5; since we consider here the discussive deducibility relation, thus these logics have to include also (M2 1).

Remark

In the case of a sentence of the form (a), resp. (b), for n = 0 we only try to find out whether a wanted logic has the same thesis beginning with ‘ ◊ ’. This problem has already been solved in the case of normal and regular classes of logics (Furmanowski 1975; Perzanowski 1975; Nasieniewski and Pietruszczak 2008). □ 

Nowadays in the considerations concerning the logic D ₂ the classical conjunction is usually omitted. It is justified by the functional completeness obtained by classical connectives of ‘ ¬’ and ‘ ∨ ’. Thus, we also do not include the classical conjunction in the discussive language.

2 Basic Notions

Let For^d be the set of all formulae of the discussive language with constants: ‘ ¬’, ‘ ∨ ’, ‘ ∧ ^​d’, ‘ → ^d’, and ‘ ↔ ^d’. Let For_m be the set of all modal formulae.³ Jaśkowski’s transformation is the function − ^∙ from For^d into For_m such that:

• 1. (a)^∙ = a, for any propositional letter a,

• 2. and for any A, B ∈ For^d:

  • (a) ( ¬A)^∙ =  ⌜  ¬A ^∙ ⌝ ,

  • (b) (A ∨ B)^∙ =  ⌜ A ^∙ ∨ B ^∙ ⌝ ,

  • (c) (A ∧ ^​d B)^∙ =  ⌜ A ^∙ ∧ ◊ B ^∙ ⌝ ,

  • (d) (A → ^d B)^∙ =  ⌜ ◊ A ^∙ → B ^∙ ⌝ 

  • (e) (A ↔ ^d B)^∙ =  ⌜ ( ◊ A ^∙ → B ^∙) ∧ ◊ ( ◊ B ^∙ → A ^∙) ⌝ .⁴

Assume that voices in a discussion are written formally by schemes: A ₁, …, A _n . We consider a possible conclusion B. Since formulae A ₁, …, A _n and B may contain logical constants thus, instead of ◊ A ₁, …, ◊ A _n and ◊ B we have to consider their discussive versions: ◊ A ₁ ^∙, …, ◊ A _n ^∙ and ◊ B ^∙. Taking into account examples given by Jaśkowski we see that he used the following definition of a discussive relation: B follows discussively fromA ₁, …, A _n iff the following formula

$$\lozenge {A}_{1}^{\bullet }\rightarrow (\ldots \rightarrow (\lozenge {A}_{ n}^{\bullet }\rightarrow \lozenge {B}^{\bullet })\ldots \,)$$

belongs to S5.⁵

To conclude, discussive deductive systems are to be based on a certain logic connected with the following consequence relation for formulae from For^d.

Definition

For any Π ⊆ For^d and B ∈ For^d : Π ⊢ _{D 2} B iff for some n ≥ 0 and for some A₁ , …, A _n ∈ Π we have

$$\ulcorner \lozenge {A}_{1}^{\bullet }\rightarrow (\ldots \rightarrow (\lozenge {A}_{ n}^{\bullet }\rightarrow \lozenge {B}^{\bullet })\ldots \,)\urcorner \in \mathbf{S5}\,.$$

In other words,

$$\Pi {\vdash }_{{\mathbf{D}}_{\mathbf{2}}}B\text{ iff }\{\lozenge {A}^{\bullet } : A \in \Pi \} {\vdash }_{\mathbf{ S5}}\lozenge {B}^{\bullet },$$

where ⊢ _S5 is the pure modus-ponens-style inference relation based on S5 (see Definition 9.A.1 and Fact 9.A.1 in Appendix).

Jaśkowski used notation ‘D ₂ ’ referring to a logic, i.e. a certain set of formulae.

Definition

D ₂ :={ A ∈ For ^d : ⌜◊A ^∙ ⌝∈ S5 }.

Thus, on the basis of D ₂ one can characterize the consequence relation for discussive systems in the following way:

Fact

For any n ≥ 0, A ₁ , …, A _n , B ∈ For^d :

$$\begin{array}{rcl}{ A}_{1},\ldots ,{A}_{n} {\vdash }_{{\mathbf{D}}_{\mathbf{2}}}B& \quad \text{ iff}\quad \ulcorner (\lozenge {A}_{1}^{\bullet }\wedge \cdots \wedge \lozenge {A}_{n}^{\bullet }) \rightarrow \lozenge {B}^{\bullet }\urcorner \in \mathbf{S5} & \\ & \quad \text{ iff}\quad \ulcorner \lozenge {A}_{1}^{\bullet }\rightarrow (\ldots \rightarrow (\lozenge {A}_{n}^{\bullet }\rightarrow \lozenge {B}^{\bullet })\ldots \,)\urcorner \in \mathbf{S5}& \\ & \quad \text{ iff}\quad \ulcorner \lozenge {({A}_{1}{\rightarrow }^{\mathrm{d}}(\ldots {\rightarrow }^{\mathrm{d}}({A}_{n}{\rightarrow }^{\mathrm{d}}B)\ldots ))}^{\bullet }\urcorner \in \mathbf{S5} & \\ & \quad \text{ iff}\quad \ulcorner {A}_{1}{\rightarrow }^{\mathrm{d}}(\ldots {\rightarrow }^{\mathrm{d}}({A}_{n}{\rightarrow }^{\mathrm{d}}B)\ldots \,)\urcorner \in {\mathbf{D}}_{\mathbf{2}} & \\ & \quad \text{ iff}\quad \ulcorner ({A}_{1}{\wedge }^{\!\mathrm{d}}\cdots {\wedge }^{\!\mathrm{d}}{A}_{n}){\rightarrow }^{\mathrm{d}}B\urcorner \in {\mathbf{D}}_{\mathbf{2}}\,. & \\ \end{array}$$

Proof.

By PL, (5 ^◇! ), (R), and definitions of the relation ⊢  _{D 2} , the function − ^∙, and the logic D ₂ .

Notice that, by the above fact, we can express the relation ⊢  _{D 2} as the pure modus-ponens-style inference relation based on D ₂ .

Fact

For any Π ⊆ For^d and B ∈ For^d :

$$\begin{array}{rcl} \Pi {\vdash }_{{\mathbf{D}}_{\mathbf{2}}}B\quad \text{ iff}\quad & & \mathrm{there\ exists\ a\ sequence\ }{A}_{1},\ldots ,{A}_{n} = B\mathrm{\ in\ which\ for\ any\ }i \leq n, \\ & & \mathrm{either\ }{A}_{i} \in \Pi \cup {\mathbf{D}}_{\mathbf{2}}\mathrm{\ or\ there\ are\ }j,k < i\mathrm{such\ that\ }{A}_{k} = \\ & & \ulcorner {A}_{j}{\rightarrow }^{\mathrm{d}}{A}_{ i}\urcorner .\end{array}$$

Proof.

Because ({ M}₂1) belongs to S5, so D ₂ is closed under modus ponens for ‘ → ^d’, i.e., for any A, B ∈ For^d, if A, ⌜ A → ^d B ⌝ ∈ D ₂ , then B ∈ D ₂ . Moreover, D ₂ contains for any A, B, C ∈ For^d the following formulae:

$$\begin{array}{rcl} A{\rightarrow }^{\mathrm{d}}(B{\rightarrow }^{\mathrm{d}}A)& & \\ (A{\rightarrow }^{\mathrm{d}}(B{\rightarrow }^{\mathrm{d}}C)){\rightarrow }^{\mathrm{d}}((A{\rightarrow }^{\mathrm{d}}B){\rightarrow }^{\mathrm{d}}(A{\rightarrow }^{\mathrm{d}}C))& & \\ \end{array}$$

So the condition from the fact is equivalent to the following condition: for some n ≥ 0 and for some A ₁, …, A _n  ∈ Π we have $\ulcorner {A}_{1}{\rightarrow }^{\mathrm{d}}(\ldots {\rightarrow }^{\mathrm{d}}({A}_{n}{\rightarrow }^{\mathrm{d}}B)\ldots \,)\urcorner \in {\mathbf{D}}_{\mathbf{2}}$.⁶ Thus, by Fact 9.1, it is equivalent to Π ⊢  _{D 2} B.

3 Other Logics Defining D ₂

Definition

Let L be any modal logic.

• (i) We say that L defines D ₂ iff D ₂  = { A ∈ For^d :  ⌜ ◊ A ^∙ ⌝ ∈ L }.

• (ii) Let S5 _◇ be the set of all modal logics which have the same theses beginning with ‘ ◊ ’ as S5, i.e., L ∈ S5 _◇ iff ${\forall }_{A\in \mathrm{{For}}_{\mathrm{m}}}(\ulcorner \lozenge A\urcorner \in \mathbf{L}\;\Longleftrightarrow\;\ulcorner \lozenge A\urcorner \in \mathbf{S5})$.

Fact

Nasieniewski and Pietruszczak (2008). For any classical modal logic L :L defines D ₂ iff L ∈ S5 _◇.

In Furmanowski (1975), it was shown that S4 and S5 have the same members beginning with ‘ ◊ ’—thus, one can use weaker modal logics to define D ₂ . In Perzanowski (1975), the smallest normal modal logic (denoted by S5 ^M) possessing this property was indicated.

In Perzanowski (1975) S5 ^M was defined as the smallest normal logic containing ⌜ ◊ ⊤ ⌝ ,⁷

$$\lozenge \square (\lozenge \square p \rightarrow \square p) $$

(ML5)

$$\lozenge \square (\square p \rightarrow p) $$

(MLT)

and closed under the following rule:

$$\text{ if $\ulcorner {\lozenge}{\lozenge} A\urcorner \in {\mathbf{S5}}^{\mathbf{M}}$ then $\ulcorner \lozenge A\urcorner \in {\mathbf{S5}}^{\mathbf{M}}$.} $$

(RM2 1)

Let NS5 _◇ and RS5 _◇ be respectively the sets of all normal and regular logics from S5 _◇.

Fact

Perzanowski (1975). S5 ^M is the smallest logic in NS5 _◇.

Notice that one can drop two out of the three axioms of the original formulation of S5 ^M (see also Fact 9.8ii).

Fact

Nasieniewski and Pietruszczak (2008). S5 ^M is the smallest normal logic which contains (MLT) and is closed under (R M ₁ ²).

Besides, it was proved in Błaszczuk and Dziobiak (1977) that one can define the logic S5 ^M without the rule (RM ₁ ²), using instead—as an additional axiom—the following formula (“semi-4”):

$$\square p \rightarrow \lozenge \square \square p $$

(4S)

Fact

Błaszczuk and Dziobiak (1977). S5 ^M is the smallest normal logic containing (4S) and (MLT), i.e. S5 ^M = K4 _s { (MLT)}.⁸

Additionally, in Nasieniewski (2002) another axiomatisation of the logic S5 ^M without the rule (RM ₁ ²) was given.

Fact

Nasieniewski (2002). S5 ^M is the smallest normal logic which contains (4S) and the converse of  (5)

$$\square p \rightarrow \lozenge \square p $$

(5c)

i.e.  S5 ^M = K4 _s 5 _c .

In Nasieniewski and Pietruszczak (2008) a regular version of the logic S5 ^M was considered. It was proved that while defining the logic D ₂ one can use a weaker modal logic than S5 ^M.

Definition

Let rS5 ^M denote the smallest regular logic which contains (MLT) and is closed under the rule (R M ₁ ²).

Fact

Nasieniewski and Pietruszczak (2008).

• (i) The logic rS5 ^M is not normal. In other words, rS5 ^M has no thesis of the form ⌜ □ B ⌝ . Thus, rS5 ^M ⊊ S5 ^M.

• (ii) (D),  (ML5) ∈ rS5 ^M.

• (iii) rS5 ^M is the smallest logic in RS5 _◇ ; so rS5 ^M is the smallest regular logic defining D ₂ .

From Fact 9.8(iii) we obtain:

Corollary

For any modal logic L : if rS5 ^M ⊆L ⊆S5, then L ∈S5 _◇ .

In Nasieniewski and Pietruszczak (2009) three axiomatisations of rS5 ^M where given: two of them were formulated without (RM ₁ ²) rule, while one was using (RM ₁ ²). Axiomatisations of rS5 ^M correspond to axiomatisations of the logic S5 ^M. These results have been summarized below.

Fact

Nasieniewski and Pietruszczak (2009).

rS5 ^M is the smallest regular logic which :

• (i) Contains (MLT) and (4S), i.e. rS5 ^M = C4 _s { (MLT)} ;

• (ii) Contains (5c) and (4S), i.e. rS5 ^M = C4 _s 5 _c ;

• (iii) Contains (5c) and is closed under (RM ₁ ²).

Besides, we have the upward analogue of the result from Fact 9.8(iii).

Fact

Nasieniewski and Pietruszczak (2008).

If L is a regular logic defining D ₂ , then L ⊆ S5.⁹

4 KD45 in the Formulation of D ₂ -Consequence

It appears that the consequence relation ⊢  _{D 2} is closely related to the normal logic KD45 ($= \mathbf{K5!} ={ \mathbf{K55}}_{\mathbf{c}}$; see Lemma 9.A.8(v)). To start an investigation of this relationship, we will prove the following lemma.

Lemma

• (i) (4S) ∈ CD4 ⊊ KD4.

• (ii) (4), (5)∉K4 _s 5 _c  = S5 ^M.

• (iii) S5 ^M ⊊ KD4 ⊊ KD45.

Proof.

• (i) By (4), (US) and PL, the formula ‘ □ p → □ □ □ p’ belongs to C4. Moreover, by (D), (US) and PL, we obtain that (4S) ∈ CD4.

• (ii) By “the corresponding Hintikka condition” from Segerberg (1971), Theorem 6.5 (see also Błaszczuk and Dziobiak 1977; Nasieniewski 2002) we know that normal logics defined by (5c), and (4S) are determined by frames ⟨W, R⟩ fulfilling, respectively, the following conditions:

  $${\forall }_{u}{\exists }_{x}{\bigl (u\mathit{R}x \& {\forall }_{v}(x\mathit{R}v\Longrightarrow u\mathit{R}v)\bigr )} $$

  (h5c)
  $${\forall }_{u}{\exists }_{x}{\bigl (u\mathit{R}x \& {\forall }_{v}(x{\mathit{R}}^{2}v\Longrightarrow u\mathit{R}v)\bigr )} $$

  (h4s)

  We can indicate a model whose frame fulfils this conditions in which (4) and (5) are falsified. Thus, (5), (4)∉K4 _s 5 _c . By Fact 9.7, K4 _s 5 _c  = S5 ^M.

• (iii) By (i), (ii) and Lemma 9.A.8(iii) we have S5 ^M ⊊ KD4 = K45 _c ⊊ KD45.

Since S5 ^M ⊆ KD45 ⊆ S5, so from Fact 9.3 and Corollary 9.1 we obtain:

Corollary

KD45 ∈NS5 _◇ and KD45 defines D ₂ .

We can define a discussive consequence on the basis of any modal logic L.

Definition

For any Π ⊆ For^d and B ∈ For^d : $\Pi {\vdash }_{{\mathbf{D}}_{\mathbf{L}}}B$ iff for some n ≥ 0 and for some A ₁ , …, A _n ∈ Π we have $\ulcorner \lozenge {A}_{1}^{\bullet }\rightarrow (\ldots \rightarrow \lozenge {A}_{n}^{\bullet }\rightarrow \lozenge {B}^{\bullet })\ldots \,)\urcorner \in \mathbf{L}$ . In other words,

$$\Pi {\vdash }_{{\mathbf{D}}_{\mathbf{L}}}B\text{ iff }\{\lozenge {A}^{\bullet } : A \in X\} {\vdash }_{\mathbf{ L}}\lozenge {B}^{\bullet },$$

where ⊢ _L is the pure modus-ponens-style inference relation based on L (see Definition 9.A.1 and Fact 9.A.1).

If $\Pi =\{ {A}_{1},\ldots ,{A}_{n}\}$ , then we will use notation: ${A}_{1},\ldots ,{A}_{n} {\vdash }_{{\mathbf{D}}_{\mathbf{L}}}A$ .

By (R) and (5!) we obtain

Lemma

Let L be any normal logic such that KD45 ⊆ L. Then for any A₁, …, A_n, B ∈ For _m :

$$\begin{array}{rcl} \ulcorner \lozenge (\lozenge {A}_{1} \rightarrow (\ldots \rightarrow (\lozenge {A}_{n} \rightarrow B)\ldots \,))\urcorner & \in & \mathbf{L}\quad \text{ iff} \\ \ulcorner \lozenge {A}_{1}& \rightarrow & (\ldots \rightarrow (\lozenge {A}_{n} \rightarrow \lozenge B)\ldots )\urcorner \in \mathbf{L}.\,\end{array}$$

Corollary

For any A ₁ , …, A _n , B ∈ For^d :

$$\begin{array}{rcl} \ulcorner {A}_{1}{\rightarrow }^{\mathrm{d}}(\ldots & {\rightarrow }^{\mathrm{d}}& ({A}_{ n}{\rightarrow }^{\mathrm{d}}B)\ldots \,)\urcorner \in {\mathbf{D}}_{\mathbf{ 2}}\quad \text{ iff} \\ \ulcorner & \lozenge & {({A}_{1}{\rightarrow }^{\mathrm{d}}(\ldots {\rightarrow }^{\mathrm{d}}({A}_{ n}{\rightarrow }^{\mathrm{d}}B)\ldots \,))}^{\bullet }\urcorner \in \mathbf{KD45}\quad \text{ iff} \\ & & \qquad \qquad \quad \ \ulcorner \lozenge {A}_{1}^{\bullet }\rightarrow (\ldots \rightarrow (\lozenge {A}_{ n}^{\bullet }\rightarrow \lozenge {B}^{\bullet })\ldots \,)\urcorner \in \mathbf{KD45}.\,\end{array}$$

By definitions, Corollaries 9.2 and 9.3, and Fact 9.1 we obtain

Theorem

${\vdash }_{{\mathbf{D}}_{\mathbf{2}}} = {\vdash }_{{\mathbf{D}}_{\mathbf{KD45}}}$ .

Proof.

For any A ₁, …, A _n , B ∈ For^d we obtain

$$\begin{array}{rcl}{ A}_{1},\ldots ,{A}_{n} {\vdash }_{{\mathbf{D}}_{\mathbf{KD45}}}B\quad & \text{ iff}\quad \ulcorner \lozenge {A}_{1}^{\bullet }\rightarrow (\ldots \rightarrow (\lozenge {A}_{n}^{\bullet }\rightarrow \lozenge {B}^{\bullet })\ldots \,)\urcorner \in \mathbf{KD45}& \\ & \text{ iff}\quad \ulcorner \lozenge {({A}_{1}{\rightarrow }^{\mathrm{d}}(\ldots {\rightarrow }^{\mathrm{d}}({A}_{n}{\rightarrow }^{\mathrm{d}}B)\ldots ))}^{\bullet }\urcorner \in \mathbf{KD45} & \\ & \text{ iff}\quad \ulcorner \lozenge {({A}_{1}{\rightarrow }^{\mathrm{d}}(\ldots {\rightarrow }^{\mathrm{d}}({A}_{n}{\rightarrow }^{\mathrm{d}}B)\ldots ))}^{\bullet }\urcorner \in \mathbf{S5} & \\ & \text{ iff}\quad {A}_{1},\ldots ,{A}_{n} {\vdash }_{{\mathbf{D}}_{\mathbf{2}}}B & \\ \end{array}$$

Thus, for any Π ⊆ For^d and B ∈ For^d: Π ⊢  _{D 2} B iff $\Pi {\vdash }_{{\mathbf{D}}_{\mathbf{KD45}}}B$.

In what follows, we prove that KD45 is the smallest, while S5 is the largest among normal logics which define the same consequence relation ⊢  _{D 2} . But neither S5 ^M nor S4 is appropriate for this purpose.

Fact

${\vdash }_{{\mathbf{D}}_{{\mathbf{ S5}}^{\mathbf{M}}}} \subsetneq {\vdash }_{{\mathbf{D}}_{\mathbf{S4}}} \subsetneq {\vdash }_{{\mathbf{D}}_{\mathbf{2}}}$ .□

The inclusions “ ⊆ ” are obvious. For “ ⊊” we can use either the following examples or the next fact.

Example

• (i) $(p \vee \neg p){\wedge }^{\!\mathrm{d}}p {\vdash }_{{\mathbf{D}}_{\mathbf{S4}}}p$, while $(p \vee \neg p){\wedge }^{\!\mathrm{d}}p {\nvdash }_{{\mathbf{D}}_{{\mathbf{ S5}}^{\mathbf{M}}}}p$. Indeed, $(p \vee \neg p){\wedge }^{\!\mathrm{d}}p {\vdash }_{{\mathbf{D}}_{{\mathbf{ S5}}^{\mathbf{M}}}}p$ iff ‘ ◊ ((p ∨  ¬p) ∧ ◊ p) → ◊ p’ belongs to S5 ^M iff (4 ^◇) ∈ S5 ^M iff (4) ∈ S5 ^M. But (4)∉S5 ^M, by Lemma 9.1(ii).

• (ii) p, q ⊢  _{D 2} p ∧ ^​d q, while $p,q {\nvdash }_{{\mathbf{D}}_{\mathbf{S4}}}p{\wedge }^{\!\mathrm{d}}q$.

• (iii) (p ∨  ¬p) ∧ ^​d p, q ⊢  _{D 2} p ∧ ^​d q, while $(p \vee \neg p){\wedge }^{\!\mathrm{d}}p,q {\nvdash }_{{\mathbf{D}}_{\mathbf{S4}}}p{\wedge }^{\!\mathrm{d}}q$. □ 

Fact

• (i) Let L be any regular logic such that ${\vdash }_{{\mathbf{D}}_{\mathbf{2}}} \subseteq {\vdash }_{{\mathbf{D}}_{\mathbf{L}}}$. Then L contains  (D), (4), and ⌜ □ ⊤ → (5) ⌝ , so CD45(1) ⊆ L.¹⁰

• (ii) Let L be any normal logic such that ${\vdash }_{{\mathbf{D}}_{\mathbf{2}}} \subseteq {\vdash }_{{\mathbf{D}}_{\mathbf{L}}}$. Then L contains (D), (4), and (5), so KD45 ⊆ L.

Proof.

• (i) For (D): Since ∅ ⊢  _{D 2} p ∨  ¬p, so—by the assumption—also $\varnothing {\vdash }_{{\mathbf{D}}_{\mathbf{L}}}p \vee \neg p$. Hence ‘ ◊ (p ∨  ¬p)′ ∈ L, by the definition of ${\vdash }_{{\mathbf{D}}_{\mathbf{L}}}$. By Lemmas 9.A.5 and 9.A.7 we have that (D) ∈ L.

  For ⌜ □ ⊤ → (5) ⌝ : Since p → ^d ¬(p ∨  ¬p), p ⊢  _{D 2} ¬(p ∨  ¬p), so—by the assumption—also $p{\rightarrow }^{\mathrm{d}}\neg (p \vee \neg p),p {\vdash }_{{\mathbf{D}}_{\mathbf{L}}}\neg (p \vee \neg p)$. Therefore, by the definition of ${\vdash }_{{\mathbf{D}}_{\mathbf{L}}}$, we get that ‘ ◊ [ ◊ p →  ¬(p ∨  ¬p)] → [ ◊ p → ◊  ¬(p ∨  ¬p)]’ belongs to L. Thus, by PL, ‘ ¬ ◊ ( ◊ p →  ¬ ⊤ ) ∨ ( ◊ p → ◊  ¬ ⊤ )’ belongs to L. Thus, by (R) and PL, also ‘ ¬( □ ◊ p → ◊  ¬ ⊤ ) ∨ ( ◊ p → ◊  ¬ ⊤ )’, ‘( □ ◊ p ∧  ¬ ◊  ¬ ⊤ ) ∨  ¬ ◊ p ∨ ◊  ¬ ⊤ ’, ‘( □ ◊ p ∨  ¬ ◊ p ∨ ◊  ¬ ⊤ ) ∧ ( ¬ ◊  ¬ ⊤ ∨  ¬ ◊ p ∨ ◊  ¬ ⊤ )’, and ‘ □ ◊ p ∨  ¬ ◊ p ∨ ◊  ¬ ⊤ ’ belong to L. Thus, ‘ ◊ p ∧ □ ⊤ → □ ◊ p’ and ⌜ □ ⊤ → (5 ^◇) ⌝ belong to L. Hence, by the standard duality result, ⌜ □ ⊤ → (5) ⌝ ∈ L as well.

  For (4): Since p ∧ ^​d q ⊢  _{D 2} q, so ‘ ◊ (p ∧ ◊ q) → ◊ q’ and ‘ ◊ ( ⊤ ∧ ◊ q) → ◊ q’ belong to L. However ‘ ◊ ◊ q → ◊ ( ⊤ ∧ ◊ q)’ is a thesis of all regular logics. Thus, by transitivity, we obtain that (4 ^◇) ∈ L; so also (4) ∈ L.

• (ii) Since L is normal, so L is regular and ⌜ □ ⊤ ⌝ ∈ L.

Let Cn _◇ S5 be the set of modal logics which satisfy the following condition: for any logic L

$$\begin{array}{rcl} \mathbf{L} \in {\mathbf{Cn}}_{\diamond}\mathbf{S5}& \stackrel{\text{ df}}{\;\Longleftrightarrow\;}\text{ for any $\Pi \subseteq \mathrm{{ For}}_{\mathrm{m}}$ and $B \in \mathrm{{ For}}_{\mathrm{m}}$,}& \\ & \lozenge \Pi {\vdash }_{\mathbf{L}}\lozenge B\text{ iff }\lozenge \Pi {\vdash }_{\mathbf{S5}}\lozenge B\,. & \\ \end{array}$$

Let NCn _◇ S5 be the set of all normal logics from Cn _◇ S5. By definitions, Lemma 9.2, and Corollary 9.2 we obtain

Fact

KD45 ∈NCn _◇ S5.

Lemma

(5c) and (5) belong to all logics from NCn _◇ S5. Thus, every logic from NCn _◇ S5 includes KD45.

Proof.

Firstly, ‘ ◊ ( ◊ p → p)’ and ‘( ◊ p ∧ ◊  ¬ ◊ p) → ◊  ¬ ⊤ ’ are theses of S5; so they are also theses of all logics from NCn _◇ S5. Secondly, these formulae are equivalent, respectively, to (5 _c ^◇) and (5 ^◇), on the basis of any normal modal logic. Thus, (5 _c ^◇) and (5 ^◇) belong to all logics from NCn _◇ S5. So every logic from NCn _◇ S5 includes K55 _c ( = KD45).

By Fact 9.13 and Lemma 9.3 we obtain:

Theorem

KD45 is the smallest element in NCn _◇ S5.

Below we introduce a transformation from For_m to For^d. It allows us to prove that if any normal logic defines the D ₂ -consequence, it has to be located between KD45 and S5.

Definition

Let − ^∘ be the function from For _m into For ^d such that:

• 1. (a)^∘ = a, for any propositional lettera,

• 2. And for anyA, B ∈ For_m:

  • (a) ( ¬A)^∘ =  ⌜  ¬A ^∘ ⌝ ,

  • (b) (A ∨ B)^∘ =  ⌜ A ^∘ ∨ B ^∘ ⌝ ,

  • (c) (A ∧ B)^∘ =  ⌜  ¬( ¬A ^∘ ∨  ¬B ^∘) ⌝ ,

  • (d) (A → B)^∘ =  ⌜  ¬A ^∘ ∨ B ^∘ ⌝ ,

  • (e) (A ↔ B)^∘ =  ⌜  ¬( ¬( ¬A ^∘ ∨ B ^∘) ∨  ¬( ¬B ^∘ ∨ A ^∘)) ⌝ ,

  • (f) ( ◊ A)^∘ =  ⌜ (p ∨  ¬p) ∧ ^​d A ^∘ ⌝ ,

  • (g) ( □ A)^∘ =  ⌜  ¬A ^∘ → ^d ¬(p ∨  ¬p) ⌝ .

Lemma

For any A ∈ For _m : ⌜A↔A ^∘∙ ⌝ is a thesis of all classical logics.

Lemma

For any classical modal logic L

$${\vdash }_{{\mathbf{D}}_{\mathbf{L}}} = {\vdash }_{{\mathbf{D}}_{\mathbf{2}}}\quad \text{ iff}\quad \mathbf{L} \in {\mathbf{Cn}}_{\diamond}\mathbf{S5}\,.$$

Proof.

“ ⇒ ” ◊ A ₁, …, ◊ A _n  ⊢  _L  ◊ B iff ⌜ ◊ A ₁ → (… → ( ◊ A _n  → ◊ B)…) ⌝ ∈ L iff, by Lemma 9.4, PL, and (REP), ⌜ ◊ A ₁ ^∘ ∙ → (… → ( ◊ A _n ^∘ ∙ → ◊ B ^∘ ∙)…) ⌝ ∈ L iff A ₁ ^∘, …, A _n ^∘ ${\vdash }_{{\mathbf{D}}_{\mathbf{L}}}{B}^{\circ }$ iff A ₁ ^∘, …, A _n ^∘ ⊢  _{D 2} B ^∘ iff ⌜ ◊ A ₁ ^∘ ∙ → (… → ( ◊ A _n ^∘ ∙ → ◊ B ^∘ ∙)…) ⌝ ∈ S5 iff, by Lemma 9.4, PL, and (REP), ◊ A ₁, …, ◊ A _n  ⊢  _S5  ◊ B.

“ ⇐ ” Obvious.

Finally, we get the following

Theorem

For any normal modal logic L :

$${\vdash }_{{\mathbf{D}}_{\mathbf{L}}} = {\vdash }_{{\mathbf{D}}_{\mathbf{2}}}\quad \text{ iff}\quad \mathbf{KD45} \subseteq \mathbf{L} \subseteq \mathbf{S5}\,.$$

Proof.

“ ⇒ ” For KD45 ⊆ L see Fact 9.12(ii).

For any A ∈ For_m we have: ∅ ⊢  _{D 2} A ^∘ iff $\varnothing {\vdash }_{{\mathbf{D}}_{\mathbf{L}}}{A}^{\circ }$. So by Definitions 9.1 and 9.5 we have: ⌜ ◊ A ^∘ ∙ ⌝ ∈ S5 iff ⌜ ◊ A ^∘ ∙ ⌝ ∈ L. Thus, by Lemma 9.4, PL, and (REP), we obtain that: ⌜ ◊ A ⌝ ∈ S5 iff ⌜ ◊ A ⌝ ∈ L. Thus, L ∈ NS5 _◇. Therefore L ⊆ S5, by Facts 9.3 and 9.10.

“ ⇐ ” By Corollary 9.2 and Fact 9.3, L ∈ NS5 _◇. Thus, L ∈ NCn _◇ S5, by Lemma 9.2. Hence ${\vdash }_{{\mathbf{D}}_{\mathbf{2}}} = {\vdash }_{{\mathbf{D}}_{\mathbf{L}}}$, by Lemma 9.5.

5 The Smallest Regular Modal Logic Defining D ₂ -Consequence

We will show that consequence relation ⊢  _{D 2} is also closely connected with the regular logic CD45(1).

Definition

Let CD45(1) be the smallest regular logic which contains (D), (4), and (5(1)), i.e.  ⌜□⊤→ (5)⌝.

Remark

In the notation of Segerberg a regular logic CN ¹ D(1)4(1)5(1) corresponds, by the definition, to the normal logic KD45. Yet in C2 the formulae (D), (4) and (5c) are respectively equivalent to (D(1)), (4(1)) and (5c(1)), i.e., ⌜ □ ⊤ → ( □ p → ◊ p) ⌝ , ⌜ □ ⊤ → ( □ p → □ □ p) ⌝ and ⌜ □ ⊤ → ( □ p → ◊ □ p) ⌝ (see Segerberg 1971, p. 208). Moreover, the formula (N ¹), i.e.  ⌜ □ ⊤ → □ □ ⊤ ⌝ (see Segerberg 1971, p. 198), is an instance of (4). Thus, CD45(1) = CN ¹ D(1)4(1)5(1). Hence, by Lemma 9.A.9, i.e. Corollary 2.4 from Segerberg (1971), vol. II, we obtain:

$$\begin{array}{rcl} \mathbf{CD45}\mathbf{(1)}& ={ \mathbf{CF}}^{\mathbf{1}} \cap \mathbf{KD45}\,,& \\ {\mathbf{CN}}^{\mathbf{1}}{\mathbf{5}}_{\mathbf{ c}}\mathbf{5}\mathbf{(1)}& ={ \mathbf{CF}}^{\mathbf{1}} \cap {\mathbf{K55}}_{\mathbf{c}}\,, & \\ \end{array}$$

where CF ¹ is the falsum logic. □ 

By the above remark and the equality KD45 = K55 _c we obtain¹¹:

Fact

CD45(1) = CN ¹ 5 _c 5(1).

Fact

The logic CD45(1) is not normal. In other words, CD45(1) has no thesis of the form ⌜□B⌝.

Proof.

It is enough to use a model from Fact 3.1 of Nasieniewski and Pietruszczak (2008): Let v be a valuation from For_m into {0, 1} which preserves classical truth conditions for classical connectives and let v( □ A) = 0 and v( ◊ A) = 1, for any A ∈ For_m. Notice that for any thesis of CD45(1) we have v(A) = 1, while, for example, v( □ ⊤ ) = 0.

Fact

rS5 ^M ⊊ CD4 ⊊ CD45(1) ⊊ KD45 ⊊ S5.

Proof.

Notice that, by Lemma 9.9, rS5 ^M = C4 _s 5 _c . Moreover, (5 _c ^◇), (4S) ∈ CD4 = C45 _c , respectively by Lemmas 9.A.8(ii) and 9.1(i). Thus, rS5 ^M ⊆ CD4. This inclusion is proper, since rS5 ^M ⊊ S5 ^M ⊊ KD4 and (4)∉S5 ^M (see Lemma 9.1).

Besides, we have CD4 ⊆ KD4. But (5)∉KD4, so also (5(1))∉KD4, since in all normal logics we have the thesis ‘(5) ↔ (5(1))’. Hence (5(1))∉CD4. Moreover, CD45(1) ⊆ KD45. This inclusion is proper by Fact 9.15.

Lemma

The formulae (†) and for any n ≥ 2

$$\lozenge {p}_{1} \rightarrow (\lozenge {p}_{2} \rightarrow \ldots (\lozenge {p}_{n} \rightarrow (\lozenge ({p}_{1} \wedge (\lozenge {p}_{2} \wedge \ldots (\lozenge {p}_{n-1} \wedge \lozenge {p}_{n})\ldots \,)))))$$

and for any n ≥ 1

$$\begin{array}{rcl} \lozenge (\lozenge {p}_{1} \rightarrow (\lozenge {p}_{2} \rightarrow \ldots (\lozenge {p}_{n}& \rightarrow & q)\ldots \,)) \rightarrow \\ &\rightarrow & (\lozenge {p}_{1} \rightarrow (\lozenge {p}_{2} \rightarrow \ldots (\lozenge {p}_{n} \rightarrow \lozenge q)\ldots \,)) \\ \end{array}$$

are theses of CN ¹ 5(1) ⊆CD45(1).

Proof.

By Lemma 9.A.8(vi), $(\dag ) \in \mathbf{K5}$. Obviously $(\dag ) \in {\mathbf{CF}}^{\mathbf{1}}$. So, we use Lemma 9.A.9. The proof in the case of remaining formulae is analogous. It is by induction on n.

Let RCn _◇ S5 be the set of all regular logics from Cn _◇ S5. We have:

Lemma

CD45(1) ∈RCn _◇ S5.

Proof.

For any A ₁, …, A _n , B ∈ For_m by Lemma 9.2 and Fact 9.16, and Fact 9.8(iii): $\ulcorner \lozenge {A}_{1} \rightarrow (\ldots \rightarrow (\lozenge {A}_{n} \rightarrow \lozenge B)\ldots \,)\urcorner \in \mathbf{S5}$ iff $\ulcorner \lozenge (\lozenge {A}_{1} \rightarrow (\ldots \rightarrow (\lozenge {A}_{n} \rightarrow B)\ldots ))\urcorner \in \mathbf{S5}$ iff $\ulcorner \lozenge (\lozenge {A}_{1} \rightarrow (\ldots \rightarrow (\lozenge {A}_{n} \rightarrow B)\ldots ))\urcorner \in \mathbf{CD45}\mathbf{(1)}$.

By Lemma 9.6, it follows from the last statement that $\ulcorner \lozenge {A}_{1} \rightarrow (\ldots \rightarrow (\lozenge {A}_{n} \rightarrow \lozenge B)\ldots \,)\urcorner \in \mathbf{CD45}\mathbf{(1)}$. The reverse implication is obvious.

By the above lemma we have directly:

Corollary

⊢ _{D 2} = ⊢ _{D CD45(1)} .

By Fact 9.12(i) and Definition 9.7 we obtain:

Lemma

For any regular logic L such that ${\vdash }_{{\mathbf{D}}_{\mathbf{2}}} = {\vdash }_{{\mathbf{D}}_{\mathbf{L}}}$ it is the case that CD45(1) ⊆ L.

By Lemmas 9.7, 9.5, and 9.8 we conclude that

Corollary

CD45(1) is the smallest element in RCn _◇ S5.

We have of course also a regular version of Theorem 9.3:

Lemma

S5 is the biggest element in RCn _◇ S5.

Proof.

Let us assume that L ∈ RCn _◇ S5 and A ∈ L. By the classical logic we have (p ∨  ¬p) → A ∈ L and by monotonicity ◊ □ (p ∨  ¬p) → ◊ □ A ∈ L i.e, ◊ □ (p ∨  ¬p) ⊢  _L  ◊ □ A. Thus, by the assumption ◊ □ (p ∨  ¬p) → ◊ □ A ∈ S5 and by MP we obtain that ◊ □ A ∈ S5, so using the standard reduction of modalities we obtain that A ∈ S5.

We have a lemma that is analogous to Lemma 9.8:

Lemma

For any regular logic L such that ⊢ _{D 2} = ⊢ _{D L} it is the case that L ⊆ S5.

Proof.

Assume that A ∈ L. By Lemma 9.4 we have also A ^∘ ∙ ∈ L.

Since ◊ ( ◊  ¬(p ∨  ¬p) →  ¬(p ∨  ¬p)) ∈ S5 thus, ¬(p ∨  ¬p) → ^d ¬(p ∨  ¬p) ∈ D ₂ and by the assumption also ¬(p ∨  ¬p) → ^d ¬(p ∨  ¬p) ∈ D _L . By the definition of D _L it means that ◊ ( ◊  ¬(p ∨  ¬p) →  ¬(p ∨  ¬p)) ∈ L. But for every regular modal logic the last statement is equivalent to: ◊ □ (p ∨  ¬p) ∈ L. It follows from Lemma 9.A.6 that ◊ □ A ^∘ ∙ ∈ L. But again for every regular modal logic this condition is equivalent to ◊ ( ◊  ¬A ^∘ ∙ →  ¬(p ∨  ¬p)) ∈ L, which means that ¬A ^∘ → ^d ¬(p ∨  ¬p) ∈ D _L , so ¬A ^∘ → ^d ¬(p ∨  ¬p) ∈ D ₂ . Therefore, ◊ ( ¬A ^∘ → ^d ¬(p ∨  ¬p))^∙ ∈ S5, equivalently ◊ □ A ^∘ ∙ ∈ S5. From this follows that A ^∘ ∙ ∈ S5 while by Lemma 9.4 we conclude that A ∈ S5.

So taking together Lemmas 9.8 and 9.10 we receive:

Corollary

For any regular logic L such that ⊢ _{D L} = ⊢ _{D 2} we have CD45(1) ⊆ L ⊆S5.

Lemma

For any regular logic L such that CD45(1) ⊆ L ⊆S5 we have L ∈RCn _◇ S5.

Proof.

Assume that CD45(1) ⊆ L ⊆ S5. We have to prove that for any A ₁, …, A _n , B ∈ For_m: $\ulcorner \lozenge (\lozenge {A}_{1} \rightarrow (\ldots \rightarrow (\lozenge {A}_{n} \rightarrow B)\ldots ))\urcorner \in \mathbf{S5}$ iff $\ulcorner \lozenge (\lozenge {A}_{1} \rightarrow (\ldots \rightarrow (\lozenge {A}_{n} \rightarrow B)\ldots ))\urcorner \in \mathbf{L}$. Left-to-right implication follows from Lemma 9.7. The reverse implication is obvious.

From this lemma and Lemma 9.5 we obtain

Theorem

For any regular logic L such that CD45(1) ⊆ L ⊆S5 we have ⊢ _{D L} = ⊢ _{D 2} .

Finally, directly from Corollary 9.6 and Lemma 9.11 we get the following

Theorem

For any regular modal logic L

$${\vdash }_{{\mathbf{D}}_{\mathbf{L}}} = {\vdash }_{{\mathbf{D}}_{\mathbf{2}}}\quad \text{ iff}\quad \mathbf{CD45}\mathbf{(1)} \subseteq \mathbf{L} \subseteq \mathbf{S5}\,.$$

6 Appendix: Some Facts from Modal Logic

As in Chellas (1980) modal formulae are formed in a relational way from propositional letters: ‘p’, ‘q’, ‘p ₀’, ‘p ₁’, ‘p ₂’, …; 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. Let For_m be the set of modal formulae, and—as in Chellas (1980)—let PL be the set of modal formulae which are instances of classical tautologies. Let ⊤ : =  ‘ p → p’.

As in Bull and Segerberg (1984) and Chellas and Segerberg (1996), a set L of modal formulae is a (modal) logic iff

• PL ⊆ L,

• For any C, A ∈ For_m: L contains the following formula

  $$C{[}^{\neg \square \neg A}{/}_{ \lozenge A}]\leftrightarrow C\,, $$

  (rep)

  where C[^A ∕  _B ] is any formula that results from C by replacing one or more occurrences of A, in C, by B, i.e. using (rep) we are replacing in C one or more occurrences of ‘ ¬ □  ¬’ by ‘ ◊ ’.¹²

• L is closed under the following three rules: modus ponens for ‘ → ’:

  $$\mathrm{if}\ A\mathrm{and}\ulcorner A \rightarrow B\urcorner \mathrm{are}\ \mathrm{members}\ \mathrm{of}\ \mathbf{L},\ \mathrm{so}\ \mathrm{is}B. $$

  (MP)

  uniform substitution:

  $$\mathrm{if}\ A \in \mathbf{L}\ \mathrm{then}\mathrm{s}A \in \mathbf{L}, $$

  (US)

  where sA is the result of uniform substitution of formulae for propositional letters in A.

Definition

Let L be any modal logic. We define the consequence ⊢ _L as follows. For any Π ⊆ For _m and B ∈ For _m : Π ⊢ _L B iff for some n ≥ 0 and for some A ₁ , …, A _n ∈ Π we have $\ulcorner {A}_{1} \rightarrow (\ldots \rightarrow ({A}_{n} \rightarrow B)\ldots \,)\urcorner \in \mathbf{L}$.

Notice that Π ⊢  _L B iff there is a derivation of B from L ∪Π with the help of modus ponens for ‘ → ’ as the only rule of inference, i.e., ⊢  _L is the pure modus-ponens-style inference relation based on L.

Fact

Lemmon (1977). Π ⊢ _L B iff there exists a sequence A ₁ , …, A _n = B in which for any i ≤ n, either A _i ∈ Π, or A _i ∈ L, or there are j,k < i such that A _k = ⌜A _j → A _i ⌝.

All members of the set L are called theses of the logic L. By (rep), every modal logic has the following thesis:

$$\lozenge p\leftrightarrow \neg \square \neg p. $$

(df)

A modal logic L is classical (congruent) iff L is closed under the following rule for any A, B ∈ For_m:

$$\mathrm{if}\ \ulcorner A\leftrightarrow B\urcorner \in \mathbf{L}\ \mathrm{then}\ \ulcorner \square A\leftrightarrow \square B\urcorner \in \mathbf{L}. $$

(RE)

Every classical logic L is closed under the rule of replacement, i.e. for any A, B, C ∈ For_m:

$$\text{ if $\ulcorner A\leftrightarrow B\urcorner \in \mathbf{L}$ then $\ulcorner C\leftrightarrow C{[}^{A}{/}_{B}]\urcorner \in \mathbf{L}$.} $$

(REP)

It is known (cf. e.g. Chellas 1980) that while defining classical logics one uses (df) instead of (rep), i.e. treats them (logics) as subsets of For_m which include PL and (df) and which are closed under rules (MP), (US) and (RE). We also have an analogous situation in the case of monotonic, regular, and normal modal logics defined further.

Every classical modal logic has the following thesis

$$\square p\leftrightarrow \neg \lozenge \neg p $$

(df)

Lemma

A classical modal logic contains, respectively, the following formulae

$$\square (p \rightarrow q) \rightarrow (\square p \rightarrow \square q) $$

(K)

$$\square (p \wedge q)\leftrightarrow (\square p \wedge \square q) $$

(R)

$$\square p \rightarrow p $$

(T)

$$\square p \rightarrow \square \square p$$

(4)

$$\lozenge \square p \rightarrow \square p$$

(5)

$$\square p \rightarrow \lozenge \square p $$

(5c)

$$\square p\leftrightarrow \lozenge \square p $$

(5!)

if and only if it contains, respectively, their dual versions

$$\square (p \rightarrow q) \rightarrow (\lozenge p \rightarrow \lozenge q) $$

(K)

$$\lozenge (p \vee q)\leftrightarrow (\lozenge p \vee \lozenge q) $$

(R)

$$p \rightarrow \lozenge p $$

(T)

$$\lozenge \lozenge p \rightarrow \lozenge p$$

(4)

$$\lozenge p \rightarrow \square \lozenge p$$

(5)

$$\square \lozenge p \rightarrow \lozenge p $$

(5c)

$$\lozenge p\leftrightarrow \square \lozenge p $$

(5!)

Lemma

For any classical modal logic L the following conditions are equivalent :

• (a) For any τ ∈ PL, ⌜ □ τ ⌝ ∈ L (resp.  ⌜ ◊ τ ⌝ ∈ L, ⌜ ◊ □ τ ⌝ ∈ L ).

• (b)  ⌜ □ ⊤ ⌝ ∈ L (resp.  ⌜ ◊ ⊤ ⌝ ∈ L, ⌜ ◊ □ ⊤ ⌝ ∈ L ).

Lemma

Let L be any classical modal logic such that

• (a) Either ⌜□⊤⌝∈ L,

• (b) or (5),⌜◊B⌝∈ L, for some B ∈ For _m .¹³

Then L is closed under the rule of necessitation :

$$\text{ {\it if } $A \in \mathbf{L}$ {\it then} $\ulcorner \square A\urcorner \in \mathbf{L}$.} $$

(RN)

Lemma

Chellas (1980). Let L be any classical modal logic such that (T),(5) ∈L. Then L has as its theses ⌜□⊤⌝, ⌜◊⊤⌝, ⌜◊□⊤⌝, (4), and

$$\square p \rightarrow \lozenge p $$

(D)

and L is closed under (RN ) and the following rules :

$${\it { if}}\ A \in \mathbf{L},{\it { then}}\ \ulcorner \lozenge A\urcorner \in \mathbf{L}, $$

(RP)

$${\it { if}}\ A \in \mathbf{L},{\it { then}}\ \ulcorner \lozenge \square A\urcorner \in \mathbf{L}. $$

(RPN)

A modal logic L is monotonic iff L is closed under the monotonicity rule, i.e. for any A, B ∈ For_m:

$$\mathrm{if}\ \ulcorner A \rightarrow B\urcorner \in \mathbf{L},\ \mathrm{then}\ \ulcorner \square A \rightarrow \square B\urcorner \in \mathbf{L}, $$

(RM)

Every monotonic logic L is classical and it is closed under the dual form of (RM), i.e. for any A, B ∈ For_m:

$$\text{ if $\ulcorner A \rightarrow B\urcorner \in \mathbf{L}$, then $\ulcorner \lozenge A \rightarrow \lozenge B\urcorner \in \mathbf{L}$.} $$

(RM)

Lemma

For any monotonic logic L the following conditions are equivalent :

• (a) For any τ ∈ PL, ⌜ □ τ ⌝ ∈ L (resp.  ⌜ ◊ τ ⌝ ∈ L, ⌜ ◊ □ τ ⌝ ∈ L).

• (b)  ⌜ □ ⊤ ⌝ ∈ L (resp.  ⌜ ◊ ⊤ ⌝ ∈ L, ⌜ ◊ □ ⊤ ⌝ ∈ L).

• (c) For some B ∈ For_m, ⌜ □ B ⌝ ∈ L (resp.  ⌜ ◊ B ⌝ ∈ L, ⌜ ◊ □ B ⌝ ∈ L).

Lemma

Let a monotonic logic L has a thesis of the form ⌜□B⌝ ( resp. ⌜◊B⌝, ⌜◊□B⌝ ) . Then L is closed under the rule (RN )  ( resp. (RP ), (RPN ) ) .

A modal logic L is regular iff L is monotonic and (K) ∈ L. A logic L is regular iff L is closed under the regularity rule, i.e. for any A, B, C ∈ For_m:

$$\mathrm{if}\ \ulcorner A \wedge B \rightarrow C\urcorner \in \mathbf{L}\ \mathrm{then}\ \ulcorner \square A \wedge \square B \rightarrow \square C\urcorner \in \mathbf{L}. $$

(RR)

Every regular modal logic has the following theses: (K ^◇), (R), (R ^◇) and

$$\lozenge (p \rightarrow q)\leftrightarrow (\square p \rightarrow \lozenge q) $$

(R)

By (R) we obtain.

Lemma

For any regular logic L : ⌜◊⊤⌝∈ L iff (D) ∈L.

A modal logic is normal iff it contains (K) and is closed under (RN) iff it is regular and contains ⌜ □ ⊤ ⌝ .

Let K (resp. C2) be the smallest normal (resp. regular) modal logic. Using names of formulae from Lemma 9.A.1, to simplify naming normal (resp. regular) logics we write the Lemmon code KX ₁ … X _n (resp. CX ₁ … X _n ) to denote the smallest normal (resp. regular) logic containing formulae (X ₁), …, (X _n ) (see Bull and Segerberg 1984; Chellas 1980; Lemmon 1977). We standardly put T : = KT, S4 : = KT4 and S5 : = KT5. As it is known, T ⊊ S4 ⊊ S5, KD45 ⊊ S5, KD45 ⊈ S4 and T ⊈ KD45.

Lemma

• (i) (D) ∈ C5 _c  ⊆ K5 _c ; (D) ∈ KT.

• (ii) (5c) ∈ CD4 ⊆ KD4.

• (iii) KD4 = K45 _c and CD4 = C45 _c .

• (iv) (4) ∈ K5! .

• (v) $\mathbf{KD45} = \mathbf{K5!} ={ \mathbf{K55}}_{\mathbf{c}}$.

• (vi) In K the formula (5) is equivalent to the following formula

  $$(\lozenge p \wedge \lozenge q) \rightarrow \lozenge (p \wedge \lozenge q) $$

  (†)

Proof.

(i) ‘ ◊ (p → □ p)’ belongs to C5 _c , by (R). So, we use Lemma 9.A.7.

(ii) By (4), (US), (D) and PL we obtain that (5c) ∈ CD4.

(iii) By (i) and (ii).

For (iv) see Exercise 4.46 in Chellas (1980).

(v) By (i), (ii) and (iv).

For (vi) see Exercise 4.37 in Chellas (1980).

Notice that from Lemmas 9.A.3, 9.A.4, and 9.A.7 we obtain:

Corollary

CD5 = KD5, CD45 = KD45 and CT5 = KT5 := S5.

Thus, while defining strictly regular logics one uses some additional formulae. We adopt a convention from Segerberg (1971), p. 206. For the formula (X) and any i ≥ 0 we put (X(i)) : =  ⌜ □ ⁱ ⊤ → (X) ⌝ .

Lemma

Segerberg (1971), vol. II, Corollary 2.4. For any i > 0 :

$${\mathbf{CN}}^{\mathbf{i}}{\mathbf{X}}_{ 1}\mathbf{(i)}\ldots {\mathbf{X}}_{n}\mathbf{(i)} ={ \mathbf{CF}}^{\mathbf{i}} \cap {\mathbf{KX}}_{ 1}\ldots {\mathbf{X}}_{n}\,,$$

where

$${\square }^{i}\top \rightarrow {\square }^{i+1}\top $$

(Ni)

$${\lozenge }^{i}\neg \top $$

(Fi)

Of course, in any modal logic N ⁰ is equivalent to ⌜ □ ⊤ ⌝ ; so CN ⁰ = K.