zbMATH — the first resource for mathematics

Predicativity through transfinite reflection. (English) Zbl 1402.03086
Reflection for a theory \(T\) and a class \(\Gamma\) of formulas states that all \(T\)-provable formulas from \(\Gamma\) are true. Note that the consistency of \(T\) arises as the special case \(\Gamma=\{0=1\}\). A classical result of G. Kreisel and A. Levy [Z. Math. Logik Grundlagen Math. 14, 97–142 (1968; Zbl 0167.01302)] (refined by D. Leivant [J. Symb. Log. 48, 182–184 (1983; Zbl 0515.03018)]) shows that (uniform) reflection for all first-order formulas over primitive recursive arithmetic is equivalent to induction for these formulas. This yields an alternative axiomatization of Peano arithmetic. The paper under review proves an analogue result for a stronger theory of second-order arithmetic: arithmetical transfinite recursion (\(\operatorname{ATR_0}\)) is equivalent both to consistency and to \(\Pi^1_2\)-reflection for a suitable notion of proof, which involves the \(\omega\)-rule and access to an oracle \(X\subseteq\mathbb N\), as well as axioms from a base theory \(T\) in the language of second-order arithmetic. One writes \([\lambda|X]^\Lambda_T\varphi\) to express that \(\varphi\) is provable with \(\lambda\in\Lambda\) nested \(\omega\)-rules, where \(\Lambda\) is some well-order.
It is an important achievement of the paper that it introduces the provability predicate \([\lambda|X]^\Lambda_T\). The latter is shown to be \(\Sigma^1_1\)-complete (if the existential witness may be used as an oracle) and sound for \(\omega\)-models of \(T\) that contain the set \(X\). The question of completeness with respect to satisfaction in all \(\omega\)-models is not considered. Also, the paper does not investigate the connection with \(\omega\)-model reflection, which is known to be equivalent to bar induction (due to H. Friedman [in: Proc. int. Congr. Math., Vancouver 1974, Vol. 1, 235–242 (1975; Zbl 0344.02022)] and refined by S. G. Simpson [in: Logic colloquium ’80. Papers intended for the European Summer Meeting of the Association for Symbolic Logic, held in Prague, August 24-30, 1980. Amsterdam-New York-Oxford: North-Holland Publishing. 239–253 (1982; Zbl 0497.03045); Subsystems of second order arithmetic. Berlin: Springer (1999; Zbl 0909.03048)] as well as G. Jäger and T. Strahm [Ann. Pure Appl. Logic 97, No. 1–3, 221–230 (1999; Zbl 0930.03087)]).
To see how reflection for \(\omega\)-proofs with oracle implies arithmetical transfinite recursion, let us write \(\operatorname{TR}^\Lambda(\varphi,Z)\) to express that \(Z\) is the iteration of \(\varphi\) along \(\Lambda\) (i.e. that \(\langle\lambda,x\rangle\in Z\) is equivalent to \(\varphi(x,Z_{<\lambda})\), where \(Z_{<\lambda}=\{\langle\eta,y\rangle\in Z\,|\,\eta<\lambda\}\)). Roughly speaking, the paper shows that \(\operatorname{TR}^\Lambda(\varphi,X)\) is satisfied for the set \[ X=\{\langle\lambda,x\rangle\,|\,[\eta|A]^\Lambda_{\operatorname{ECA_0}}\forall Z(\operatorname{TR}^\Lambda(\varphi,Z)\rightarrow\varphi(\dot x,Z_{<\dot\lambda}))\}, \] where \(\eta\) and \(A\) are determined by the other parameters. Reflection is needed to ensure that \(\langle\lambda,x\rangle\in X\) implies \(\varphi(x,X_{<\lambda})\). For the converse one needs to establish the existence of infinite proofs \([\eta|A]^\Lambda_{\operatorname{ECA_0}}\forall_Z(\operatorname{TR}^\Lambda(\varphi,Z)\rightarrow\varphi(\dot x,Z_{<\dot\lambda}))\). This is done by a beautiful double induction on \(\lambda\) and the buildup of \(\varphi\) (see Lemma 6.3). In order to form the set \(X\) in a sufficiently weak theory we need the provability predicate \([\eta|A]^\Lambda_{\operatorname{ECA_0}}\) to be arithmetical. The authors achieve this in the following way: Consider the characteristic properties of the set \(P=\{\langle\eta,\varphi\rangle\,|\,[\eta|A]^\Lambda_T\varphi\}\) (e.g. closure under the \(\omega\)-rule requires that \(\langle\eta,\varphi(\overline n)\rangle\in P\) for all \(n\in\mathbb N\) implies \(\langle\eta+1,\forall x\,\varphi(x)\rangle\in P\)). Any set \(P\) that satisfies these properties is called an iterated oracle provability class for \(\Lambda\), \(A\) and \(T\) (abbreviated \(\operatorname{IPC}^\Lambda_{T|A}(P)\)). Now one can formally define \[ [\eta|A]^\Lambda_T\varphi\quad:\Leftrightarrow\quad\forall P(\operatorname{IPC}^\Lambda_{T|A}(P)\rightarrow\langle\eta,\varphi\rangle\in P). \] As the authors point out, the consistency statement \(\neg[\eta|A]^\Lambda_T(0=1)\) implies the existence of a set \(P\) with \(\operatorname{IPC}^\Lambda_{T|A}(P)\). Together with uniqueness we see that \([\eta|A]^\Lambda_T\varphi\) becomes equivalent to \(\langle\eta,\varphi\rangle\in P\), which is indeed an arithmetical formula.
The existence of iterated oracle provability classes is a delicate issue: Lemma 4.3 of the paper shows \[ \operatorname{ACA}\equiv_{\Pi^0_1}\operatorname{ACA}{}+{}\forall_{\Lambda,A}(\text{``\(\Lambda\) is a well-order''}\rightarrow\exists P\,\operatorname{IPC}^\Lambda_{\operatorname{ACA}|A}(P)). \] However, this result is not robust with respect to the base theory, since its proof uses Löb’s theorem. Indeed, the reviewer has observed that we do have \[ \operatorname{ATR_0}\equiv\operatorname{ACA_0^+}{}+{}\forall_{\Lambda,A}(\text{``\(\Lambda\) is a well-order''}\rightarrow\exists P\,\operatorname{IPC}^\Lambda_{\operatorname{ACA}|A}(P)). \] The inclusion \(\supseteq\) holds by Lemma 4.5. Let us now establish the other inclusion: In view of Theorem 6.7 it suffices to show that the theory on the right side proves consistency for \(\omega\)-proofs with oracle and base theory \(\operatorname{ACA}\). Lemma 7.10 implies that this consistency statement can be established in \(\operatorname{ATR_0}\). It is not hard to see that the same proof goes through in the theory on the right side, since \(\operatorname{ATR_0}\) is only used in two ways: It guarantees that there are full \(\omega\)-models of \(\operatorname{ACA}\), which is already provable in \(\operatorname{ACA_0^+}\); and it ensures the existence of iterated oracle provability classes. In view of this observation the reviewer thinks that the paper tells us more about the formalization of infinite proofs than about consistency and reflection.

