# Provability logic

The Gödel -Löb sys­tem of prov­abil­ity logic, or $$GL$$ for short, is a nor­mal sys­tem of prov­abil­ity logic which cap­tures im­por­tant no­tions about prov­abil­ity pred­i­cates. It can be re­garded as a for­mal­ism which al­lows to de­cide whether cer­tain sen­tences in which a prov­abil­ity pred­i­cate ap­pears are in fact the­o­rems of Peano Arith­metic.

$$GL$$ has two rules of in­fer­ence:

• Mo­dus po­nens al­lows to in­fer $$B$$ from $$A\to B$$ and $$A$$.

• Ne­ces­si­ta­tion says that if $$GL\vdash A$$ then $$GL\vdash \square A$$.

The ax­ioms of $$GL$$ are as fol­lows:

• $$GL\vdash \square (A\to B)\to(\square A \to \square B)$$ (Distibu­tive ax­ioms)

• $$GL\vdash \square (\square A \to A)\to \square A$$ (Gödel-Löb ax­ioms)

• Propo­si­tional tau­tolo­gies are ax­ioms of $$GL$$.

Ex­er­cise: Show us­ing the rules of $$GL$$ that $$\square \bot \leftrightarrow \square \diamond p$$. note$$\diamond p$$ is short for $$\neg \square \neg p$$.

Those prob­lems are best solved by work­ing back­wards.

We want to show that $$GL\vdash \square \bot \leftrightarrow \square \diamond p$$.

What can lead us to that? Well, we know that be­cause of nor­mal­ity, this can be de­duced from $$GL\vdash \square (\bot \leftrightarrow \diamond p)$$.

Similarly, that can be de­rived from ne­ces­si­ta­tion of $$GL\vdash \bot \leftrightarrow \diamond p$$.

The propo­si­tional calcu­lus shows that $$GL\vdash \bot \to \diamond p$$ is a tau­tol­ogy, so we can prove by fol­low­ing the steps back­ward 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 go­ing to go for­ward from the tau­tol­ogy $$GL\vdash \bot \to \neg p$$.

By nor­mal­ity, $$GL\vdash \square \bot \to \square \neg p$$.

Con­tra­pos­ing, $$Gl\vdash \neg \square \neg p\to\neg\square\bot$$. By ne­ces­si­ta­tion and nor­mal­ity, $$Gl\vdash \square \neg \square \neg p\to\square \neg\square\bot$$.

But $$\square\neg\square\bot$$ is equiv­a­lent to $$\square[\square \bot \to \bot]$$, and it is an ax­iom that $$GL\vdash \square[\square \bot \to \bot] \to\square \bot$$, so by modus po­nens, $$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 con­sis­tent. If we in­ter­pret $$\square$$ as the verum op­er­a­tor which is always true, we re­al­ize that ev­ery the­o­rem of $$GL$$ is as­signed a value of true ac­cord­ing to this in­ter­pre­ta­tion and the usual rules of propo­si­tional calcu­lus noteproof . How­ever, there are well formed modal sen­tences such as $$\neg \square \bot$$ such that the as­signed value is false, and thus they can­not be the­o­rems of $$GL$$.

## Semantics

How­ever sim­ple the de­duc­tion pro­ce­dures of $$GL$$ are, they are both­er­some to use in or­der to find proofs. Thank­fully, an al­ter­na­tive in­ter­pre­ta­tion in terms of Kripke mod­els has been de­vel­oped that al­lows to de­cide far more con­ve­niently whether a modal sen­tence is a the­o­rem of $$GL$$.

$$GL$$ is ad­e­quate for finite, tran­si­tive and ir­reflex­ive Kripke mod­els. That is, a sen­tence $$A$$ is a the­o­rem of $$GL$$ if and only if $$A$$ is valid in ev­ery finite, tran­si­tive and ir­reflex­ive mod­elnoteproof. Check out the page on Kripke mod­els if you do not know how to con­struct Kripke mod­els or de­cide if a sen­tence is valid in it.

An im­por­tant no­tion in this kind of mod­els is that of rank. The rank $$\rho$$ of a world $$w$$ from which no world is visi­ble is $$\rho(w)=0$$. The rank of any other world is defined as the max­i­mum among the ranks of its suc­ces­sors, plus one. In other words, the rank of a world is the length of the great­est “chain of wor­lds” in the model such that $$w$$ can view the first slate of the chain.

