Solovay's theorems of arithmetical adequacy for GL

One of the things that makes prov­abil­ity logic such an in­ter­est­ing for­mal sys­tem is the di­rect re­la­tion be­tween its the­o­rems and a re­stricted albeit rich class of the­o­rems re­gard­ing prov­abil­ity pred­i­cates in Peano Arith­metic.

As usual, the ad­e­quacy re­sult comes in the form of a pair of the­o­rems, prov­ing re­spec­tively sound­ness and com­plete­ness for this class. Be­fore stat­ing the re­sults, we de­scribe the way to trans­late modal sen­tences to sen­tences of ar­ith­metic, thus de­scribing the class of sen­tences of ar­ith­metic the re­sult al­ludes to.


A re­al­iza­tion \(*\) is a func­tion from the set of well-formed sen­tences of modal logic to the set of sen­tences of ar­ith­metic. In­tu­itively, we are try­ing to pre­serve the struc­ture of the sen­tence while map­ping the ex­pres­sions proper of modal logic to re­lated pred­i­cates in the lan­guage of \(PA\).


  • \(p^* = S_p\): sen­tence let­ters are mapped to ar­bi­trary closed sen­tences of ar­ith­metic.

  • \((\square A)^*=P(A^*)\): the box op­er­a­tor is mapped to a prov­abil­ity pred­i­cate \(P\), usu­ally the stan­dard prov­abil­ity pred­i­cate.

  • \((A\to B)^* = A^* \to B^*\): truth func­tional com­pounds are mapped as ex­pected.

  • \(\bot ^* = \neg X\), where \(X\) is any the­o­rem of \(PA\), for ex­am­ple, \(0\ne 1\).

The class of sen­tences of \(PA\) such that there ex­ists a modal sen­tence of which they are a re­al­iza­tion is the set for which we will prove the sound­ness and com­plete­ness.

Arith­meti­cal soundness

If \(GL\vdash A\), then \(PA\vdash A^*\) for ev­ery re­al­iza­tion \(*\).

The ap­pli­ca­tions to this re­sult are end­less. For ex­am­ple, this the­o­rem al­lows us to take ad­van­tage of the pro­ce­dures to calcu­late fixed points in \(GL\) to get re­sults about \(PA\).

To bet­ter get an in­tu­ition of how this cor­re­spon­dence works, try figur­ing out how the prop­er­ties of the prov­abil­ity pred­i­cate re­late to the ax­ioms and rules of in­fer­ence of \(GL\).


Arith­meti­cal completeness

If \(GL\not\vdash A\), then there ex­ists a re­al­iza­tion \(*\) such that \(PA\not\vdash A^*\).

The proof of ar­ith­meti­cal com­plete­ness is a beau­tiful and in­tri­cate con­struc­tion that ex­ploits the se­man­ti­cal re­la­tion­ship be­tween \(GL\) and the finite, tran­si­tive and ir­reflex­ive Kripke mod­els. Check its page for the de­tails.

Uniform ar­ith­meti­cal completeness

There ex­ists a re­al­iza­tion \(*\) such that for ev­ery modal sen­tence \(A\) we have that \(GL\not\vdash A\) only if \(PA\not\vdash A\).

This re­sult gen­er­al­izes the ar­ith­meti­cal com­plete­ness the­o­rem to a new level.