Authors: Juan Aguilera and Fedor Pakhomov

In his well-known paper [4] Robert Solovay proved that the provability logic of \(\mathsf{PA}\) is the Gödel-Löb logic \(\mathsf{GL}\). Also in the same paper Solovay considered some set-theoretic interpretations of provability logic which lead to stronger provability logics.

Latter Japaridze [3] proved arithmetical completeness theorem for the polymodal provability logic \(\mathsf{GLP}\), where for a modernized version [2] of his result \([n]\phi\) is interpreted as “the sentence \(\phi\) is provable in \(\mathsf{PA}\) extended by all true \(\Pi_n\)-sentences.”

In our work [1] we investigated the set theoretic interpretation of \([n]\), where \([n]\phi\) mean “the sentence \(\phi\) is true in all \(\Sigma_{n+1}\)-correct transitive sets.” Assuming Gödel’s axiom \(V = L\) we prove that the set of polymodal formulas valid under this interpretation is precisely the set of theorems of the logic \(\mathsf{GLP}.3\). Here \(\mathsf{GLP}.3\) is the extension of \(\mathsf{GLP}\) by the axioms of linearity for all \([n]\). We also show that this result is not provable in \(\mathsf{ZFS}\), so the hypothesis \(V = L\) cannot be removed.

As part of the proof, we derive the following purely modal-logical results which are of independent interest: the logic \(\mathsf{GLP}.3\) coincides with the logic of closed substitutions of \(\mathsf{GLP}\), and is the maximal normal extension of \(\mathsf{GLP}\) that doesn’t prove \([n]\bot\), for any \(n\).

Bibliography

1. Juan P. Aguilera and Fedor Pakhomov,The Logic of Correct Models.,arXiv preprints,2402.15382, 20 pages, 2024.
2. L.D. Beklemishev,A simplified proof of arithmetical completeness theorem for provability logic GLP.,Proceedings of the Steklov Institute of Mathematics,274 (2011): 25-33.
3. G.K. Japaridze,The modal logical means of investigation of provability. Thesis in Philosophy,Moscow (in Russian), 1986.
4. Robert M. Solovay,Provability interpretations of modal logic.,Israel Journal of Mathematics,25 (1976): 287-304.