Since mod­els are ir­reflex­ive and finite, the rank is a well-defined no­tion: no in­finite chain of wor­lds is ever pos­si­ble.

Ex­er­cise: Show that the Gödel-Löb ax­ioms are valid in ev­ery finite, tran­si­tive and ir­reflex­ive Kripke model.

Sup­pose there is a finite, tran­si­tive and ir­reflex­ive Kripke model in which an sen­tence of the form $$\square[\square A\to A]\to \square A$$ is not valid.

Let $$w$$ be the low­est 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$$.

There­fore, there ex­ists $$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$$. Com­bin­ing 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 tran­si­tivity $$wRy$$, con­tra­dict­ing that $$w\models \square[\square A\to A]$$. So the sup­po­si­tion was false, and the proof is done. <div><div>

The Kripke model for­mu­la­tion spe­cially sim­plifies rea­son­ing in cases in which no sen­tence let­ters ap­pear. A polyno­mial time al­gorithm can be writ­ten for de­cid­ing the­o­rem­hood this case.

Fur­ther­more, $$GL$$ is de­cid­able. How­ever, it is $$PSPACE$$-com­plete noteproof.

You can trans­late sen­tences of modal logic to sen­tences of ar­ith­metic us­ing re­al­iza­tions.

A re­al­iza­tion $$*$$ is a func­tion such that $$A\to B*=A*\to B*$$, $$(\square A)* =\square_{PA}(A*)$$, and $$p* = S_p$$ for ev­ery sen­tence let­ter $$p$$, where each $$S_p$$ is an ar­bi­trary well formed closed sen­tence of ar­ith­metic.

Solo­vay’s ad­e­quacy the­o­rem for GL states that a modal sen­tence $$A$$ is a the­o­rem of $$GL$$ iff $$PA$$ proves $$A*$$ for ev­ery re­al­iza­tion $$*$$.

Thus we can use $$GL$$ to rea­son about ar­ith­metic and vicev­ersa.

No­tice that $$GL$$ is de­cid­able while ar­ith­metic is not. This is ex­plained by the fact that $$GL$$ only deals with a spe­cific sub­set of log­i­cal sen­tences, in which quan­tifi­ca­tion plays a re­stricted role. In fact, quan­tified prov­abil­ity logic is un­de­cid­able.

Another re­mark is that while know­ing that $$GL\not\vdash A$$ im­plies that there is a re­al­iza­tion such that $$PA\not\vdash A*$$, we do not know whether a spe­cific re­al­iza­tion of A is a the­o­rem or not. A re­lated re­sult, the uniform com­plete­ness the­o­rem for $$GL$$, proves that there ex­ists a spe­cific re­al­iza­tion $$\#$$ such that $$PA\not \vdash A^{\#}$$ if $$GL\not\vdash A$$, which works for ev­ery $$A$$.

## Fixed points

One of the most im­por­tant re­sults in $$GL$$ is the ex­is­tence of fixed points of sen­tences of the form $$p\leftrightarrow \phi(p)$$. Con­cretely, the fixed point the­o­rem says that for ev­ery sen­tence $$\phi(p)$$ modal­ized in $$p$$ notethat is, ev­ery $$p$$ oc­curs within the scope of a $$\square$$ there ex­ists $$H$$ in which $$p$$ does not ap­pear such that $$GL\vdash \square [p\leftrightarrow \phi(p)] \leftrightarrow \square (p\leftrightarrow h)$$. Fur­ther­more, there are con­struc­tive proofs which al­low to build such an $$H$$.

In ar­ith­metic, there are plenty of in­ter­est­ing self refer­en­tial sen­tences such as the Gödel sen­tence for which the fixed point the­o­rem is ap­pli­ca­ble and gives us in­sights about their mean­ing.

For ex­am­ple, the modal­iza­tion of the Gödel sen­tence is some­thing of the form $$p\leftrightarrow \neg\square p$$. The pro­ce­dure for find­ing fixed points tells us that $$GL\vdash \square (p\leftrightarrow \neg\square p)\to \square(p\leftrightarrow \neg\square\bot$$. Thus by ar­ith­meti­cal ad­e­quacy, and since ev­ery­thing $$PA$$ proves is true we can con­clude that the Gödel sen­tence is equiv­a­lent to the con­sis­tency of ar­ith­metic.

Children:

Parents: