some theorem schemas of normal modal logic

Primary tabs

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

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)

Major Section:

Reference

Type of Math Object:

Definition

Parent:

normal modal logic

Mathematics Subject Classification

03B45 Modal logic (including the logic of norms)

Add a correction
Attach a problem
Ask a question

User menu

some theorem schemas of normal modal logic

Primary tabs

some theorem schemas of normal modal logic

Proof.

Mathematics Subject Classification

Recent Activity

Info

Versions

User menu

User login

You are here

some theorem schemas of normal modal logic

Primary tabs

some theorem schemas of normal modal logic

Proof.

Mathematics Subject Classification

Search form

Recent Activity

Info

Versions