Hostname: page-component-586b7cd67f-gb8f7 Total loading time: 0 Render date: 2024-11-24T03:58:25.319Z Has data issue: false hasContentIssue false
  • English
  • Français

MÜNCHHAUSEN PROVABILITY

Part of: Proof theory and constructive mathematics

Published online by Cambridge University Press:  10 June 2021

JOOST J. JOOSTEN
JOOST J. JOOSTEN*
Affiliation:
DEPARTMENT OF PHILOSOPHY UNIVERSITY OF BARCELONABARCELONA, SPAINE-mail:[email protected]:http://www.phil.uu.nl/~jjoosten
Get access Rights & Permissions [Opens in a new window]

Abstract

By Solovay’s celebrated completeness result [31] on formal provability we know that the provability logic ${\textbf {GL}}$ describes exactly all provable structural properties for any sound and strong enough arithmetical theory with a decidable axiomatisation. Japaridze generalised this result in [22] by considering a polymodal version ${\mathsf {GLP}}$ of ${\textbf {GL}}$ with modalities $[n]$ for each natural number n referring to ever increasing notions of provability. Modern treatments of ${\mathsf {GLP}}$ tend to interpret the $[n]$ provability notion as “provable in a base theory T together with all true $\Pi ^0_n$ formulas as oracles.” In this paper we generalise this interpretation into the transfinite. In order to do so, a main difficulty to overcome is to generalise the syntactical characterisations of the oracle formulas of complexity $\Pi ^0_n$ to the hyper-arithmetical hierarchy. The paper exploits the fact that provability is $\Sigma ^0_1$ complete and that similar results hold for stronger provability notions. As such, the oracle sentences to define provability at level $\alpha $ will recursively be taken to be consistency statements at lower levels: provability through provability whence the name of the paper. The paper proves soundness and completeness for the proposed interpretation for a wide class of theories, namely for any theory that can formalise the recursion described above and that has some further very natural properties. Some remarks are provided on how the recursion can be formalised into second order arithmetic and on lowering the proof-theoretical strength of these systems of second order arithmetic.

Keywords

provability logicsordinal analysissecond order arithmetictransfinite polymodal provability

MSC classification

