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

## Realizations

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$$.

Con­cretely,

• $$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$$.

Proof

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

Proof

Parents: