On provability logics of Niebergall arithmetic

L. V. Dvorkin

Izvestiya. Mathematics , Tome 88 (2024) no. 3, pp. 468-505.

Résumé

K. G. Niebergall suggested a simple example of a non-gödelean arithmetical theory $\mathrm{NA}$, in which a natural formalization of its consistency is derivable. In the present paper we consider the provability logic of $\mathrm{NA}$ with respect to Peano arithmetic. We describe the class of its finite Kripke frames and establish the corresponding completeness theorem. For a conservative extension of this logic in the language with an additional propositional constant, we obtain a finite axiomatization. We also consider the truth provability logic of $\mathrm{NA}$ and the provability logic of $\mathrm{NA}$ with respect to $\mathrm{NA}$ itself. We describe the classes of Kripke models with respect to which these logics are complete. We establish $\mathrm{PSpace}$-completeness of the derivability problem in these logics and describe their variable free fragments. We also prove that the provability logic of $\mathrm{NA}$ with respect to Peano arithmetic does not have the Craig interpolation property.

Détail

Keywords: the logic of provability, Kripke semantics.

Bibliographie

[1] K.-G. Niebergall, “ ‘Natural’ representations and extensions of Gödel's second theorem”, Logic colloquium '01, Lect. Notes Log., 20, Assoc. Symbol. Logic, Urbana, IL, 2005, 350–368 | MR | Zbl

[2] S. Feferman, “Arithmetization of metamathematics in a general setting”, Fund. Math., 49 (1960), 35–92 | DOI | MR | Zbl

[3] G. Kreisel, “A survey of proof theory”, J. Symb. Log., 33:3 (1968), 321–388 | DOI | MR | Zbl

[4] D. E. Willard, “Self-verifying axiom systems, the incompleteness theorem and related reflection principles”, J. Symb. Log., 66:2 (2001), 536–596 | DOI | MR | Zbl

[5] F. Pakhomov, A weak set theory that proves its own consistency, 2019, arXiv: 1907.00877

[6] S. N. Artemov and L. D. Beklemishev, “Provability logic”, Handb. Philos. Log., 13, 2nd ed., Kluwer, Dordrecht, 2005, 189–360 | DOI

[7] C. Smoryński, Self-reference and modal logic, Universitext, Springer-Verlag, New York, 1985 | DOI | MR | Zbl

[8] G. Boolos, The logic of provability, Cambridge Univ. Press, Cambridge, 1993 | DOI | MR | Zbl

[9] R. M. Solovay, “Provability interpretations of modal logic”, Israel J. Math., 25:3-4 (1976), 287–304 | DOI | MR | Zbl

[10] A. Visser, “Peano's smart children: a provability logical study of systems with built-in consistency”, Notre Dame J. Form. Log., 30:2 (1989), 161–196 | DOI | MR | Zbl

[11] V. Yu. Shavrukov, “On Rosser's provability predicate”, Z. Math. Logik Grundlag. Math., 37:19-22 (1991), 317–330 | DOI | MR | Zbl

[12] V. Yu. Shavrukov, “A smart child of Peano's”, Notre Dame J. Form. Log., 35:2 (1994), 161–185 ; Preprint ML-92-10, ILLC Prepublication Series, Univ. Amsterdam, 1991 https://eprints.illc.uva.nl/id/eprint/1324/1/ML-1992-10.text.pdf | DOI | MR | Zbl

[13] L. D. Beklemishev, “Reflection principles and provability algebras in formal arithmetic”, Russian Math. Surveys, 60:2 (2005), 197–268 | DOI

[14] K. N. Ignatiev, “On strong provability predicates and the associated modal logics”, J. Symb. Log., 58:1 (1993), 249–290 | DOI | MR | Zbl

[15] G. K. Japaridze, Modal logic tools of investigation of provability, Candidate (PhD) dissertation, Moscow State Univ., Moscow, 1986 (Russian)

[16] G. K. Japaridze [G. K. Dzhaparidze], “Polymodal provability logic”, Intensional logics and the logical structure of theories (Telavi 1985), Metsniereba, Tbilisi, 1988, 16–48 (Russian) | MR | Zbl

[17] A. Chagrov and M. Zakharyaschev, Modal logic, Oxford Logic Guides, 35, The Clarendon Press, Oxford Univ. Press, New York, 1997 | MR | Zbl

[18] L. D. Beklemishev, “Kripke semantics for provability logic GLP”, Ann. Pure Appl. Logic, 161:6 (2010), 756–774 | DOI | MR | Zbl

[19] I. Shapirovsky, “PSPACE-decidability of Japaridze's polymodal logic”, Advances in modal logic, v. 7, College Publications, London, 2008, 289–304 | MR | Zbl