Reflection principles and provability algebras in formal arithmetic

L. D. Beklemishev

Trudy Matematicheskogo Instituta imeni V.A. Steklova, Tome 60 (2005) no. 2, pp. 197-268

Résumé

This paper is a study of reflection principles in fragments of formal Peano arithmetic and their applications to the comparison and classification of arithmetical theories.

Bibliographie

[1] W. Ackermann, “Zur Widerspruchsfreiheit der Zahlentheorie”, Math. Ann., 117 (1940), 162–194 | DOI | MR | Zbl

[2] T. Arai, “Epsilon substitution method for theories of jump hierarchies”, Arch. Math. Logic, 41:2 (2002), 123–153 | DOI | MR | Zbl

[3] T. Arai, “Epsilon substitution method for $\operatorname{ID}_1(\Pi_1^0\vee\Sigma_1^0)$”, Ann. Pure Appl. Logic, 121:2–3 (2003), 163–208 | DOI | MR | Zbl

[4] S. N. Artemov, Rasshireniya arifmetiki i modalnye logiki, Diss. ... kand. fiz.-matem. nauk, MIAN, M., 1979

[5] S. N. Artëmov, “Prilozheniya modalnoi logiki v teorii dokazatelstv”, Voprosy kibernetiki: Neklassicheskie logiki i ikh primeneniya, Nauka, M., 1982, 3–20

[6] S. N. Artemov, L. D. Beklemishev, “On propositional quantifiers in provability logic”, Notre Dame J. Formal Logic, 34 (1993), 401–419 | DOI | MR | Zbl

[7] S. N. Artemov, L. D. Beklemishev, “Provability logic”, Handbook of Philosophical Logic, 13, eds. D. Gabbay, F. Guenthner, Kluwer, Dordrecht, 2004, 229–403

[8] J. Avigad, “An ordinal analysis of admissible set theory using recursion on ordinal notations”, J. Math. Logic, 2:1 (2002), 91–112 | DOI | MR | Zbl

[9] J. Avigad, R. Sommer, “A model-theoretic approach to ordinal analysis”, Bull. Symbolic Logic, 3:1 (1997), 17–52 | DOI | MR | Zbl

[10] J. Avigad, R. Sommer, “The model-theoretic ordinal analysis of theories of predicative strength”, J. Symbolic Logic, 64:1 (1999), 327–349 | DOI | MR | Zbl

[11] L. D. Beklemishev, “Ob ogranichennom pravile induktsii i iterirovannykh skhemakh refleksii nad kalmarovskoi elementarnoi arifmetikoi”, Teoreticheskie i prikladnye aspekty matematicheskikh issledovanii, ed. O. B. Lupanov, Izd-vo Mosk. un-ta, M., 1994, 36–39

[12] L. D. Beklemishev, “Iterated local reflection versus iterated consistency”, Ann. Pure Appl. Logic, 75:1–2 (1995), 25–48 | DOI | MR | Zbl

[13] L. D. Beklemishev, “Remarks on Magari algebras of PA and $I\Delta_0+\mathrm{EXP}$”, Lecture Notes in Pure and Appl. Math., 180 (1996), 317–325 | MR | Zbl

[14] L. D. Beklemishev, “Induction rules, reflection principles, and provably recursive functions”, Ann. Pure Appl. Logic, 85:3 (1997), 193–242 | DOI | MR | Zbl

[15] L. D. Beklemishev, “Notes on local reflection principles”, Theoria, 63:3 (1997), 139–146 | MR

[16] L. D. Beklemishev, “Parameter free induction and reflection”, Lecture Notes in Comput. Sci., 1289 (1997), 103–113 | MR | Zbl

[17] L. D. Beklemishev, “A proof-theoretic analysis of collection”, Arch. Math. Logic, 37:5–6 (1998), 275–296 | DOI | MR | Zbl

[18] L. D. Beklemishev, “Parameter free induction and provably total computable functions”, Theoret. Comput. Sci., 224:1–2 (1999), 13–33 | DOI | MR | Zbl

[19] L. D. Beklemishev, “Proof-theoretic analysis by iterated reflection”, Arch. Math. Logic., 42:6 (2003), 515–552 | DOI | MR | Zbl

[20] L. D. Beklemishev, The Worm principle, Logic Group Preprint Ser., 219, University of Utrecht, Utrecht, 2003 ; http://preprints.phil.uu.nl/lgps/ | MR

