Solovay's Arithmetical Completeness Theorem Solovay's Arithmetical Completeness Theorem affirms that:

Let $A$ be a sentence of modal logic. If every realization $A^\phi$ of $A$ is proved by $PA$, then $GL\vdash A$.

I am troubled by this result. Taking the contrapositive, it affirms that if $GL\not\vdash A$ then there exists some realization $A^\phi$ such that $PA\not\vdash A^\phi$.
Since $GL$ is nice, consistent and decidable, then we can affirm that there are sentences such as $\neg\square\bot$ such that $GL\not\vdash\neg\square\bot$, and thus by Solovay's $PA\not\vdash (\neg\square\bot)^\phi$ for some realization $\phi$. But this is huge, since then the consistency of $GL$ automatically gives us the consistency of $PA$!
A similar result, Gentzen's theorem, also proves the consistency of $PA$, but requires the consistency of Primitive Recursive Arithmetic, which is disputable (I think, I am not really familiarized with Gentzen's result).
I strongly suspect I am assuming here something I should not, but I am not seeing what.
Some possible weak points in my argument:


*

*GL is not as nice as I thought and its consistency can be disputed.

*Solovay's theorem has some obscure clause which I did not take into account, such as supposing the consistency of $PA$.


Any thoughts?
 A: After going through Solovay's proof, I realized that it is indeed the case that the consistency of $PA$ is a hypothesis of the theorem.
Concretely, through the proof we aim to construct a series of Solovay sentences ($S_0,...,S_n$) such that $PA\vdash \wedge_{i:1\le i\le n}[Bew(\neg S_i)\to \neg S_i]\to S_0$ and $PA\vdash S_0\to \neg Bew(A^*)$, where $A$ is a modal sentence which is not a theorem of $GL$ and $*$ a specific realization constructed in the proof.
The remainder of the argument is arguing that while the reflection principles $Bew(\neg S_i)\to \neg S_i$ are not provable, they are certainly true. And therefore it must be the case that $\neg Bew (A^*)$ is true, which implies that there is no proof of $A^*$, if PA is consistent.
To address my other doubt in the question, it is easy to prove that $GL$ is consistent. Simply realize that every theorem in $GL$ evaluates to true if you take $\square$ to be the verum operator that always evaluates to true. Then a modal sentence as $\neg \square\bot$ can never be a theorem of $GL$, and thus $GL$ is consistent.
