syntactic properties of a normal modal logic

Recall that a normal modal logic is a logic containing all tautologies, the schema K

$$\mathrm{\square }(A\to B)\to (\mathrm{\square }A\to \mathrm{\square }B),$$

and closed under modus ponens and necessitation rules. Also, the modal operator diamond $\diamond$ is defined as

$$\diamond A:=\mathrm{\neg }\mathrm{\square }\mathrm{\neg }A.$$

Let $\mathrm{\Lambda }$ be any normal modal logic. We write $⊢A$ to mean $\mathrm{\Lambda }⊢A$, or wff $A\in \mathrm{\Lambda }$, or $A$ is a theorem of $\mathrm{\Lambda }$. In addition, for any set $\mathrm{\Delta }$, $\mathrm{\Delta }⊢A$ means there is a finite sequence of wff’s such that each wff is either a theorem, a member of $\mathrm{\Delta }$, or obtained either by modus ponens or necessitation from earlier wff’s in the sequence, and $A$ is the last wff in the sequence. The sequence is called a deduction (of $A$) from $\mathrm{\Delta }$.

Below are some useful meta-theorems of $\mathrm{\Lambda }$:

1. (RM) $⊢A\to B$ implies $⊢\mathrm{\square }A\to \mathrm{\square }B$

   Proof.

   By assumption and by necessitation, $⊢\mathrm{\square }(A\to B)$, by schema K and by modus ponens, we have the result.∎

2. As a result, $⊢A\leftrightarrow B$ implies $⊢\mathrm{\square }A\leftrightarrow \mathrm{\square }B$.