[21] L. D. Beklemishev, “Provability algebras and proof-theoretic ordinals. I”, Ann. Pure Appl. Logic, 128:1–3 (2004), 103–123 | DOI | MR | Zbl

[22] G. Boolos, “Reflection principles and iterated consistency assertions”, J. Symbolic Logic, 44:1 (1979), 33–35 | DOI | MR | Zbl

[23] G. Boolos, The Unprovability of Consistency: An Essay in Modal Logic, Cambridge Univ. Press, Cambridge, 1979 | MR | Zbl

[24] G. Boolos, “Omega-consistency and the diamond”, Studia Logica, 39:2–3 (1980), 237–243 | DOI | MR | Zbl

[25] G. Boolos, The Logic of Provability, Cambridge Univ. Press, Cambridge, 1993 | MR | Zbl

[26] W. Buchholz, “Explaining Gentzen's consistency proof within infinitary proof theory”, Lecture Notes in Comput. Sci., 1289 (1997), 4–17 | MR | Zbl

[27] W. Buchholz, “Explaining the Gentzen–Takeuti reduction steps: A second-order system”, Arch. Math. Logic., 40:4 (2001), 255–272 | DOI | MR | Zbl

[28] W. Buchholz, S. Wainer, “Provably computable functions and the fast growing hierarchy”, Contemp. Math., 65 (1987), 179–198 | MR | Zbl

[29] N. Katlend, Vychislimost. Vvedenie v teoriyu rekursivnykh funktsii, Mir, M., 1983 | MR

[30] Yu. L. Ershov, Teoriya numeratsii, Nauka, M., 1977 | MR

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

[32] S. Feferman, “Transfinite recursive progressions of axiomatic theories”, J. Symbolic Logic, 27 (1962), 259–316 | DOI | MR

[33] S. Feferman, “Three conceptual problems that bug me”, Lecture text for 7-th Scandinavian Logic Symposium (Uppsala, 1996)

[34] G. Gentzen, “Die Widerspruchsfreiheit der reinen Zahlentheorie”, Math. Ann., 112 (1936), 493–565 | DOI | MR | Zbl

[35] G. Gentzen, “Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie”, Forsch. Logik Grundlegung Exakt. Wiss., 4 (1938), 19–44 | Zbl

[36] K. Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. I”, Monatsh. Math. Phys., 38 (1931), 173–198 | DOI | MR | Zbl

[37] S. S. Goncharov, Schetnye bulevy algebry i razreshimost, Sibirskaya shkola algebry i logiki, Nauchnaya Kniga, Novosibirsk, 1996 | MR

[38] S. V. Goryachev, “Ob interpretiruemosti nekotorykh rasshirenii arifmetiki”, Matem. zametki, 40:5 (1986), 561–571 | MR | Zbl

[39] P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetic, Springer-Verlag, Berlin, 1993 | MR

[40] L. Henkin, J. D. Monk, A. Tarski, Cylindric algebras, Part I, II, Stud. Logic Found. Math., 64, 115, North-Holland, Amsterdam, 1985 | MR | Zbl

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

[42] G. K. Dzhaparidze, Modalno-logicheskie sredstva issledovaniya dokazuemosti, Diss. ... kand. filos. nauk, MGU, M., 1986

[43] G. K. Dzhaparidze, “Polimodalnaya logika dokazuemosti”, Intensionalnye logiki i logicheskaya struktura teorii, Materialy IV Sovetsko-finskogo simpoziuma po logike (Telavi, 1985), eds. V. A. Smirnov i M. N. Bezhanishvili, Metsniereba, Tbilisi, 1988, 16–48 | MR

[44] G. Japaridze, D. de Jongh, “The logic of provability”, Stud. Logic Found. Math., 137 (1998), 475–546 | DOI | MR | Zbl

[45] R. Kaye, J. Paris, C. Dimitracopoulos, “On parameter free induction schemas”, J. Symbolic Logic, 53:4 (1988), 1082–1097 | DOI | MR | Zbl

[46] L. A. S. Kirby, J. B. Paris, “Accessible independence results for Peano arithmetic”, Bull. London Math. Soc., 14:4 (1982), 285–293 | DOI | MR | Zbl

[47] G. Kreisel, “On the interpretation of non-finitist proofs. II: Interpretation of number theory. Applications”, J. Symbolic Logic, 17 (1952), 43–58 | DOI | MR | Zbl

[48] G. Kreisel, “A survey of proof theory”, J. Symbolic Logic, 33 (1968), 321–388 | DOI | MR | Zbl

[49] G. Kreisel, “Wie die Beweistheorie zu ihren Ordinalzahlen kam und kommt”, Jahresber. Deutsch. Math.-Verein., 78:4 (1976/1977), 177–223 | MR

[50] G. Kreisel, A. Lévy, “Reflection principles and their use for establishing the complexity of axiomatic systems”, Z. Math. Logik Grundlagen Math., 14 (1968), 97–142 | DOI | MR | Zbl

[51] D. Leivant, “The optimality of induction as an axiomatization of arithmetic”, J. Symbolic Logic, 48:1 (1983), 182–184 | DOI | MR | Zbl

[52] P. Lindström, “On partially conservative sentences and interpretability”, Proc. Amer. Math. Soc., 91:3 (1984), 436–443 | DOI | MR | Zbl

[53] P. Lindström, “Provability logic – a short introduction”, Theoria, 62:1–2 (1996), 19–61 | MR | Zbl

[54] M. H. Löb, “Solution of a problem of Leon Henkin”, J. Symbolic Logic, 20 (1955), 115–118 | DOI | MR | Zbl

[55] R. Magari, “The diagonalizable algebras”, Boll. Unione Mat. Ital. (4), 12:3 (1975), 117–125 | MR | Zbl

[56] R. Magari, “Representation and duality theory for diagonalizable algebras”, Studia Logica, 34:4 (1975), 305–313 | DOI | MR

[57] G. E. Mints, “Beskvantornye i odnokvantornye sistemy”, Zapiski nauch. semin. LOMI, 20 (1971), 115–133 | MR | Zbl

[58] G. Mints, S. Tupailo, “Epsilon-substitution method for the ramified language and $\Delta_1^1$-comprehension rule”, Synthese Lib., 280 (1999), 107–130 | MR | Zbl

[59] F. Montagna, “On the algebraization of a Feferman's predicate”, Studia Logica, 37:3 (1978), 221–236 | DOI | MR | Zbl

[60] F. Montagna, “On the diagonalizable algebra of Peano arithmetic”, Boll. Unione Mat. Ital. B (5), 16:3 (1979), 795–812 | MR | Zbl

[61] F. Montagna, “The undecidability of the first-order theory of diagonalizable algebras in Peano arithmetic”, Studia Logica, 39:4 (1980), 347–354 | DOI | MR | Zbl

[62] H. Ono, “Reflection principles in fragments of Peano arithmetic”, Z. Math. Logik Grundlagen Math., 33:4 (1987), 317–333 | DOI | MR | Zbl

[63] V. P. Orevkov, “Nizhnie otsenki udlinneniya vyvodov posle ustraneni secheniya”, Zapiski nauch. semin. LOMI, 88 (1979), 137–162 | MR | Zbl

[64] R. Parikh, “Existence and feasibility in arithmetic”, J. Symbolic Logic, 36 (1971), 494–508 | DOI | MR | Zbl

[65] C. Parsons, “On a number-theoretic choice schema and its relation to induction”, Intuitionism and Proof Theory (Buffalo, 1968), eds. A. Kino, J. Myhill, R. E. Vessley, North-Holland, Amsterdam, 1970, 459–473 | MR

[66] C. Parsons, “On $n$-quantifier induction”, J. Symbolic Logic, 37:3 (1972), 466–482 | DOI | MR | Zbl

[67] W. Pohlers, “A short course in ordinal analysis”, Proof Theory. Papers from International Summer School and Conference on Proof Theory (Leeds, 1990), eds. P. Aczel, H. Simmons, S. S. Wainer, Cambridge Univ. Press, Cambridge, 1992, 2–78 | MR | Zbl

[68] W. Pohlers, “Subsystems of set theory and second order number theory”, Handbook of Proof Theory, ed. S. R. Buss, North-Holland, Amsterdam, 1998, 209–335 | MR

[69] M. B. Pour-El, S. Kripke, “Deduction-preserving “recursive isomorphisms” between theories”, Fund. Math., 61 (1967), 141–163 | MR | Zbl

[70] L. J. Pozsgay, “Gödel's second theorem for elementary arithmetic”, Z. Math. Logik Grundlagen Math., 14 (1968), 67–80 | DOI | MR | Zbl

[71] M. O. Rabin, “Non-standard models and independence of the induction axiom”, Essays on the Foundations of Mathematics, Dedicated to A. Fraenkel on his 70th anniversary, Magnes Press, Hebrew Univ., Jerusalem, 1964, 287–299 | MR

