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

•
W: $\mathrm{\square}(\mathrm{\square}A\to A)\to \mathrm{\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 $\mathrm{\square}A\to \mathrm{\square}\mathrm{\square}A$.
Proposition 1.
In any normal modal logic, $\mathrm{\u22a2}W$ implies $\mathrm{\u22a2}\mathrm{4}$.
The proof of this requires some theorems (http://planetmath.org/SomeTheoremSchemasOfNormalModalLogic) and metatheorems (http://planetmath.org/SyntacticPropertiesOfANormalModalLogic) of a normal modal logic.
Proof.
We start with the tautology^{} $A\to ((\mathrm{\square}\mathrm{\square}A\wedge \mathrm{\square}A)\to (\mathrm{\square}A\wedge A))$, which an instance of the schema $X\to ((Y\wedge Z)\to (Z\wedge X))$. Since $\mathrm{\square}(\mathrm{\square}A\wedge A)\leftrightarrow \mathrm{\square}\mathrm{\square}A\wedge \mathrm{\square}A$ is a theorem in any normal modal logic, $A\to (\mathrm{\square}(\mathrm{\square}A\wedge A)\to (\mathrm{\square}A\wedge A))$ is a theorem by the substitution theorem. By the syntactic property RM, $\mathrm{\square}A\to \mathrm{\square}(\mathrm{\square}(\mathrm{\square}A\wedge A)\to (\mathrm{\square}A\wedge A))$ is a theorem. Since $\mathrm{\square}(\mathrm{\square}(\mathrm{\square}A\wedge A)\to (\mathrm{\square}A\wedge A))\to \mathrm{\square}(\mathrm{\square}A\wedge A)$ is an instance of W, by law of syllogism, $\mathrm{\square}A\to \mathrm{\square}(\mathrm{\square}A\wedge A)$ is a theorem.
Next, from the tautology $\mathrm{\square}A\wedge A\to \mathrm{\square}A$, we have the theorem $\mathrm{\square}(\mathrm{\square}A\wedge A)\to \mathrm{\square}\mathrm{\square}A$ by RM. Combining this with the last theorem in the previous paragraph, we see that, by law of syllogism, $\mathrm{\square}A\to \mathrm{\square}\mathrm{\square}A$, or 4, is a theorem. ∎
Corollary 1.
4 is a theorem of GL.
A binary relation^{} is said to be converse^{} wellfounded iff its inverse^{} is wellfounded.
Proposition 2.
W is valid in a frame $\mathrm{F}$ iff $\mathrm{F}$ is transitive^{} and converse wellfounded.
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 wellfounded. Suppose not. Then there is a nonempty 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$, ${\vDash \u0338}_{u}\mathrm{\square}(\mathrm{\square}p\to p)\to \mathrm{\square}p$, or equivalently, ${\vDash}_{u}\mathrm{\square}(\mathrm{\square}p\to p)$ and ${\vDash \u0338}_{u}\mathrm{\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 ${\vDash}_{u}\mathrm{\square}(\mathrm{\square}p\to p)$, we want to show that ${\vDash}_{v}\mathrm{\square}p\to p$. There are two cases:

•
If $v\in S$, then ${\vDash \u0338}_{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$, ${\vDash \u0338}_{w}p$. Since $vRw$, ${\vDash \u0338}_{v}\mathrm{\square}p$. As a result, ${\vDash}_{v}\mathrm{\square}p\to p$.

•
If $v\notin S$, then ${\vDash}_{v}p$, so that ${\vDash}_{v}\mathrm{\square}p\to p$.
Next, we want to show that ${\vDash \u0338}_{u}\mathrm{\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$, ${\vDash \u0338}_{w}p$. But since $uRw$, ${\vDash \u0338}_{u}\mathrm{\square}p$.
Conversely, let $\mathcal{F}$ be a transitive and converse wellfounded frame, $M$ a model based on $\mathcal{F}$, and $u$ a world in $M$. We want to show that ${\vDash}_{u}\mathrm{\square}(\mathrm{\square}p\to p)\to \mathrm{\square}p$. So suppose ${\vDash \u0338}_{u}\mathrm{\square}p$. Then the set $S:=\{v\mid uRv\text{and}{\vDash \u0338}_{v}p\}$ is not empty. Since $R$ is converse wellfounded, $S$ has a $R$maximal element, say $w$. So $uRw$ and ${\vDash \u0338}_{w}p$. Now, if ${\vDash}_{w}\mathrm{\square}p\to p$, then ${\vDash \u0338}_{w}\mathrm{\square}p$, which means there is a $v$ such that $wRv$ and ${\vDash \u0338}_{v}p$. But since $R$ is transitive and $uRw$, we get $uRv$, implying $v\in S$, contradicting the $R$maximality of $w$. Therefore, ${\vDash \u0338}_{w}\mathrm{\square}p\to p$, or ${\vDash \u0338}_{u}\mathrm{\square}(\mathrm{\square}p\to p)$. As a result, ${\vDash}_{u}\mathrm{\square}(\mathrm{\square}p\to p)\to \mathrm{\square}p$. ∎
Proposition^{} 2 immediately implies
Corollary 2.
GL is sound in the class of transitive and converse wellfounded frames.
Remark. However, unlike many other modal logics, GL is not complete^{} in the class of transitive and converse wellfounded frames. While its canonical model (hence the corresponding canonical frame) is transitive (because 4 is valid in it), it is not converse wellfounded.
Instead, it can be shown that GL is complete in the restricted class of finite transitive and converse wellfounded frames, or equivalently, finite transitive and irreflexive^{} frames.
Title  modal logic GL 

Canonical name  ModalLogicGL 
Date of creation  20130322 19:35:33 
Last modified on  20130322 19:35:33 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  19 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03B45 
Classification  msc 03F45 
\@unrecurse 