# 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!

Parents:

• Does x cor­re­spond to a state­ment (as used in the pre­vi­ous sen­tence about ex­pres­sive­ness), or does the for­mula Prv(x) cor­re­spond to a state­ment?

What’s the re­la­tion­ship be­tween a for­mula and a state­ment?

• “For­mula” and “State­ment” can be in­ter­changed freely.

Both re­fer to well-formed strings in the lan­guage of in­ter­est, in this case the lan­guage of ar­ith­metic (${+,\dot,0,1}$ and the log­i­cal sym­bols).