You are here
Homemodal logic GL
Primary tabs
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 and metatheorems 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 wellfounded iff its inverse is wellfounded.
Proposition 2.
W is valid in a frame $\mathcal{F}$ iff $\mathcal{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). 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$, $\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 wellfounded 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 wellfounded, $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 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.
Mathematics Subject Classification
03B45 no label found03F45 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections