×

Reflection algebras and conservation results for theories of iterated truth. (English) Zbl 07501986

Summary: We consider extensions of the language of Peano arithmetic by transfinitely iterated truth definitions satisfying uniform Tarskian biconditionals. Without further axioms, such theories are known to be conservative extensions of the original system of arithmetic. Much stronger systems, however, are obtained by adding either induction axioms or reflection axioms on top of them. Theories of this kind can interpret some well-known predicatively reducible fragments of second-order arithmetic such as iterated arithmetical comprehension.
We obtain sharp results on the proof-theoretic strength of these systems using methods of provability logic. Reflection principles naturally define unary operators acting on the semilattice of axiomatizable extensions of our basic theory of iterated truth. The substructure generated by the top element of this algebra provides a canonical ordinal notation system for the class of theories under investigation.
Using these notations we obtain conservativity relationships for iterated reflection principles of different logical complexity levels corresponding to the levels of the hyperarithmetical hierarchy, i.e., the analogs of Schmerl’s formulas. These relationships, in turn, provide proof-theoretic analysis of our systems and of some related predicatively reducible theories. In particular, we uniformly calculate the ordinals characterizing the standard measures of their proof-theoretic strength, such as provable well-orderings, classes of provably recursive functions, and \(\Pi_1^0\)-ordinals.

MSC:

