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.

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

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

$\square\neg\perp$
4.

$\square A\leftrightarrow\neg\diamond\neg A$
5.

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

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

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

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

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

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

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

Proof.

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.

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.

From the tautology $\neg\perp$ , we have the result by necessitation.
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.

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.

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.

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.

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.

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.

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.

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
Canonical name	SomeTheoremSchemasOfNormalModalLogic
Date of creation	2013-03-22 19:34:26
Last modified on	2013-03-22 19:34:26
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	12
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03B45