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?