[72] M. Rathjen, “Recent advances in ordinal analysis: $\Pi_2^1$-CA and related systems”, Bull. Symbolic Logic, 1:4 (1995), 468–485 | DOI | MR | Zbl

[73] M. Rathjen, “The realm of ordinal analysis”, London Math. Soc. Lecture Note Ser., 258 (1999), 219–279 | MR | Zbl

[74] H. E. Rose, Subrecursion: Functions and Hierarchies, Clarendon Press, New York, 1984 | MR | Zbl

[75] J. B. Rosser, “Extensions of some theorems of Gödel and Church”, J. Symbolic Logic, 1 (1936), 87–91 | DOI | Zbl

[76] J. B. Rosser, “Gödel Theorems for non-constructive logics”, J. Symbolic Logic, 2 (1937), 129–137 | DOI | Zbl

[77] U. R. Schmerl, “A fine structure generated by reflection formulas over primitive recursive arithmetic”, Stud. Logic Found. Math., 97 (1979), 335–350 | DOI | MR | Zbl

[78] G. Shvikhtenberg, “Nekotorye prilozheniya ustraneniya secheniya”, Spravochnaya kniga po matematicheskoi logike. Ch. IV. Teoriya dokazatelstv i konstruktivnaya matematika, ed. Dzh. Barvais, Nauka, M., 1983, 54–83

[79] K. Segerberg, An Essay in Classical Modal Logic, vols. 1–3, Filosofiska Föreningen och Filosofiska Institutionen vid Uppsala Universitet, Uppsala, 1971 | MR | Zbl

[80] V. Yu. Shavrukov, “Subalgebras of diagonalizable algebras of theories containing arithmetic”, Dissertationes Math. (Rozprany Mat.), 323 (1993), 1–82 | MR

[81] V. Yu. Shavrukov, “A note on the diagonalizable algebras of PA and ZF”, Ann. Pure Appl. Logic, 61:1–2 (1993), 161–173 | DOI | MR | Zbl

[82] V. Yu. Shavrukov, “Undecidability in diagonalizable algebras”, J. Symbolic Logic, 62:1 (1997), 79–116 | DOI | MR | Zbl

[83] V. Yu. Shavrukov, “Isomorphisms of diagonalizable algebras”, Theoria, 63:3 (1997), 210–221 | MR

[84] K. Smorinskii, “Teoremy o nepolnote”, Spravochnaya kniga po matematicheskoi logike. Ch. IV. Teoriya dokazatelstv i konstruktivnaya matematika, ed. Dzh. Barvais, Nauka, M., 1983, 9–53

[85] C. Smoryński, “$\omega$-consistency and reflection”, Colloque International de Logique (Clermont-Ferrand, 1975), Colloq. Internat. CNRS, 249, CNRS, Paris, 1977, 167–181 | MR | Zbl

[86] C. Smoryński, “The finite inseparability of the first-order theory of diagonalizable algebras”, Studia Logica, 41:4 (1982), 347–349 | DOI | MR | Zbl

[87] C. Smoryński, Self-Reference and Modal Logic, Springer-Verlag, New York, 1985 | MR | Zbl

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

[89] R. Sommer, “Transfinite induction within Peano arithmetic”, Ann. Pure Appl. Logic, 76:3 (1995), 231–289 | DOI | MR | Zbl

[90] R. Statman, “Bounds for proof-search and speed-up in the predicate calculus”, Ann. Math. Logic, 15:3 (1978), 225–287 | DOI | MR | Zbl

[91] S. Tupailo, “Epsilon substitution method for $\Delta_1^1$-CR: A constructive termination proof”, Log. J. IGPL, 11:3 (2003), 367–377 | DOI | MR | Zbl

[92] A. M. Turing, “Systems of logic based on ordinals”, Proc. London Math. Soc. (2), 45 (1939), 161–228 | DOI | Zbl

[93] A. Visser, “An overview of interpretability logic”, Advances in Modal Logic, vol. 1 (Berlin, 1996), CSLI Lecture Notes., 87, eds. M. Kracht et al., CSLI Publications, Stanford, 1998, 307–359 | MR | Zbl

[94] A. Wilkie, J. Paris, “On the scheme of induction for bounded arithmetic formulas”, Ann. Pure Appl. Logic, 35:3 (1987), 261–302 | DOI | MR | Zbl

[95] D. Zambella, “Shavrukov's theorem on the subalgebras of diagonalizable algebras for theories containing $\mathrm I\Delta_0+\exp$”, Notre Dame J. Formal Logic, 35:1 (1994), 147–157 | DOI | MR | Zbl