# some theorem schemas of normal modal logic

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

 $\square(A\to B)\to(\square A\to\square B),$

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

 $\diamond A:=\neg\square\neg A.$

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$.

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

1. 1.

$\square(A\land B)\to\square A\land\square B$

2. 2.

$\square A\land\square B\to\square(A\land B)$

3. 3.

$\square\neg\perp$

4. 4.

$\square A\leftrightarrow\neg\diamond\neg A$

5. 5.

$\square(A\to B)\to(\diamond A\to\diamond B)$

6. 6.

$\diamond(A\to B)\to(\square A\to\diamond B)$

7. 7.

$\diamond A\land\square B\to\diamond(A\land B)$

8. 8.

$\square A\lor\square B\to\square(A\lor B)$

9. 9.

$\diamond(A\land B)\to\diamond A\land\diamond B$

10. 10.

$\square(A\lor B)\to\square A\lor\diamond B$

11. 11.

$\diamond(A\lor B)\leftrightarrow\diamond A\lor\diamond B$

###### Proof.
1. 1.

From tautologies $A\land B\to A$ and $A\land B\to B$ and meta-theorem 1, we get $\vdash\square(A\land B)\to\square A$ and $\vdash\square(A\land B)\to\square B$. So $\vdash\square(A\land B)\to\square A\land\square B$.

2. 2.

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

 $\vdash\square A\to\square(B\to(A\land B)).$

From the K instance

 $\square(B\to(A\land B))\to(\square B\to\square(A\land B))$

and the tautology

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

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

3. 3.

From the tautology $\neg\perp$, we have the result by necessitation.

4. 4.

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

5. 5.

To show $\square(A\to B)\to(\diamond A\to\diamond B)$, it is enough to show $\square(A\to B)\to(\square\neg A\lor\diamond B)$, which is enough to show $\square(A\to B)\to(\square\neg B\to\square\neg A)$, which is enough to show $\square(\neg B\to\neg A)\to(\square\neg B\to\square\neg A)$, which is just an instance of K.

6. 6.

To show $\diamond(A\to B)\to(\square A\to\diamond B)$, it is enough to show $\neg\square(A\land\neg B)\to(\square A\to\diamond B)$, which is enough to show $\neg(\square A\land\square\neg B)\to(\square A\to\diamond B)$ by 1 and 2, which is enough to show $\neg\square A\lor\diamond B\to(\square A\to\diamond B)$, which is just $(\square A\to\diamond B)\to(\square A\to\diamond B)$.

7. 7.

To show $\diamond A\land\square B\to\diamond(A\land B)$, it is enough to show $\neg\square\neg A\land\square B\to\diamond(A\land B)$, which is enough to show $\neg(\neg\square B\lor\square\neg A)\to\diamond(A\land B)$, which is enough to show $\neg(\square B\to\square\neg A)\to\neg\square\neg(A\land B)$, which is enough to show $\square\neg(A\land B)\to(\square B\to\square\neg A)$, which is enough to show $\square(\neg A\lor\neg B)\to(\square B\to\square\neg A)$, which is enough to show $\square(B\to\neg A)\to(\square B\to\square\neg A)$, which is an instance of K.

8. 8.

Since $\vdash A\to A\lor B$ and $B\vdash A\lor B$, $\square A\to\square(A\lor B)$ and $\square B\to\square(A\lor B)$, and therefore $\square A\lor\square B\to\square(A\lor B)$.

9. 9.

By 8, $\square\neg A\lor\square\neg B\to\square(\neg A\lor\neg B)$, so $\neg\square(\neg A\lor\neg B)\to\neg(\square\neg A\lor\square\neg B)$, whence $\diamond(A\land B)\to\diamond A\land\diamond B$.

10. 10.

To show $\square(A\lor B)\to\square A\lor\diamond B$, it is enough to show $\square(\neg B\to A)\to\square A\lor\diamond B$, which is enough to show $\square(\neg B\to A)\to\neg\square\neg B\lor\square A$, or $\square(\neg B\to A)\to\square\neg B\to\square A$, an instance of K.

11. 11.

From $A\to A\lor B$ and $B\to A\lor B$, we get $\diamond A\to\diamond(A\lor B)$ and $\diamond B\to\diamond(A\lor B)$, so that $\diamond A\lor\diamond B\to\diamond(A\lor B)$. On the other hand, from $\square\neg A\land\square\neg B\to\square(\neg A\land\neg B)$, we get $\neg\square(\neg A\land\neg B)\to\neg(\square\neg A\land\square\neg B)$, or $\diamond(A\lor B)\to\diamond A\lor\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 $\#5$ is

 an instance of K $\displaystyle\qquad\square(\neg B\to\neg A)\to(\square\neg B\to\square\neg A)$ (1) $\displaystyle\mbox{tautology }(p\to q)\to(\neg q\to\neg p)$ $\displaystyle(A\to B)\to(\neg B\to\neg A)$ (2) meta-theorem 1 applied to (2) $\displaystyle\square(A\to B)\to\square(\neg B\to\neg A)$ (3) law of syllogism on (3) to (1) $\displaystyle\square(A\to B)\to(\square\neg B\to\square\neg A)$ (4) $\displaystyle\mbox{definition of }\lor$ $\displaystyle\square(A\to B)\to(\neg\square\neg B\lor\square\neg A)$ (5) $\displaystyle\mbox{definition of }\diamond$ $\displaystyle\square(A\to B)\to(\diamond B\lor\square\neg A)$ (6) $\displaystyle\mbox{a tautology }p\land q\to q\land p$ $\displaystyle\diamond B\lor\square\neg A\to\square\neg A\lor\diamond B$ (7) law of syllogism on (7) to (6) $\displaystyle\square(A\to B)\to(\square\neg A\lor\diamond B)$ (8) $\displaystyle\mbox{a tautology }p\leftrightarrow\neg\neg p$ $\displaystyle\square\neg A\leftrightarrow\neg\neg\square\neg A$ (9) substitution theorem on (8) by (9) $\displaystyle\square(A\to B)\to(\neg\neg\square\neg A\lor\diamond B)$ (10) $\displaystyle\mbox{definition of }\diamond$ $\displaystyle\square(A\to B)\to(\neg\diamond A\lor\diamond B)$ (11) $\displaystyle\mbox{definition of }\lor$ $\displaystyle\square(A\to B)\to(\diamond A\to\diamond B)$ (12)
Title some theorem schemas of normal modal logic SomeTheoremSchemasOfNormalModalLogic 2013-03-22 19:34:26 2013-03-22 19:34:26 CWoo (3771) CWoo (3771) 12 CWoo (3771) Definition msc 03B45