03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
03F35 Second- and higher-order arithmetic and fragments
03F03 Proof theory, general (including proof-theoretic semantics)
Full Text: DOI
[1] Beeson, M. and Ščedrov, A., Church’s thesis, continuity, and set theory, this Journal, vol. 49 (1984), no. 2, pp. 630-643. · Zbl 0599.03060
[2] Beklemishev, L. D., Induction rules, reflection principles, and provably recursive functions. Annals of Pure and Applied Logic, vol. 85 (1997), pp. 193-242. doi:10.1016/S0168-0072(96)00045-0 · Zbl 0882.03055
[3] Beklemishev, L. D., Provability algebras and proof-theoretic ordinals, I. Annals of Pure and Applied Logic, vol. 128 (2004), pp. 103-124. doi:10.1016/j.apal.2003.11.030 · Zbl 1048.03045
[4] Beklemishev, L. D., Veblen hierarchy in the context of provability algebras, Logic, Methodology and Philosophy of Science, Proceedings of the Twelfth International Congress (Hájek, P., Valdés-Villanueva, L., and Westerståhl, D., editors), Kings College Publications, London, 2005, pp. 65-78. · Zbl 1105.03062
[5] Beklemishev, L. D., Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, vol. 60 (2005), pp. 197-268. doi:10.1070/RM2005v060n02ABEH000823 · Zbl 1097.03054
[6] Beklemishev, L. D., The Worm principle, Logic Colloquium2002 (Chatzidakis, Z., Koepke, P., and Pohlers, W., editors), Lecture Notes in Logic 27, ASL Publications, 2006, pp. 75-95. · Zbl 1108.03055
[7] Beklemishev, L. D., On the reduction property for GLP-algebras. Doklady: Mathematics, vol. 472 (2017), no. 4. · Zbl 1379.03020
[8] 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. doi:10.1007/s11225-013-9490-7 · Zbl 1322.03042
[9] Beklemishev, L. D. and Onoprienko, A. A., On some slowly terminating term rewriting systems. Sbornik: Mathematics, vol. 206 (2015), no. 9, pp. 1173-1190. doi:10.1070/SM2015v206n09ABEH004493 · Zbl 1334.68110
[10] Boolos, G. S., The Logic of Provability, (1993), Cambridge University Press: Cambridge University Press, Cambridge · Zbl 0891.03004
[11] Cordón-Franco, A., Fernández-Margarit, A., and Lara-Martín, F. F., Fragments of Arithmetic and true sentences. Mathematical Logic Quarterly, vol. 51 (2005), pp. 313-328. doi:10.1002/malq.200410034 · Zbl 1067.03064
[12] Feferman, S., Systems of predicative analysis, this Journal, vol. 29 (1964), pp. 1-30. · Zbl 0134.01101
[13] Feferman, S., Systems of predicative analysis II, this JOURNAL, vol. 33 (1968), pp. 193-220. · Zbl 0162.02201
[14] Fernández-Duque, D., The polytopologies of transfinite provability logic. Archive for Mathematical Logic, vol. 53 (2014), no. 3-4, pp. 385-431. doi:10.1007/s00153-014-0371-1 · Zbl 1352.03071
[15] Fernández-Duque, D. and Joosten, J. J., Models of transfinite provability logics, this Journal, vol. 78 (2013), no. 2, pp. 543-561. · Zbl 1275.03158
[16] Fernández-Duque, D. and Joosten, J. J., The omega-rule interpretation of transfinite provability logic, (2013), arXiv, vol. 1205.2036 [math.LO].
[17] Fernández-Duque, D. and Joosten, J. J., Well-orders in the transfinite Japaridze algebra. Logic Journal of the Interest Group in Pure and Applied Logic, vol. 22 (2014), no. 6, pp. 933-963. · Zbl 1405.03095
[18] Hájek, P. and Pudlák, P., Metamathematics of First Order Arithmetic, Springer-Verlag, Berlin, Heidelberg, New York, 1993. · Zbl 0781.03047
[19] Hirst, J. L., A survey of the reverse mathematics of ordinal arithmetic, Reverse mMathematics 2001, Lecture Notes in Logic, vol. 21, Peters, A. K., Natick, MA, 2005, pp. 222-234. · Zbl 1088.03047
[20] Ignatiev, K. N., On strong provability predicates and the associated modal logics, this Journal, vol. 58 (1993), pp. 249-290. · Zbl 0795.03082
[21] 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, pp. 16-48, In Russian.
[22] Joosten, J. J., .\({\rm{\Pi }}_1^0\)-ordinal analysis beyond first-order arithmetic. Mathematical Communications, vol. 18 (2013), pp. 109-121. · Zbl 1298.03111
[23] 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. doi:10.1002/malq.19680140702 · Zbl 0167.01302
[24] Leivant, D., The optimality of induction as an axiomatization of arithmetic, this Journal, vol. 48 (1983), pp. 182-184. · Zbl 0515.03018
[25] Schmerl, U. R., A fine structure generated by reflection formulas over primitive recursive arithmetic, Logic Colloquium ’78 (Mons, 1978) (Boffa, M., Dalen, D., and Mcaloon, K., editors), Studies in Logic and the Foundations of Mathematics, vol. 97, North-Holland, Amsterdam, 1979, pp. 335-350.
[26] Simpson, S. G., Friedman’s research on subsystems of second-order arithmetic, Harvey Friedman’s Research in the Foundations of Mathematics (Harrington, L., Morley, M., Ščedrov, A, and Simpson, S. G., editors), North-Holland, Amsterdam, 1985, pp. 137-159. · Zbl 0588.03001
[27] Simpson, S. G., Subsystems of Second Order Arithmetic, (2009), Cambridge University Press: Cambridge University Press, New York · Zbl 1181.03001
[28] Simpson, S. G. and Smith, R. L., Factorization of polynomials and \({\rm{\Sigma }}_1^0\) induction. Annals of Pure and Applied Logic, vol. 31 (1986), pp. 289-306. doi:10.1016/0168-0072(86)90074-6 · Zbl 0603.03019
[29] Tait, W., Finitism. Journal of Philosophy, vol. 78 (1981), pp. 524-546. doi:10.2307/2026089
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.