3. (substitution theorem). If $⊢B_i\leftrightarrow C_i$ for $i=1,\mathrm{\dots },m$, then

   $$⊢A[\overline{B}/\overline{p}]\leftrightarrow A[\overline{C}/\overline{p}],$$

   where $\overline{p}:=(p_1,\mathrm{\dots },p_m)$ is the tuple of all the propositional variables in $A$ listed in order.

   Proof.

   For most of the proof, consult this entry (http://planetmath.org/SubstitutionTheoremForPropositionalLogic) for more detail. What remains is the case when $A$ has the form $\mathrm{\square }D$. We do induction on the number $n$ of $\mathrm{\square }$’s in $A$. The case when $n=0$ means that $A$ is a wff of PL${}_c$, and has already been proved. Now suppose $A$ has $n+1$ $\mathrm{\square }$’s. Then $D$ has $n$ $\mathrm{\square }$’s, and so by induction, $⊢D[B/p]\leftrightarrow D[C/p]$, and therefore $⊢\mathrm{\square }D[B/p]\leftrightarrow \mathrm{\square }D[C/p]$ by 2. This means that $⊢A[B/p]\leftrightarrow A[C/p]$.∎

4. $⊢A\to B$ implies $⊢\diamond A\to \diamond B$

   Proof.

   By assumption, tautology $⊢(A\to B)\to (\mathrm{\neg }B\to \mathrm{\neg }A)$, and modus ponens, we get $⊢\mathrm{\neg }B\to \mathrm{\neg }A$. By 1, $⊢\mathrm{\square }\mathrm{\neg }B\to \mathrm{\square }\mathrm{\neg }A$. By another instance of the above tautology and modus ponens, and the definition of $\diamond$, we get the result.∎

5. $⊢A\vee B$ implies $⊢\diamond A\vee \mathrm{\square }B$

   Proof.

   Since $⊢A\vee B\leftrightarrow (\mathrm{\neg }A\to B)$, we have $⊢\mathrm{\neg }A\to B$, so $⊢\mathrm{\square }\mathrm{\neg }A\to \mathrm{\square }B$. By the tautology $C\leftrightarrow \mathrm{\neg }\mathrm{\neg }C$, we have $⊢\mathrm{\neg }\mathrm{\neg }\mathrm{\square }\mathrm{\neg }A\to \mathrm{\square }B$, or $⊢\mathrm{\neg }\diamond A\to \mathrm{\square }B$, and therefore $⊢\diamond A\vee \mathrm{\square }B$.∎

6. (RR) $⊢A\wedge B\to C$ implies $⊢\mathrm{\square }A\wedge \mathrm{\square }B\to \mathrm{\square }C$

   Proof.

   By assumption and 1, $⊢\mathrm{\square }(A\wedge B)\to \mathrm{\square }C$. Since $\mathrm{\square }A\wedge \mathrm{\square }B\to \mathrm{\square }(A\wedge B)$ is a theorem (see here (http://planetmath.org/SomeTheoremSchemasOfNormalModalLogic)), we get $⊢\mathrm{\square }A\wedge \mathrm{\square }B\to \mathrm{\square }C$ by the law of syllogism.∎

7. (RK) More generally, $⊢A_1\wedge \mathrm{\cdots }\wedge A_n\to A$ implies $⊢\mathrm{\square }{A}_1\wedge \mathrm{\cdots }\mathrm{\square }{A}_n\to \mathrm{\square }A$, where the case $n=0$ is the necessitation rule.

   Proof.

   Cases $n=1,2$ are meta-theorems 1 and 6. If $⊢A_1\wedge \mathrm{\cdots }\wedge A_n\wedge A_{n+1}\to A$, or $⊢(A_1\wedge \mathrm{\cdots }\wedge A_n)\wedge A_{n+1}\to A$, then $⊢\mathrm{\square }(A_1\wedge \mathrm{\cdots }\wedge A_n)\wedge \mathrm{\square }{A}_{n+1}\to \mathrm{\square }A$ by 6. But $⊢\mathrm{\square }(A_1\wedge \mathrm{\cdots }\wedge A_n)\leftrightarrow \mathrm{\square }{A}_1\wedge \mathrm{\cdots }\wedge \mathrm{\square }{A}_n$, the result follows.∎

8. Define a function $s$ on $\{\mathrm{\neg },\lambda \}$, where $\lambda$ is the empty word, such that $s(\mathrm{\neg })=\lambda$, the empty word, and $s(\lambda )=\mathrm{\neg }$. Then for any wff $A$, and ${ϵ}_1,{ϵ}_2\in \{\mathrm{\neg },\lambda \}$:

   $$⊢{ϵ}_1{\mathrm{\square }}^n{ϵ}_{2}A\leftrightarrow s({ϵ}_1){\diamond }^{n}s({ϵ}_2)A.$$

   Technically speaking, this is really an infinite collection of theorem schemas.

   Proof.

   We will check the case when ${ϵ}_1=\mathrm{\neg }$ and ${ϵ}_2=\lambda$ and leave the rest to the reader. We do induction on $n$. If $n=0$, then we have the tautology $\mathrm{\neg }A\leftrightarrow \mathrm{\neg }A$. Suppose $⊢\mathrm{\neg }{\mathrm{\square }}^{n}A\leftrightarrow {\diamond }^n\mathrm{\neg }A$. Then $⊢\mathrm{\neg }{\mathrm{\square }}^{n+1}A\leftrightarrow {\diamond }^n\mathrm{\neg }\mathrm{\square }A$, by applying the induction case on wff $\mathrm{\square }A$. Since $A\leftrightarrow \mathrm{\neg }\mathrm{\neg }A$ is a tautology, $⊢\mathrm{\neg }{\mathrm{\square }}^{n+1}A\leftrightarrow {\diamond }^n\mathrm{\neg }\mathrm{\square }\mathrm{\neg }\mathrm{\neg }A$ by the substitution theorem. By the definition of $\diamond$, we have $⊢\mathrm{\neg }{\mathrm{\square }}^{n+1}A\leftrightarrow {\diamond }^{n+1}\mathrm{\neg }A$.∎

9. Let $\mathrm{\square }\mathrm{\Delta }:=\{\mathrm{\square }A\mid A\in \mathrm{\Delta }\}$. Then $\mathrm{\Delta }⊢A$ implies $\mathrm{\square }\mathrm{\Delta }⊢\mathrm{\square }A$.

   Proof.

   Induct on the length $n$ of deduction of $A$ from $\mathrm{\Delta }$. If $n=0$, then either $⊢A$, in which case $⊢\mathrm{\square }A$ by necessitation, or $A\in \mathrm{\Delta }$, in which case $\mathrm{\square }A\in \mathrm{\square }\mathrm{\Delta }$. In either case, $\mathrm{\square }\mathrm{\Delta }⊢\mathrm{\square }A$. Next suppose the property holds for all deductions of length $n$, and there is a deduction $ℰ$ of $A$ of length $n+1$. If $A$ is obtained from $\mathrm{\Delta }$ by necessitation, say $A$ is $\mathrm{\square }B$, where $B$ is in $ℰ$, then a subsequence of $ℰ$ is a deduction of $B$ of length $\le n$, from $\mathrm{\Delta }$. So by induction, $\mathrm{\square }\mathrm{\Delta }⊢\mathrm{\square }B$, or $\mathrm{\square }\mathrm{\Delta }⊢A$. By necessitation, $\mathrm{\square }\mathrm{\Delta }⊢\mathrm{\square }A$. Finally, if $A$ is obtained by modus ponens, then there is a wff $B$ such that $B,B\to A$ are both in $ℰ$. By induction, $\mathrm{\square }\mathrm{\Delta }⊢\mathrm{\square }B$ and $\mathrm{\square }\mathrm{\Delta }⊢\mathrm{\square }(B\to A)$, which, by K and modus ponens, $\mathrm{\square }\mathrm{\Delta }⊢\mathrm{\square }B\to \mathrm{\square }A$, and as a result, $\mathrm{\square }\mathrm{\Delta }⊢\mathrm{\square }A$ by modus ponens.∎

Noticeably absent is the deduction theorem, for the necessitation rule says $A⊢\mathrm{\square }A$, but this does not imply $⊢A\to \mathrm{\square }A$. In fact, the wff $A\to \mathrm{\square }A$ is not a theorem in general, unless of course the logic includes the entire schema. All we can say is the following:

1. (deduction theorem) If $\mathrm{\Delta },A⊢B$ and $B$ is not of the form $\mathrm{\square }C$, then $\mathrm{\Delta }⊢A\to B$.

Remark. It can be shown that conversely, if a modal logic obeys meta-theorem 7 above as an inference rule, then it is normal. For more detail, see here (http://planetmath.org/EquivalentFormulationsOfNormality).