Standard provability predicate

We know that ev­ery the­ory as ex­pres­sive as min­i­mal ar­ith­metic (i.e., \(PA\)) is ca­pa­ble of talk­ing about state­ments about it­self via en­cod­ings of sen­tences of the lan­guage of ar­ith­metic into the nat­u­ral num­bers.

Of par­tic­u­lar in­ter­est is figur­ing out whether it is pos­si­ble to write a for­mula \(Prv(x)\) which is true iff there ex­ists a proof of \(x\) from the ax­ioms and rules of in­fer­ence of our the­ory.

If we re­flect on what a proof is, we will come to the con­clu­sion that a proof is a se­quence of sym­bols which fol­lows cer­tain rules. Con­cretely, it is a se­quence of strings such that ei­ther:

  1. The string is an ax­iom of the sys­tem or…

  2. The string is a the­o­rem that can be de­duced from pre­vi­ous strings of the sys­tem by ap­ply­ing a rule of in­fer­ence.

And the last string in the se­quence cor­re­sponds to the the­o­rem we want to prove.

If the ax­ioms are a com­putable set, and the rules of in­fer­ence are also effec­tively com­putable, then check­ing whether a cer­tain string is a proof of a given the­o­rem is also com­putable.

Since ev­ery com­putable set can be defined by a \(\Delta_1\)-for­mula in ar­ith­metic noteProof then we can define the \(\Delta_1\)-for­mula \(Prv(x,y)\) such that \(PA\vdash Prv(n,m)\) iff \(m\) en­codes a proof of the sen­tence of ar­ith­metic en­coded by \(n\).

Then a sen­tence \(S\) is a the­o­rem of \(PA\) if \(PA\vdash \exists y Prv(\ulcorner S \urcorner, y)\).

This for­mula is the stan­dard prov­abil­ity pred­i­cate, which we will ab­bre­vi­ate as \(\square_{PA}(x)\), and has some nice prop­er­ties which cor­re­spond to what one would ex­pect of a prov­abil­ity pred­i­cate.

How­ever, due to non-stan­dard mod­els, there are some in­tu­itions about prov­abil­ity that the stan­dard prov­abil­ity pred­i­cate fails to cap­ture. For ex­am­ple, it turns out that \(\square_{PA}A\rightarrow A\) is not always a the­o­rem of \(PA\).

There are non-stan­dard mod­els of \(PA\) which con­tain num­bers other than \(0,1,2,..\) (called non-stan­dard mod­els of ar­ith­metic). In those mod­els, the stan­dard pred­i­cate \(\square_{PA}x\) can be true even if for no nat­u­ral num­ber \(n\) it is the case that \(Prv(x,n)\). noteThis con­di­tion is called \(\omega\)-in­con­sis­tency This means that there is a non-stan­dard num­ber which satis­fies the for­mula, but non­stan­dard num­bers do not en­code stan­dard proofs!