03F15 Recursive ordinals and ordinal notations
03F30 First-order arithmetic and fragments
03F35 Second- and higher-order arithmetic and fragments
03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Beklemishev, L.; Fernández-Duque, D.; Joosten, J., On provability logics with linearly ordered modalities, Stud. Log., 102, 3, 541-566 (2014), Preprint · Zbl 1322.03042
[2] Beklemishev, L. D., Proof-theoretic analysis by iterated reflection, Arch. Math. Log., 42, 515-552 (2003) · Zbl 1026.03041
[3] Beklemishev, L. D., Provability algebras and proof-theoretic ordinals, I, Ann. Pure Appl. Log., 128, 103-123 (2004) · Zbl 1048.03045
[4] Beklemishev, L. D., Reflection principles and provability algebras in formal arithmetic, Usp. Mat. Nauk. Usp. Mat. Nauk, Russ. Math. Surv., 60, 2, 197-268 (2005), In Russian. English translation in: · Zbl 1097.03054
[5] Beklemishev, L. D., Veblen hierarchy in the context of provability algebras, (Hájek, P.; Valdés-Villanueva, L.; Westerståhl, D., Logic, Methodology and Philosophy of Science. Logic, Methodology and Philosophy of Science, Proceedings of the Twelfth International Congress (June 2005), Kings College Publications: Kings College Publications London). (Logic Group Preprint Series, vol. 232 (June 2004), Utrecht University), 65-78, Preprint: · Zbl 1105.03062
[6] Beklemishev, L. D., Calibrating provability logic: from modal logic to reflection calculus, (Bolander, T.; Braüner, T.; Ghilardi, S.; Moss, L., Advances in Modal Logic, vol. 9 (2012), College Publications: College Publications London), 89-94 · Zbl 1331.03040
[7] Beklemishev, L. D., Positive provability logic for uniform reflection principles, Ann. Pure Appl. Log., 165, 1, 82-105 (2014) · Zbl 1322.03041
[8] Beklemishev, L. D., A note on strictly positive logics and word rewriting systems, (Odintsov, Sergei, Larisa Maximova on Implication, Interpolation, and Definability, vol. 15 (2018), Springer: Springer Berlin, Heidelberg), 61-70 · Zbl 1429.03077
[9] Beklemishev, L. D., Reflection calculus and conservativity spectra, Russ. Math. Surv.. Russ. Math. Surv., Usp. Mat. Nauk, 73:4, 442, 3-52 (2018), Russian original: · Zbl 1522.03326
[10] Boolos, G., The Logic of Provability (1993), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0891.03004
[11] Chagrov, A.; Zakharyaschev, M., Modal Logic (1997), Clarendon Press: Clarendon Press Oxford · Zbl 0871.03007
[12] Cieśliński, C., The Epistemic Lightness of Truth: Deflationism and its Logic (2017), Cambridge University Press
[13] Dashkov, E. V., On the positive fragment of the polymodal provability logic GLP, Math. Notes, 91, 3, 318-333 (2012) · Zbl 1315.03113
[14] Enayat, Ali; Pakhomov, Fedor, Truth, disjunction, and induction, Arch. Math. Log., 58, 5, 753-766 (Aug 2019) · Zbl 1477.03250
[15] Feferman, S., Arithmetization of metamathematics in a general setting, Fundam. Math., 49, 35-92 (1960) · Zbl 0095.24301
[16] Feferman, S., Systems of predicative analysis, J. Symb. Log., 29, 1-30 (1964) · Zbl 0134.01101
[17] Feferman, S., Reflecting on incompleteness, J. Symb. Log., 56, 1, 1-49 (1991) · Zbl 0746.03046
[18] Feferman, S.; Strahm, T., The unfolding of non-finitist arithmetic, Ann. Pure Appl. Log., 104, 1, 75-96 (2000) · Zbl 0959.03048
[19] Fernández-Duque, D.; Joosten, J. J., Kripke models of transfinite provability logic, Advances in Modal Logic, vol. 9, 185-199 (2012), College Publications · Zbl 1301.03063
[20] Fernández-Duque, D.; Joosten, J. J., Models of transfinite provability logic, J. Symb. Log., 78, 2, 543-561 (2013) · Zbl 1275.03158
[21] Fernández-Duque, D.; Joosten, J. J., The omega-rule interpretation of transfinite provability logic, Ann. Pure Appl. Log., 169, 4, 333-371 (2018) · Zbl 1429.03211
[22] Fernández-Duque, David; Joosten, Joost J., Well-orders in the transfinite Japaridze algebra, Log. J. IGPL, 22, 6, 933-963 (2014) · Zbl 1405.03095
[23] Flumini, D.; Sato, K., From hierarchies to well-foundedness, Arch. Math. Log., 53, 7, 855-863 (2014) · Zbl 1338.03011
[24] Hájek, P.; Pudlák, P., Metamathematics of First Order Arithmetic (1993), Springer-Verlag: Springer-Verlag Berlin, Heidelberg, New York · Zbl 0781.03047
[25] Halbach, V., Axiomatic theories of truth (2014), Cambridge University Press · Zbl 1223.03001
[26] Hermo Reyes, E.; Joosten, J. J., The logic of Turing progressions (2017) · Zbl 1452.03132
[27] Ignjatovic, A. D., Fragments of first and Second Order Arithmetic and Length of Proof (1990), University of California: University of California Berkeley, PhD thesis
[28] Joosten, J. J., Turing-Taylor expansions of arithmetical theories, Stud. Log., 104, 1225-1243 (2015) · Zbl 1417.03297
[29] Joosten, J. J., Turing jumps through provability, (Beckmann, Arnold; Mitrana, Victor; Ivanova Soskova, Mariya, Evolving Computability - 11th Conference on Computability in Europe, CiE 2015, Bucharest, Romania, June 29-July 3, 2015. Proceedings. Evolving Computability - 11th Conference on Computability in Europe, CiE 2015, Bucharest, Romania, June 29-July 3, 2015. Proceedings, Lecture Notes in Computer Science, vol. 9136 (2015), Springer), 216-225 · Zbl 1461.03056
[30] Kikot, S.; Kurucz, A.; Tanaka, Y.; Wolter, F.; Zakharyaschev, M., Kripke completeness of strictly positive modal logics over meet-semilattices with operators (2017)
[31] Kotlarski, H., Bounded induction and satisfaction classes, Z. Math. Log., 32, 531-544 (1986) · Zbl 0622.03025
[32] Kotlarski, H.; Ratajczyk, Z., Inductive full satisfaction classes, Ann. Pure Appl. Log., 47, 3, 199-223 (1990) · Zbl 0708.03014
[33] Kreisel, G.; Lévy, A., Reflection principles and their use for establishing the complexity of axiomatic systems, Z. Math. Log. Grundl. Math., 14, 97-142 (1968) · Zbl 0167.01302
[34] Leigh, G., Reflecting on truth, IfCoLog J. Log. Appl., 3, 4, 557-594 (2016)
[35] Leivant, D., The optimality of induction as an axiomatization of arithmetic, J. Symb. Log., 48, 182-184 (1983) · Zbl 0515.03018
[36] Łełyk, Mateusz, Axiomatic theories of truth, bounded induction and reflection principles (2017), University of Warsaw, PhD thesis · Zbl 1421.03028
[37] Łełyk, Mateusz, Model theory and proof theory of the global reflection principle (2021), Technical report · Zbl 1473.03047
[38] Pakhomov, Fedor; Walsh, James, Reflection ranks and ordinal analysis (2018), arXiv preprint · Zbl 1511.03018
[39] Pakhomov, Fedor; Walsh, James, Reducing ω-model reflection to iterated syntactic reflection (2021), arXiv preprint · Zbl 1511.03018
[40] Pohlers, W., Proof Theory. An Introduction, Lecture Notes in Mathematics, vol. 1407 (1989), Springer-Verlag: Springer-Verlag Berlin · Zbl 0695.03024
[41] Pudlák, P., Cuts, consistency statements and interpretations, J. Symb. Log., 50, 423-441 (1985) · Zbl 0569.03024
[42] Rose, H. E., Subrecursion: Functions and Hierarchies (1984), Clarendon Press: Clarendon Press Oxford · Zbl 0539.03018
[43] Schmerl, U. R., A fine structure generated by reflection formulas over Primitive Recursive Arithmetic, (Boffa, M.; van Dalen, D.; McAloon, K., Logic Colloquium’78 (1979), North Holland: North Holland Amsterdam), 335-350 · Zbl 0429.03039
[44] Schmerl, U. R., A proof-theoretical fine structure in systems of ramified analysis, Arch. Math. Log., 22, 167-186 (1982) · Zbl 0506.03016
[45] Schütte, K., Proof Theory (1977), Springer-Verlag: Springer-Verlag Berlin, Heidelberg, New York · Zbl 0367.02012
[46] Smoryński, C., Self-Reference and Modal Logic (1985), Springer-Verlag: Springer-Verlag Berlin · Zbl 0596.03001
[47] Takeuti, G., Proof Theory (2013), Dover Publications
[48] Visser, A., Semantics and the liar paradox, (Handbook of philosophical logic (1989), Springer), 617-706 · Zbl 0875.03030
[49] Weaver, N., Predicativity beyond \(\operatorname{\Gamma}_0 (2007)\), Technical report
[50] Yablo, S., Truth and reflection, J. Philos. Log., 14, 3, 297-349 (1985) · Zbl 0588.03002
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.