Primary: 03F03: Proof theory, general
Secondary: 03F35: Second- and higher-order arithmetic and fragments 03F45: Provability logics and related algebras (e.g., diagonalizable algebras)
Type
Article
Information
The Journal of Symbolic Logic , Volume 86 , Issue 3 , September 2021 , pp. 1006 - 1034
Check for updates
Copyright
© Association for Symbolic Logic 2021

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Aguilera, J. P. and Fernández-Duque, D., Strong completeness of provability logic for ordinal spaces, this Journal, vol. 82 (2017), no. 2, pp. 608–628.Google Scholar
Bagaria, J., Magidor, M., and Sakai, H., Reflection and indescribability in the constructible universe. Israel Journal of Mathematics, vol. 208 (2015), no. 1, pp. 1–11.CrossRefGoogle Scholar
Beklemishev, L. D., Proof-theoretic analysis by iterated reflection. Archive for Mathematical Logic, vol. 42 (2003), pp. 515–552.CrossRefGoogle Scholar
Beklemishev, L. D., Provability algebras and proof-theoretic ordinals, I. Annals of Pure and Applied Logic, vol. 128 (2004), pp. 103–124.CrossRefGoogle Scholar
Beklemishev, L. D., Reflection principles and provability algebras in formal arithmetic. Uspekhi Matematicheskikh Nauk, vol. 60 (2005), no. 2, pp. 3–78 (in Russian). English translation in: Russian Mathematical Surveys , vol. 60 (2005), no. 2, pp. 197–268.Google Scholar
Beklemishev, L. D., Veblen hierarchy in the context of provability algebras, Proceedings of the Twelfth International Congress of Logic, Methodology and Philosophy of Science (Hájek, P., Valdés-Villanueva, L., and Westerståhl, D., editors), Kings College Publications, London, 2005, pp. 65–78.Google Scholar
Beklemishev, L. D., Fernández-Duque, D., and Joosten, J.J., On provability logics with linearly ordered modalities. Studia Logica, vol. 102 (2014), pp. 541–566.CrossRefGoogle Scholar
Beklemishev, L. D. and Gabelaia, D., Topological completeness of the provability logic $\mathsf{GLP}$ . Annals of Pure and Applied Logic, vol. 164 (2013), no. 12, pp. 1201–1223.CrossRefGoogle Scholar
Beklemishev, L. D. and Pakhomov, F. N., Reflection algebras and conservation results for theories of iterated truth, preprint, 2019, arXiv:1908.10302.Google Scholar
Cordón Franco, A., Fernández-Duque, D., Joosten, J.J., and Lara Martín, F., Predicativity through transfinite reflection, this Journal, vol. 82 (2017), no. 3, pp. 787–808.Google Scholar
Fernández-Duque, D., The polytopologies of transfinite provability logic. Archive for Mathematical Logic, vol. 53 (2014), no. 3–4, pp. 385–431.CrossRefGoogle Scholar
Fernández-Duque, D., Impredicative consistency and reflection, preprint, 2017, arXiv:1509.04547.Google Scholar
Fernández-Duque, D., Worms and spiders: Reflection calculi and ordinal notation systems. Journal of Applied Logics—IfCoLoG Journal of Logics and Their Applications, vol. 4 (2017), no. 10, pp. 3277–3356.Google Scholar
Fernández-Duque, D. and Hermo Reyes, D., A self-contained provability calculus for, Proceedings of the 26th International Workshop on Logic, Language, Information, and Computation, Wollic 2019, (Iemhoff, R., Moortgat, M., and de Queiroz, R. J. G. B., editors), Lecture Notes in Computer Science, vol. 11541, Springer, Berlin, 2019, pp. 195–207.Google Scholar
Fernández-Duque, D. and Joosten, J.J., Kripke models of transfinite provability logic, Advances in Modal Logic (Bolander, T., Braüner, T., Ghilardi, S., and Moss, L., editors), vol. 9, College Publications, London, 2012, pp. 185–199.Google Scholar
Fernández-Duque, D. and Joosten, J.J., Models of transfinite provability logics, this Journal, vol. 78 (2013), no. 2, pp. 543–561.Google Scholar
Fernández-Duque, D. and Joosten, J.J., Well-orders in the transfinite Japaridze algebra. Logic Journal of the IGPL, vol. 22 (2014), no. 6, pp. 933–963.CrossRefGoogle Scholar
Fernández-Duque, D. and Joosten, J.J., The omega-rule interpretation of transfinite provability logic. Annals of Pure and Applied Logic, vol. 169 (2018), no. 4, pp. 333–371.CrossRefGoogle Scholar
Hájek, P. and Pudlák, P., Metamathematics of First Order Arithmetic, Springer, Berlin, 1993.CrossRefGoogle Scholar
Icard, T.F. III, A topological study of the closed fragment of $\mathsf{GLP}$ . Journal of Logic and Computation, vol. 21 (2011), pp. 683–696.CrossRefGoogle Scholar
Ignatiev, K.N., On strong provability predicates and the associated modal logics, this Journal, vol. 58 (1993), pp. 249–290.Google Scholar
Japaridze, G., The polymodal provability logic, Intensional Logics and Logical Structure of Theories: Material from the Fourth Soviet-Finnish Symposium on Logic, Metsniereba, Telaviv, 1988 (in Russian).Google Scholar
Joosten, J. J., ${\varPi}_1^0$ -ordinal analysis beyond first-order arithmetic. Mathematical Communications, vol. 18 (2013), pp. 109–121.Google Scholar
Joosten, J. J., Turing jumps through provability, Evolving Computability—11th Conference on Computability in Europe, CiE 2015, (Beckmann, A., Mitrana, V., and Soskova, M. I., editors), Lecture Notes in Computer Science, vol. 9136, Springer, New York, 2015, pp. 216–225.Google Scholar
Joosten, J. J., Turing–Taylor expansions of arithmetic theories. Studia Logica, vol. 104 (2016), pp. 1225–1243.CrossRefGoogle Scholar
Joosten, J. J., Transfinite Turing jumps through provability, preprint, 2021, arXiv (soon).Google Scholar
Kreisel, G. and Lévy, A., Reflection principles and their use for establishing the complexity of axiomatic systems. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 14 (1968), pp. 97–142.CrossRefGoogle Scholar
Schmerl, U. R., A fine structure generated by reflection formulas over primitive recursive arithmetic, Logic Colloquium '78 (Mons, 1978), Studies in Logic and the Foundations of Mathematics, vol. 97, North-Holland, Amsterdam, 1979, pp. 335–350.Google Scholar
Shapirovsky, I., PSPACE-decidability of Japaridze's polymodal logic, Advances in Modal Logic (Areces, C. and Goldblatt, R., editors), vol. 8, College Publications, London, 2008, pp. 289–304.Google Scholar
Simpson, S.G., Subsystems of Second Order Arithmetic, Cambridge University Press, New York, 2009.CrossRefGoogle Scholar
Solovay, R.M., Provability interpretations of modal logic. Israel Journal of Mathematics, vol. 28 (1976), pp. 33–71.Google Scholar
Visser, A., Faith & falsity: A study of faithful interpretations and false ${\varSigma}_1^0$ -sentences. Annals of Pure and Applied Logic, vol. 131 (2005), no. 1–3, pp. 103–131.CrossRefGoogle Scholar