some theorem schemas of 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 }$.

Based on some of the meta-theorems of $\mathrm{\Lambda }$ (see here (http://planetmath.org/SyntacticPropertiesOfANormalModalLogic)), we can easily derive the following theorem schemas:

1. $\mathrm{\square }(A\wedge B)\to \mathrm{\square }A\wedge \mathrm{\square }B$

2. $\mathrm{\square }A\wedge \mathrm{\square }B\to \mathrm{\square }(A\wedge B)$

3. $\mathrm{\square }\mathrm{\neg }⟂$

4. $\mathrm{\square }A\leftrightarrow \mathrm{\neg }\diamond \mathrm{\neg }A$

5. $\mathrm{\square }(A\to B)\to (\diamond A\to \diamond B)$

6. $\diamond (A\to B)\to (\mathrm{\square }A\to \diamond B)$

7. $\diamond A\wedge \mathrm{\square }B\to \diamond (A\wedge B)$

8. $\mathrm{\square }A\vee \mathrm{\square }B\to \mathrm{\square }(A\vee B)$

9. $\diamond (A\wedge B)\to \diamond A\wedge \diamond B$

10. $\mathrm{\square }(A\vee B)\to \mathrm{\square }A\vee \diamond B$

11. $\diamond (A\vee B)\leftrightarrow \diamond A\vee \diamond B$

Proof.

1. From tautologies $A\wedge B\to A$ and $A\wedge B\to B$ and meta-theorem 1, we get $⊢\mathrm{\square }(A\wedge B)\to \mathrm{\square }A$ and $⊢\mathrm{\square }(A\wedge B)\to \mathrm{\square }B$. So $⊢\mathrm{\square }(A\wedge B)\to \mathrm{\square }A\wedge \mathrm{\square }B$.

2. From tautology $A\to (B\to (A\wedge B))$ and meta-theorem 1, we get

   $$⊢\mathrm{\square }A\to \mathrm{\square }(B\to (A\wedge B)).$$

   From the K instance

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

   and the tautology

   $$(p\to q)\to ((q\to (r\to s))\to ((p\wedge r)\to s))$$

   substituting $p$ for $\mathrm{\square }A$, $q$ for $\mathrm{\square }(B\to (A\wedge B))$, $r$ for $\mathrm{\square }B$, and $s$ for $\mathrm{\square }(A\wedge B)$, and applying modus ponens twice, we get the result.

3. From the tautology $\mathrm{\neg }⟂$, we have the result by necessitation.

4. All we need is $⊢\mathrm{\square }A\to \mathrm{\neg }\diamond \mathrm{\neg }A$. From tautology $A\to \mathrm{\neg }\mathrm{\neg }A$, we get $⊢\mathrm{\square }A\to \mathrm{\square }\mathrm{\neg }\mathrm{\neg }A$ by meta-theorem 1. From tautology $\mathrm{\square }\mathrm{\neg }\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }\mathrm{\square }\mathrm{\neg }\mathrm{\neg }A$ and the definition of $\diamond$, we get $⊢\mathrm{\square }A\to \mathrm{\neg }\diamond \mathrm{\neg }A$.

5. To show $\mathrm{\square }(A\to B)\to (\diamond A\to \diamond B)$, it is enough to show $\mathrm{\square }(A\to B)\to (\mathrm{\square }\mathrm{\neg }A\vee \diamond B)$, which is enough to show $\mathrm{\square }(A\to B)\to (\mathrm{\square }\mathrm{\neg }B\to \mathrm{\square }\mathrm{\neg }A)$, which is enough to show $\mathrm{\square }(\mathrm{\neg }B\to \mathrm{\neg }A)\to (\mathrm{\square }\mathrm{\neg }B\to \mathrm{\square }\mathrm{\neg }A)$, which is just an instance of K.

6. To show $\diamond (A\to B)\to (\mathrm{\square }A\to \diamond B)$, it is enough to show $\mathrm{\neg }\mathrm{\square }(A\wedge \mathrm{\neg }B)\to (\mathrm{\square }A\to \diamond B)$, which is enough to show $\mathrm{\neg }(\mathrm{\square }A\wedge \mathrm{\square }\mathrm{\neg }B)\to (\mathrm{\square }A\to \diamond B)$ by 1 and 2, which is enough to show $\mathrm{\neg }\mathrm{\square }A\vee \diamond B\to (\mathrm{\square }A\to \diamond B)$, which is just $(\mathrm{\square }A\to \diamond B)\to (\mathrm{\square }A\to \diamond B)$.

7. To show $\diamond A\wedge \mathrm{\square }B\to \diamond (A\wedge B)$, it is enough to show $\mathrm{\neg }\mathrm{\square }\mathrm{\neg }A\wedge \mathrm{\square }B\to \diamond (A\wedge B)$, which is enough to show $\mathrm{\neg }(\mathrm{\neg }\mathrm{\square }B\vee \mathrm{\square }\mathrm{\neg }A)\to \diamond (A\wedge B)$, which is enough to show $\mathrm{\neg }(\mathrm{\square }B\to \mathrm{\square }\mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\square }\mathrm{\neg }(A\wedge B)$, which is enough to show $\mathrm{\square }\mathrm{\neg }(A\wedge B)\to (\mathrm{\square }B\to \mathrm{\square }\mathrm{\neg }A)$, which is enough to show $\mathrm{\square }(\mathrm{\neg }A\vee \mathrm{\neg }B)\to (\mathrm{\square }B\to \mathrm{\square }\mathrm{\neg }A)$, which is enough to show $\mathrm{\square }(B\to \mathrm{\neg }A)\to (\mathrm{\square }B\to \mathrm{\square }\mathrm{\neg }A)$, which is an instance of K.

8. Since $⊢A\to A\vee B$ and $B⊢A\vee B$, $\mathrm{\square }A\to \mathrm{\square }(A\vee B)$ and $\mathrm{\square }B\to \mathrm{\square }(A\vee B)$, and therefore $\mathrm{\square }A\vee \mathrm{\square }B\to \mathrm{\square }(A\vee B)$.

9. By 8, $\mathrm{\square }\mathrm{\neg }A\vee \mathrm{\square }\mathrm{\neg }B\to \mathrm{\square }(\mathrm{\neg }A\vee \mathrm{\neg }B)$, so $\mathrm{\neg }\mathrm{\square }(\mathrm{\neg }A\vee \mathrm{\neg }B)\to \mathrm{\neg }(\mathrm{\square }\mathrm{\neg }A\vee \mathrm{\square }\mathrm{\neg }B)$, whence $\diamond (A\wedge B)\to \diamond A\wedge \diamond B$.

10. To show $\mathrm{\square }(A\vee B)\to \mathrm{\square }A\vee \diamond B$, it is enough to show $\mathrm{\square }(\mathrm{\neg }B\to A)\to \mathrm{\square }A\vee \diamond B$, which is enough to show $\mathrm{\square }(\mathrm{\neg }B\to A)\to \mathrm{\neg }\mathrm{\square }\mathrm{\neg }B\vee \mathrm{\square }A$, or $\mathrm{\square }(\mathrm{\neg }B\to A)\to \mathrm{\square }\mathrm{\neg }B\to \mathrm{\square }A$, an instance of K.

11. From $A\to A\vee B$ and $B\to A\vee B$, we get $\diamond A\to \diamond (A\vee B)$ and $\diamond B\to \diamond (A\vee B)$, so that $\diamond A\vee \diamond B\to \diamond (A\vee B)$. On the other hand, from $\mathrm{\square }\mathrm{\neg }A\wedge \mathrm{\square }\mathrm{\neg }B\to \mathrm{\square }(\mathrm{\neg }A\wedge \mathrm{\neg }B)$, we get $\mathrm{\neg }\mathrm{\square }(\mathrm{\neg }A\wedge \mathrm{\neg }B)\to \mathrm{\neg }(\mathrm{\square }\mathrm{\neg }A\wedge \mathrm{\square }\mathrm{\neg }B)$, or $\diamond (A\vee B)\to \diamond A\vee \diamond B$, and the result follows.

∎

Remark. The proofs are condensed for the sake of space. Properly, a formal proof should lay out the sequence of wff’s and their derivations. For example, the proof for $\mathrm{\#}5$ is

an instance of K$\mathrm{\hspace{1em}\hspace{1em}}\mathrm{\square }(\mathrm{\neg }B\to \mathrm{\neg }A)\to (\mathrm{\square }\mathrm{\neg }B\to \mathrm{\square }\mathrm{\neg }A)$(1)

$\text{tautology }(p\to q)\to (\mathrm{\neg }q\to \mathrm{\neg }p)$$(A\to B)\to (\mathrm{\neg }B\to \mathrm{\neg }A)$(2)

meta-theorem 1 applied to (2)$\mathrm{\square }(A\to B)\to \mathrm{\square }(\mathrm{\neg }B\to \mathrm{\neg }A)$(3)

law of syllogism on (3) to (1)$\mathrm{\square }(A\to B)\to (\mathrm{\square }\mathrm{\neg }B\to \mathrm{\square }\mathrm{\neg }A)$(4)

$\text{definition of }\vee$$\mathrm{\square }(A\to B)\to (\mathrm{\neg }\mathrm{\square }\mathrm{\neg }B\vee \mathrm{\square }\mathrm{\neg }A)$(5)

$\text{definition of }\diamond$$\mathrm{\square }(A\to B)\to (\diamond B\vee \mathrm{\square }\mathrm{\neg }A)$(6)

$\text{a tautology }p\wedge q\to q\wedge p$$\diamond B\vee \mathrm{\square }\mathrm{\neg }A\to \mathrm{\square }\mathrm{\neg }A\vee \diamond B$(7)

law of syllogism on (7) to (6)$\mathrm{\square }(A\to B)\to (\mathrm{\square }\mathrm{\neg }A\vee \diamond B)$(8)

$\text{a tautology }p\leftrightarrow \mathrm{\neg }\mathrm{\neg }p$$\mathrm{\square }\mathrm{\neg }A\leftrightarrow \mathrm{\neg }\mathrm{\neg }\mathrm{\square }\mathrm{\neg }A$(9)

substitution theorem on (8) by (9)$\mathrm{\square }(A\to B)\to (\mathrm{\neg }\mathrm{\neg }\mathrm{\square }\mathrm{\neg }A\vee \diamond B)$(10)

$\text{definition of }\diamond$$\mathrm{\square }(A\to B)\to (\mathrm{\neg }\diamond A\vee \diamond B)$(11)

$\text{definition of }\vee$$\mathrm{\square }(A\to B)\to (\diamond A\to \diamond B)$(12)