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

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

Let $\Lambda$ be any normal modal logic. We write $\vdash A$ to mean $\Lambda\vdash A$, or wff $A\in\Lambda$, or $A$ is a theorem of $\Lambda$. In addition, for any set $\Delta$, $\Delta\vdash A$ means there is a finite sequence of wff’s such that each wff is either a theorem, a member of $\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 $\Delta$.

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

1. 1.

   (RM) $\vdash A\to B$ implies $\vdash\square A\to\square B$

   Proof.

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

2. 2.

   As a result, $\vdash A\leftrightarrow B$ implies $\vdash\square A\leftrightarrow\square B$.

3. 3.

   (substitution theorem). If $\vdash B_{i}\leftrightarrow C_{i}$ for $i=1,\ldots,m$, then

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

   where $\overline{p}:=(p_{1},\ldots,p_{m})$ is the tuple of all the propositional variables in $A$ listed in order.

   Proof.

   For most of the proof, consult this entry for more detail. What remains is the case when $A$ has the form $\square D$. We do induction on the number $n$ of $\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$ $\square$’s. Then $D$ has $n$ $\square$’s, and so by induction, $\vdash D[B/p]\leftrightarrow D[C/p]$, and therefore $\vdash\square D[B/p]\leftrightarrow\square D[C/p]$ by 2. This means that $\vdash A[B/p]\leftrightarrow A[C/p]$. ∎

4. 4.

   $\vdash A\to B$ implies $\vdash\diamond A\to\diamond B$

   Proof.

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

5. 5.

   $\vdash A\lor B$ implies $\vdash\diamond A\lor\square B$

   Proof.

   Since $\vdash A\lor B\leftrightarrow(\neg A\to B)$, we have $\vdash\neg A\to B$, so $\vdash\square\neg A\to\square B$. By the tautology $C\leftrightarrow\neg\neg C$, we have $\vdash\neg\neg\square\neg A\to\square B$, or $\vdash\neg\diamond A\to\square B$, and therefore $\vdash\diamond A\lor\square B$. ∎

6. 6.

   (RR) $\vdash A\land B\to C$ implies $\vdash\square A\land\square B\to\square C$

   Proof.

   By assumption and 1, $\vdash\square(A\land B)\to\square C$. Since $\square A\land\square B\to\square(A\land B)$ is a theorem (see here), we get $\vdash\square A\land\square B\to\square C$ by the law of syllogism. ∎

7. 7.

   (RK) More generally, $\vdash A_{1}\land\cdots\land A_{n}\to A$ implies $\vdash\square A_{1}\land\cdots\square A_{n}\to\square A$, where the case $n=0$ is the necessitation rule.

   Proof.

   Cases $n=1,2$ are meta-theorems 1 and 6. If $\vdash A_{1}\land\cdots\land A_{n}\land A_{{n+1}}\to A$, or $\vdash(A_{1}\land\cdots\land A_{n})\land A_{{n+1}}\to A$, then $\vdash\square(A_{1}\land\cdots\land A_{n})\land\square A_{{n+1}}\to\square A$ by 6. But $\vdash\square(A_{1}\land\cdots\land A_{n})\leftrightarrow\square A_{1}\land\cdots\land\square A_{n}$, the result follows. ∎

8. 8.

   Define a function $s$ on $\{\neg,\lambda\}$, where $\lambda$ is the empty word, such that $s(\neg)=\lambda$, the empty word, and $s(\lambda)=\neg$. Then for any wff $A$, and $\epsilon_{1},\epsilon_{2}\in\{\neg,\lambda\}$:

   $$\vdash\epsilon_{1}\square^{n}\epsilon_{2}A\leftrightarrow s(\epsilon_{1})\diamond^{n}s(\epsilon_{2})A.$$

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

   Proof.

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

9. 9.

   Let $\square\Delta:=\{\square A\mid A\in\Delta\}$. Then $\Delta\vdash A$ implies $\square\Delta\vdash\square A$.

   Proof.

   Induct on the length $n$ of deduction of $A$ from $\Delta$. If $n=0$, then either $\vdash A$, in which case $\vdash\square A$ by necessitation, or $A\in\Delta$, in which case $\square A\in\square\Delta$. In either case, $\square\Delta\vdash\square A$. Next suppose the property holds for all deductions of length $n$, and there is a deduction $\mathcal{E}$ of $A$ of length $n+1$. If $A$ is obtained from $\Delta$ by necessitation, say $A$ is $\square B$, where $B$ is in $\mathcal{E}$, then a subsequence of $\mathcal{E}$ is a deduction of $B$ of length $\leq n$, from $\Delta$. So by induction, $\square\Delta\vdash\square B$, or $\square\Delta\vdash A$. By necessitation, $\square\Delta\vdash\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 $\mathcal{E}$. By induction, $\square\Delta\vdash\square B$ and $\square\Delta\vdash\square(B\to A)$, which, by K and modus ponens, $\square\Delta\vdash\square B\to\square A$, and as a result, $\square\Delta\vdash\square A$ by modus ponens. ∎

Noticeably absent is the deduction theorem, for the necessitation rule says $A\vdash\square A$, but this does not imply $\vdash A\to\square A$. In fact, the wff $A\to\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. 10.

   (deduction theorem) If $\Delta,A\vdash B$ and $B$ is not of the form $\square C$, then $\Delta\vdash 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.