[summary: $~$GL\vdash A$~$ iff $~$PA\vdash A^*$~$ for every realization $~$*$~$.
Realizations are translations from modal sentences to sentences of arithmetic. ]
One of the things that makes Provability logic such an interesting formal system is the direct relation between its theorems and a restricted albeit rich class of theorems regarding provability predicates in Peano Arithmetic.
As usual, the adequacy result comes in the form of a pair of theorems, proving respectively [-soundness] and [-completeness] for this class. Before stating the results, we describe the way to [translation translate] modal sentences to sentences of arithmetic, thus describing the class of sentences of arithmetic the result alludes to.
Realizations
A realization $~$*$~$ is a function from the set of well-formed sentences of modal logic to the set of sentences of arithmetic. Intuitively, we are trying to preserve the structure of the sentence while mapping the expressions proper of modal logic to related predicates in the language of $~$PA$~$.
Concretely,
- $~$p^* = S_p$~$: sentence letters are mapped to arbitrary closed sentences of arithmetic.
- $~$(\square A)^*=P(A^*)$~$: the box operator is mapped to a Provability predicate $~$P$~$, usually the Standard provability predicate.
- $~$(A\to B)^* = A^* \to B^*$~$: truth functional compounds are mapped as expected.
- $~$\bot ^* = \neg X$~$, where $~$X$~$ is any theorem of $~$PA$~$, for example, $~$0\ne 1$~$.
The class of sentences of $~$PA$~$ such that there exists a modal sentence of which they are a realization is the set for which we will prove the soundness and completeness.
Arithmetical soundness
If $~$GL\vdash A$~$, then $~$PA\vdash A^*$~$ for every realization $~$*$~$.
The applications to this result are endless. For example, this theorem allows us to take advantage of the procedures to calculate fixed points in $~$GL$~$ to get results about $~$PA$~$.
To better get an intuition of how this correspondence works, try figuring out how the properties of the Provability predicate relate to the axioms and rules of inference of $~$GL$~$.
[ Proof]
Arithmetical completeness
If $~$GL\not\vdash A$~$, then there exists a realization $~$*$~$ such that $~$PA\not\vdash A^*$~$.
The proof of arithmetical completeness is a beautiful and intricate construction that exploits the semantical relationship between $~$GL$~$ and the finite, transitive and irreflexive Kripke models. Check [ its page] for the details.
Uniform arithmetical completeness
There exists a realization $~$*$~$ such that for every modal sentence $~$A$~$ we have that $~$GL\not\vdash A$~$ only if $~$PA\not\vdash A$~$.
This result generalizes the arithmetical completeness theorem to a new level.
[ Proof]