modal logic GL

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

  • W: (AA)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 AA.

Proposition 1.

In any normal modal logic, W implies 4.

The proof of this requires some theorems ( and meta-theorems ( of a normal modal logic.


We start with the tautologyMathworldPlanetmath A((AA)(AA)), which an instance of the schema X((YZ)(ZX)). Since (AA)AA is a theorem in any normal modal logic, A((AA)(AA)) is a theorem by the substitution theorem. By the syntactic property RM, A((AA)(AA)) is a theorem. Since ((AA)(AA))(AA) is an instance of W, by law of syllogism, A(AA) is a theorem.

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

Corollary 1.

4 is a theorem of GL.

A binary relationMathworldPlanetmath is said to be converseMathworldPlanetmath well-founded iff its inversePlanetmathPlanetmathPlanetmathPlanetmath is well-founded.

Proposition 2.

W is valid in a frame F iff F is transitiveMathworldPlanetmathPlanetmathPlanetmathPlanetmath and converse well-founded.


Suppose first that the schema W is valid in =(U,R), then any theorem of GL is valid in , so in particular 4 is valid in , and hence is transitive (see here ( We next show that R is converse well-founded. Suppose not. Then there is a non-empty subset SU such that S has no R-maximal elementMathworldPlanetmath. We want to find a model (U,R,V) such that, for some propositional variable p and some world u in U, ⊧̸u(pp)p, or equivalently, u(pp) and ⊧̸up. Let V be the valuation such that V(p):={wUwS}. Pick any uS. Suppose uRv. To show that u(pp), we want to show that vpp. There are two cases:

  • If vS, then ⊧̸vp. Furthermore, since S does not contain an R-maximal element, there is a wS such that vRw. Since wS, ⊧̸wp. Since vRw, ⊧̸vp. As a result, vpp.

  • If vS, then vp, so that vpp.

Next, we want to show that ⊧̸up. Since uS, and S does not have an R-maximal element, there is a wS such that uRw. Since wS, ⊧̸wp. But since uRw, ⊧̸up.

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

PropositionPlanetmathPlanetmath 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 completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 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 irreflexiveMathworldPlanetmath 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