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 $u R v$ . 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 $v R w$ . Since $w\in S$ , $\not\models_{w}p$ . Since $v R w$ , $\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 $u R w$ . Since $w\in S$ , $\not\models_{w}p$ . But since $u R w$ , $\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 $u R w$ 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 $w R v$ and $\not\models_{v}p$ . But since $R$ is transitive and $u R w$ , we get $u R v$ , 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
Canonical name	ModalLogicGL
Date of creation	2013-03-22 19:35:33
Last modified on	2013-03-22 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