modal logic GL

The modal logic GL (after Gödel and Löb) is the smallest normal modal logic containing the following schema:

• W: $\square(\square A\to A)\to\square A$.

GL is also known as provability logic, because it is used to study the provability and consistency of first order Peano arithmetic.

Recall that 4 is the schema $\square A\to\square\square A$.

Proposition 1.

In any normal modal logic, $\vdash W$ implies $\vdash 4$.

The proof of this requires some theorems (http://planetmath.org/SomeTheoremSchemasOfNormalModalLogic) and meta-theorems (http://planetmath.org/SyntacticPropertiesOfANormalModalLogic) of a normal modal logic.

Proof.

We start with the tautology $A\to((\square\square A\land\square A)\to(\square A\land A))$, which an instance of the schema $X\to((Y\land Z)\to(Z\land X))$. Since $\square(\square A\land A)\leftrightarrow\square\square A\land\square A$ is a theorem in any normal modal logic, $A\to(\square(\square A\land A)\to(\square A\land A))$ is a theorem by the substitution theorem. By the syntactic property RM, $\square A\to\square(\square(\square A\land A)\to(\square A\land A))$ is a theorem. Since $\square(\square(\square A\land A)\to(\square A\land A))\to\square(\square A% \land A)$ is an instance of W, by law of syllogism, $\square A\to\square(\square A\land A)$ is a theorem.

Next, from the tautology $\square A\land A\to\square A$, we have the theorem $\square(\square A\land A)\to\square\square A$ by RM. Combining this with the last theorem in the previous paragraph, we see that, by law of syllogism, $\square A\to\square\square A$, or 4, is a theorem. ∎

Corollary 1.

4 is a theorem of GL.

A binary relation is said to be converse well-founded iff its inverse is well-founded.

Proposition 2.

W is valid in a frame $\mathcal{F}$ iff $\mathcal{F}$ is transitive and converse well-founded.

Proof.

Suppose first that the schema W is valid in $\mathcal{F}=(U,R)$, then any theorem of GL is valid in $\mathcal{F}$, so in particular 4 is valid in $\mathcal{F}$, and hence $\mathcal{F}$ is transitive (see here (http://planetmath.org/ModalLogicS4)). We next show that $R$ is converse well-founded. Suppose not. Then there is a non-empty subset $S\subseteq U$ such that $S$ has no $R$-maximal element. We want to find a model $(U,R,V)$ such that, for some propositional variable $p$ and some world $u$ in $U$, $\not\models_{u}\square(\square p\to p)\to\square p$, or equivalently, $\models_{u}\square(\square p\to p)$ and $\not\models_{u}\square p$. Let $V$ be the valuation such that $V(p):=\{w\in U\mid w\notin S\}$. Pick any $u\in S$. Suppose $uRv$. To show that $\models_{u}\square(\square p\to p)$, we want to show that $\models_{v}\square p\to p$. There are two cases:

• If $v\in S$, then $\not\models_{v}p$. Furthermore, since $S$ does not contain an $R$-maximal element, there is a $w\in S$ such that $vRw$. Since $w\in S$, $\not\models_{w}p$. Since $vRw$, $\not\models_{v}\square p$. As a result, $\models_{v}\square p\to p$.

• If $v\notin S$, then $\models_{v}p$, so that $\models_{v}\square p\to p$.

Next, we want to show that $\not\models_{u}\square p$. Since $u\in S$, and $S$ does not have an $R$-maximal element, there is a $w\in S$ such that $uRw$. Since $w\in S$, $\not\models_{w}p$. But since $uRw$, $\not\models_{u}\square p$.

Conversely, let $\mathcal{F}$ be a transitive and converse well-founded frame, $M$ a model based on $\mathcal{F}$, and $u$ a world in $M$. We want to show that $\models_{u}\square(\square p\to p)\to\square p$. So suppose $\not\models_{u}\square p$. Then the set $S:=\{v\mid uRv\mbox{ and }\not\models_{v}p\}$ is not empty. Since $R$ is converse well-founded, $S$ has a $R$-maximal element, say $w$. So $uRw$ and $\not\models_{w}p$. Now, if $\models_{w}\square p\to p$, then $\not\models_{w}\square p$, which means there is a $v$ such that $wRv$ and $\not\models_{v}p$. But since $R$ is transitive and $uRw$, we get $uRv$, implying $v\in S$, contradicting the $R$-maximality of $w$. Therefore, $\not\models_{w}\square p\to p$, or $\not\models_{u}\square(\square p\to p)$. As a result, $\models_{u}\square(\square p\to p)\to\square p$. ∎

Proposition 2 immediately implies

Corollary 2.

GL is sound in the class of transitive and converse well-founded frames.

Remark. However, unlike many other modal logics, GL is not complete in the class of transitive and converse well-founded frames. While its canonical model (hence the corresponding canonical frame) is transitive (because 4 is valid in it), it is not converse well-founded.

Instead, it can be shown that GL is complete in the restricted class of finite transitive and converse well-founded frames, or equivalently, finite transitive and irreflexive frames.

Title modal logic GL ModalLogicGL 2013-03-22 19:35:33 2013-03-22 19:35:33 CWoo (3771) CWoo (3771) 19 CWoo (3771) Definition msc 03B45 msc 03F45