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$.

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. <div><div>

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 noteproof . 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 modelnoteproof. 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.

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. <div><div>

The Kripke model formulation specially simplifies reasoning in cases in which 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 noteproof.

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$ notethat 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 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.