Provability logic

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.