The Logic of Correct Models
Fedor Pakhomov
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
- Juan P. Aguilera and Fedor Pakhomov,The Logic of Correct Models.,arXiv preprints,2402.15382, 20 pages, 2024.
- 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.
- G.K. Japaridze,The modal logical means of investigation of provability. Thesis in Philosophy,Moscow (in Russian), 1986.
- Robert M. Solovay,Provability interpretations of modal logic.,Israel Journal of Mathematics,25 (1976): 287-304.