syntactic properties of a 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$ . 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.

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

As a result, $\vdash A\leftrightarrow B$ implies $\vdash\square A\leftrightarrow\square B$ .
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 (http://planetmath.org/SubstitutionTheoremForPropositionalLogic) 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.

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

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

(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 (http://planetmath.org/SomeTheoremSchemasOfNormalModalLogic)), we get $\vdash\square A\land\square B\to\square C$ by the law of syllogism. ∎
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.

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.

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:

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 (http://planetmath.org/EquivalentFormulationsOfNormality).

Title	syntactic properties of a normal modal logic
Canonical name	SyntacticPropertiesOfANormalModalLogic
Date of creation	2013-03-22 19:34:18
Last modified on	2013-03-22 19:34:18
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	24
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03B45

syntactic properties of a normal modal logic

Proof.

Proof.

Proof.

Proof.

Proof.

Proof.

Proof.

Proof.