The Gödel -Löb system of provability logic, or $~$GL$~$ for short, is a Normal system of provability logic which captures important notions about provability predicates. It can be regarded as a formalism which allows to decide whether certain sentences in which a provability predicate appears are in fact theorems of Peano Arithmetic.
$~$GL$~$ has two rules of inference:
- Modus ponens allows to infer $~$B$~$ from $~$A\to B$~$ and $~$A$~$.
- Necessitation says that if $~$GL\vdash A$~$ then $~$GL\vdash \square A$~$.
The axioms of $~$GL$~$ are as follows:
- $~$GL\vdash \square (A\to B)\to(\square A \to \square B)$~$ (Distibutive axioms)
- $~$GL\vdash \square (\square A \to A)\to \square A$~$ (Gödel-Löb axioms)
- Propositional tautologies are axioms of $~$GL$~$.
Exercise: Show using the rules of $~$GL$~$ that $~$\square \bot \leftrightarrow \square \diamond p$~$. %%note:$~$\diamond p$~$ is short for $~$\neg \square \neg p$~$.%%
%%hidden(Show solution): Those problems are best solved by working backwards.
We want to show that $~$GL\vdash \square \bot \leftrightarrow \square \diamond p$~$.
What can lead us to that? Well, we know that because of [ normality], this can be deduced from $~$GL\vdash \square (\bot \leftrightarrow \diamond p)$~$.
Similarly, that can be derived from necessitation of $~$GL\vdash \bot \leftrightarrow \diamond p$~$.
The propositional calculus shows that $~$GL\vdash \bot \to \diamond p$~$ is a tautology, so we can prove by following the steps backward that $~$GL\vdash \square \bot \to \square \diamond p$~$.
Now we have to prove that $~$GL\vdash \square \diamond p\to \square \bot$~$ and we are done.
For that we are going to go forward from the tautology $~$GL\vdash \bot \to \neg p$~$.
By normality, $~$GL\vdash \square \bot \to \square \neg p$~$.
Contraposing, $~$Gl\vdash \neg \square \neg p\to\neg\square\bot$~$. By necessitation and normality, $~$Gl\vdash \square \neg \square \neg p\to\square \neg\square\bot$~$.
But $~$\square\neg\square\bot$~$ is equivalent to $~$\square[\square \bot \to \bot]$~$, and it is an axiom that $~$GL\vdash \square[\square \bot \to \bot] \to\square \bot$~$, so by modus ponens, $~$Gl\vdash \square \neg \square \neg p\to\square \bot$~$, and since $~$\diamond p = \neg \square \neg p$~$ we are done. %%
It is fairly easy to see that GL is consistent. If we interpret $~$\square$~$ as the verum operator which is always true, we realize that every theorem of $~$GL$~$ is assigned a value of true according to this interpretation and the usual rules of propositional calculus %%note:[ proof] %%. However, there are well formed modal sentences such as $~$\neg \square \bot$~$ such that the assigned value is false, and thus they cannot be theorems of $~$GL$~$.
Semantics
However simple the deduction procedures of $~$GL$~$ are, they are bothersome to use in order to find proofs. Thankfully, an alternative interpretation in terms of Kripke models has been developed that allows to decide far more conveniently whether a modal sentence is a theorem of $~$GL$~$.
$~$GL$~$ is adequate for finite, transitive and irreflexive Kripke models. That is, a sentence $~$A$~$ is a theorem of $~$GL$~$ if and only if $~$A$~$ is valid in every finite, transitive and irreflexive model%%note: [ proof]%%. Check out the page on Kripke models if you do not know how to construct Kripke models or decide if a sentence is valid in it.
An important notion in this kind of models is that of rank. The rank $~$\rho$~$ of a world $~$w$~$ from which no world is visible is $~$\rho(w)=0$~$. The rank of any other world is defined as the maximum among the ranks of its successors, plus one. In other words, the rank of a world is the length of the greatest "chain of worlds" in the model such that $~$w$~$ can view the first slate of the chain.
Since models are irreflexive and finite, the rank is a well-defined notion: no infinite chain of worlds is ever possible.
Exercise: Show that the Gödel-Löb axioms are valid in every finite, transitive and irreflexive Kripke model.
%%hidden(Show solution): Suppose there is a finite, transitive and irreflexive Kripke model in which an sentence of the form $~$\square[\square A\to A]\to \square A$~$ is not valid.
Let $~$w$~$ be the lowest rank world in the model such that $~$w\not\models \square[\square A\to A]\to \square A$~$. Then we have that $~$w\models \square[\square A\to A]$~$ but $~$w\not \models \square A$~$.
Therefore, there exists $~$x$~$ such that $~$w R x$~$, also $~$x\models \neg A$~$ and $~$x\models \square A\to A$~$. But then $~$x\models \neg\square A$~$.
Since $~$x$~$ has lower rank than $~$w$~$, we also have that $~$x\models \square[\square A\to A]\to \square A$~$. Combining those two last facts we get that $~$x\not\models \square[\square A\to A]$~$, so there is $~$y$~$ such that $~$xRy$~$ and $~$y\not\models \square A\to A$~$.
But by transitivity $~$wRy$~$, contradicting that $~$w\models \square[\square A\to A]$~$. So the supposition was false, and the proof is done. %%
The Kripke model formulation specially simplifies reasoning in cases in which [constant_sentences no sentence letters appear]. A polynomial time algorithm can be written for deciding theoremhood this case.
Furthermore, $~$GL$~$ is [-decidable]. However, it is [ $~$PSPACE$~$-complete] %%note:[ proof]%%.
Arithmetical adequacy
You can translate sentences of modal logic to sentences of arithmetic using realizations.
A realization $~$*$~$ is a function such that $~$A\to B*=A*\to B*$~$, $~$(\square A)* =\square_{PA}(A*)$~$, and $~$p* = S_p$~$ for every sentence letter $~$p$~$, where each $~$S_p$~$ is an arbitrary well formed closed sentence of arithmetic.
[ Solovay's adequacy theorem for GL] states that a modal sentence $~$A$~$ is a theorem of $~$GL$~$ iff $~$PA$~$ proves $~$A*$~$ for every realization $~$*$~$.
Thus we can use $~$GL$~$ to reason about arithmetic and viceversa.
Notice that $~$GL$~$ is decidable while [ arithmetic is not]. This is explained by the fact that $~$GL$~$ only deals with a specific subset of logical sentences, in which quantification plays a restricted role. In fact, quantified provability logic is undecidable.
Another remark is that while knowing that $~$GL\not\vdash A$~$ implies that there is a realization such that $~$PA\not\vdash A*$~$, we do not know whether a specific realization of A is a theorem or not. A related result, the [ uniform completeness theorem for $~$GL$~$], proves that there exists a specific realization $~$\#$~$ such that $~$PA\not \vdash A^{\#}$~$ if $~$GL\not\vdash A$~$, which works for every $~$A$~$.
Fixed points
One of the most important results in $~$GL$~$ is the existence of fixed points of sentences of the form $~$p\leftrightarrow \phi(p)$~$. Concretely, the [ fixed point theorem] says that for every sentence $~$\phi(p)$~$ modalized in $~$p$~$ %%note:that is, every $~$p$~$ occurs within the scope of a $~$\square$~$%% there exists $~$H$~$ in which $~$p$~$ does not appear such that $~$GL\vdash \square [p\leftrightarrow \phi(p)] \leftrightarrow \square (p\leftrightarrow h)$~$. Furthermore, there are constructive proofs which allow to build such an $~$H$~$.
In arithmetic, there are plenty of interesting self referential sentences such as the [godel_first_incompleteness_theorem Gödel sentence] for which the fixed point theorem is applicable and gives us insights about their meaning.
For example, the modalization of the Gödel sentence is something of the form $~$p\leftrightarrow \neg\square p$~$. The procedure for finding fixed points tells us that $~$GL\vdash \square (p\leftrightarrow \neg\square p)\to \square(p\leftrightarrow \neg\square\bot$~$. Thus by arithmetical adequacy, and since [ everything $~$PA$~$ proves is true] we can conclude that the Gödel sentence is equivalent to the consistency of arithmetic.