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\).


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.

Arith­meti­cal adequacy

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.