Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Iterated Inductive Definitions Revisited

  • Chapter
  • First Online:
Feferman on Foundations

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 13))

Abstract

In this paper we revisit our contribution to Lecture Note 897 and present a computation of the prooftheoretic ordinals of formal theories for iterated inductive definitions together with a characterization of their provably recursive functions. The techniques used here differ essentially from the original ones. Sections 1–5 contain a general survey of the connections between recursion theoretic and proof theoretic ordinals and roughly recap some basic facts on iterated inductive definitions. Beginning with Sect. 6 the paper becomes more technical. After introducing the semi–formal system for iterated inductive definition and the necessary ordinals we compute the ordinal spectrum of the formal theory for iterated inductive definitions and characterize their provably total functions in terms of a subrecursive hierarchy. The last section briefly discusses the foundational aspects of the paper.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    A problem that was and apparently still is in the focus of interest. Cf. e.g. [1, 6, 14].

  2. 2.

    This technique has been introduced by Wilfried Buchholz in [8] .

  3. 3.

    Cf. [25] Exercise 1.6. and Chap. 8.

  4. 4.

    For more details cf. [31] .

  5. 5.

    For a proof cf. e.g. [31] Theorem 3.5 or [35] Theorem 5.4.9 which treats the case \({\mathfrak {M}}={\mathbb N}\).

  6. 6.

    Proofs can be found in [2, 35] , Sect. 6.6 and [31] Sect. 5.2.

  7. 7.

    The axiom system for weak second order logic above the axiomatization \({\textsf {PA}}\) for the structure \({\mathbb N}\) of arithmetic, i.e. \({\textsf {PA}}\) plus the full comprehension scheme, is also known as classical analysis.

  8. 8.

    Cf. [25] Chap. 9.

  9. 9.

    Cf. [24] .

  10. 10.

    Observe that the opposite direction is false in general. It is possible that \(\textsf {T}\vdash F(G)\) for every formula G with a proof depending on G whilst \(\textsf {T}(X)\not \vdash F(X)\) since this would require a uniform proof. An effect which reminds of (and is connected to) the \(\omega \)–defect of the first order language of \(\textsf {T}\). Whilst \(\textsf {T}\vdash F(t)\) for any closed first order term t we cannot get \(\textsf {T}\vdash F(x)\) for a free variable x.

  11. 11.

    Cf. [23].

  12. 12.

    Cf. [25] Corollary 9A.3.

  13. 13.

    In slight abuse of notation we will denote by \({\mathfrak {M}}\) both: the structure and its domain.

  14. 14.

    Due to the fact that we have an elementary pairing in \({\mathfrak {M}}\) we sloppily talk about sets whenever [25] talks about relations.

  15. 15.

    The proof is similar to that of the Boundedness Theorem. Cf. [31] Theorem 5.27. The 2–power is in general unavoidable.

  16. 16.

    Originally–and closer to formal systems–only infinite inferences whose premises could be enumerated primitive recursively were allowed in semi–formal systems. However, for the purpose of ordinal analysis the more liberalized version suffices.

  17. 17.

    The abstractly defined ordinals \(\kappa ^{\mathfrak {M}}_\mu \)—-symbolized by the constants” \(\Omega _\mu \)—are ideal objects as introduced in [38] . Their elimination in course of the ordinal analysis corresponds to Hilbert’s “elimination of ideal objects” as discussed there.

  18. 18.

    The notion \(\xi \le \Omega _{\mu +1}\) is to be read relative to an interpretation of the constants \(\Omega _{\mu +1}\) which is not yet fixed. So the language \({\mathcal{L}_{\mathbf{ID}_{\nu }}^*}\) varies with different interpretations of \(\Omega _{\mu +1}\).

  19. 19.

    Observe that there are two types of ordinals. First ordinals \(\le \nu \) which are represented by the elements in the field of \(\prec _0\) and thus are just numbers, hence “quantifiable”, and secondly the ordinal constants \(\xi \) occurring in the form of \(I_{F_\mu }^{<\xi }\).

  20. 20.

    The proof is similar to that of [35] Lemma 9.5.3.

  21. 21.

    Cf. the discussion in [38] .

  22. 22.

    Already Feferman in [12] Sect. 4.1 conjectured “some collapsing argument my perhaps be possible” in finding the “provably recursive ordinals” of \(\mathbf{ID}_{\nu }\).

  23. 23.

    A technique that goes back to work of many people among them Sol Feferman, Peter Aczel, Jane Bridge (Kister) , Wilfried Buchholz and others.

  24. 24.

    By \(\alpha =_{\textit{NF}}{\alpha }_1+\cdots +{\alpha }_{n}\) we denote the Cantor normal form for \(\alpha \).

  25. 25.

    \(\alpha =_{\textit{NF}}\varphi _{\alpha _1}({\alpha _2})\) means \(\alpha =\varphi _{\alpha _1}({\alpha _2})\) and \(\alpha _i<\alpha \) for \(i=1,2\).

  26. 26.

    To avoid a lengthy passage which is inessential for our result we suppressed to indicate that the less than relation between terms that are not both strongly critical, i.e., at least one of them is different from \(\Omega _\mu \) or \(\Psi _{\Omega _{\mu +1}}^{\alpha }\), can also be obtained primitive recursively, i.e., elementarily in our setting. This has been widely handled in the literature. E.g [39] Sect. 14, [35] Definition 9.6.7.

  27. 27.

    Cf. [24] .

  28. 28.

    “Closure under first order quantification” has to be replaced by “closure under bounded quantification” in \({\varvec{{\Sigma }}^{0}_{1}}\).

  29. 29.

    This is based on an idea due to Jan Carl Stegert in [42].

  30. 30.

    In [38] we call a dominant for \((\forall x)(\exists y)F(x,y,{\mathbf {k}})\) a testfunction since it gives an upper bound for testing instances for y in \((\exists y)F(n,y,{\mathbf {k}})\). More details on testfunctions and their impact on Hilbert’s programme of elimination of ideal elements are discussed in [38] .

  31. 31.

    Cited from [11].

  32. 32.

    This paper is also in another context of seminal importance. It led Wilfried Buchholz to develop his \(\Omega _{\mu }\)–rules also presented in [5] . This is another story which I briefly touched in [29].

  33. 33.

    This approach has the advantage that only the monotonicity of the inductive definition is used. All the results obtained there are (as explicitly stated there) valid for monotone inductive definitions. This is in contrast to the more perspicuous approach in [5] where the positivity of the inductive definition is needed.

  34. 34.

    Cf. [7] .

  35. 35.

    Cf. [40].

  36. 36.

    Cf. [1].

  37. 37.

    Cf. [19].

  38. 38.

    Cf. [18].

  39. 39.

    This is the reason why we required in Note 4.2 to restrict the iterations to ordinals less than the first recursively inaccessible ordinal.

References

  1. Avigad, J., Towsner, H.: Functional interpretation and inductive definitions. J. Symb. Logic 74(4), 1100–1120 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  2. Beckmann, A., Pohlers, W.: Application of cut-free infinitary derivations to generalized recursion theory. Ann. Pure Appl. Logic 94, 1–19 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  3. Blankertz, B., Weiermann, A.: How to characterize provably total functions by the Buchholz operator method. Lecture Notes in Logic, vol. 6. Springer, Heidelberg (1996)

    Google Scholar 

  4. Blankertz, B.: Beweistheoretischen Techniken zur Bestimmung von \(\Pi ^0_2\)–Skolem Funktionen, Dissertation, Westfälische Wilhelms-Universität, Münster (1997)

    Google Scholar 

  5. Buchholz, W., Feferman, S., Pohlers, W., Sieg, W. (eds.): Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-theoretical Studies, Lecture Notes in Mathematics, vol. 897. Springer, Heidelberg (1981)

    Google Scholar 

  6. Buchholz, W.: Another reduction of classical \({I\!D}_\nu \) to constructive \({I\!D}_\nu \). In: Schindler, R. (ed.) Ways of Proof Theory, Ontos Mathematical Logic, vol.  2, Ontos Verlag, Frankfurt, Paris, Lancaster, New Brunswick, pp. 183–197 (2010)

    Google Scholar 

  7. Buchholz, W.: The \({\Omega }_{\mu +1}\)-rule, iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies. In: Buchholz, W. et al. (eds.), Lecture Notes in Mathematics, vol. 897, pp. 188–233. Springer, Heidelberg (1981)

    Google Scholar 

  8. Buchholz, W.: A simplified version of local predicativity. In: Aczel, P. (ed.) Proof Theory, pp. 115–147. Cambridge University Press, Cambridge (1992)

    Google Scholar 

  9. Buchholz, W., Pohlers, W.: Provable well orderings of formal theories for transfinitely iterated inductive definitions. J. Symb. Logic 43, 118–125 (1978)

    Article  MATH  Google Scholar 

  10. Buchholz, W., Cichon, E.A., Weiermann, A.: A uniform approach to fundamental sequences and hierarchies. Math. Logic Quart. 40, 273–286 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  11. Feferman, S., Sieg, W.: Inductive definitions and subsystems of analysis. In: Buchholz, W. et al., (ed.), Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-theoretical Studies, Lecture Notes in Mathematics, vol.  897, pp. 16–77. Springer, Heidelberg (1981)

    Google Scholar 

  12. Feferman, S.: Formal theories for transfinite iteration of generalized inductive definitions and some subsystems of analysis. In: Kino, A. et al., (ed.) Intuitionism and Proof Theory, Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Company, Amsterdam, pp. 303–326 (1970)

    Google Scholar 

  13. Feferman, S.: Preface: how we got from there to here. In: Buchholz W. et al., (eds.) Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-theoretical Studies, Lecture Notes in Mathematics, vol.  897, pp. 1–15. Springer, Heidelberg (1981)

    Google Scholar 

  14. Feferman, S.: The proof theory of classical and constructive inductive definitions. A forty year saga, 1968–2008. In: Schindler, R. (ed.) Ways of Proof Theory, Ontos Mathematical Logic, vol. 2, Ontos Verlag, Frankfurt, Paris, Lancaster, New Brunswick, pp. 79–95 (2010)

    Google Scholar 

  15. Gentzen, G.: Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie. Math. Ann. 119, 140–161 (1943)

    Article  MathSciNet  MATH  Google Scholar 

  16. Hilbert, D., Die Grundlagen der Mathematik. Vortrag gehalten auf Einladung des Mathematischen Seminars im Juli 1927 in Hamburg. In: Hamburger Mathematische Einzelschriften, vol. 5, pp. 1–21. Heft (1928)

    Google Scholar 

  17. Howard, W.A.: A system of abstract constructive ordinals. J. Symb. Logic 37, 355–374 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  18. Jäger, G., Pohlers, W.: Eine beweistheoretische Untersuchung von \(({\Delta }^1_2\) -CA\()+(\)BI\()\) und verwandter Systeme. Bayerische Akademie der Wissenschaften, Sitzungsberichte 1982, pp. 1–28 (1983)

    Google Scholar 

  19. Jäger, G.: Theories for Admissible Sets. A Unifying Approach to Proof Theory, Studies in Proof Theory, Lecture Notes, vol.  2. Bibliopolis, Naples (1986)

    Google Scholar 

  20. Jäger, G., Strahm, T.: Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory. J. Symb. Logic 66(2), 935–958 (2001)

    Google Scholar 

  21. Kreisel, G.: Generalized inductive definitions, Reports of seminars on the foundation of Analysis. (Stanford Report), mimeographed, vol. section III (1963)

    Google Scholar 

  22. Martin-Löf, P.: Hauptsatz for the intuitionistic theory of iterated inductive definitions. In: Fenstad, J.E. (ed.) Proceedings of the 2nd Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics, pp. 179–216, vol.  63. North-Holland Publishing Company, Amsterdam (1971)

    Google Scholar 

  23. Möllerfeld, M.: Systems of inductive definitions, Ph.D. thesis, Münster (2003)

    Google Scholar 

  24. Moschovakis, Y.N.: Axioms for computation theories – first draft. In: Gandy, R.O., Yates, C.M.E. (eds.), Logic colloquium ’69 Studies in Logic and the Foundations of Mathematics, vol. 61, pp. 199–255. North-Holland Publishing Company, Amsterdam (1971)

    Google Scholar 

  25. Moschovakis, Y.N.: Elementary Induction on Abstract Structures, Studies in Logic and the Foundations of Mathematics, vol. 77. North-Holland Publishing Company, Amsterdam (1974)

    Google Scholar 

  26. Pohlers, W., Stegert, J.C.: Provably recursive functions of reflections. In: Berger, U. et al. (eds.), Logic, Construction, Computation, Ontos Mathematical Logic, vol. 3, pp. 381–474. Ontos Verlag, Frankfurt (2012)

    Google Scholar 

  27. Pohlers, W.: An upper bound for the provability of transfinite induction, \(\models \). In: Diller, J., Müller, G.H. (eds.) ISILC Proof Theory Symposium, Lecture Notes in Mathematics, vol. 500, pp. 271–289. Springer, Heidelberg (1975)

    Google Scholar 

  28. Pohlers, W.: Beweistheorie der iterierten induktiven Definitionen. Ludwig Maximilians-Universität, München, München, Habilschrift (1977)

    Google Scholar 

  29. Pohlers, W.: From subsystems of analysis to subsystems of set theory. In: Kahle, R. et al., (eds.), Advances in Proof Theory, Progress in Computer Science and Applied Logic 28, pp. 319–338. Birkhäuser Verlag (2016)

    Google Scholar 

  30. Pohlers, W.: Proof-theoretical analysis of ID\(_{\nu }\) by the method of local predicativity. In: Buchholz, W. et al., (eds.) Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-theoretical Studies, Lecture Notes in Mathematics, vol. 897, pp. 261–357. Springer, Heidelberg (1981)

    Google Scholar 

  31. Pohlers, W.: Semi–formal calculi and their applications. In: Kahle, R., Rathjen, M. (eds.), Gentzen’s Centenary: The Quest for Consistency, pp. 195–232. Springer, Berlin (2015)

    Google Scholar 

  32. Pohlers, W.: Ordinals connected with formal theories for transfinitely iterated inductive definitions. J. Symb. Logic 43, 161–182 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  33. Pohlers, W.: Proof Theory, The First Step into Impredicativity. Universitext, Springer, Berlin (2009)

    Google Scholar 

  34. Pohlers, W.: Hilbert’s programme and ordinal analysis. In  Probst, D., Schuster, P. (eds.), Concepts of Proof in Mathematics, Philosophy and Computer Science, Ontos Mathematical Logic, DeGruyter, pp. 291–322 (2016)

    Google Scholar 

  35. Rathjen, M.: Proof theory of reflection. Ann. Pure Appl. Logic 68, 181–224 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  36. Rathjen, M.: An ordinal analyis of parameter free \({\Pi }_2^1\)-comprehension. Arch. Math. Logic 48(3), 263–362 (2005)

    Google Scholar 

  37. Rathjen, M.: An ordinal analyis of stability. Arch. Math. Logic 48(2), 1–62 (2005)

    Google Scholar 

  38. Schindler, R. (ed.): Ways of Proof Theory, Ontos Mathematical Logic, vol. 2. Ontos Verlag, Frankfurt (2010)

    Google Scholar 

  39. Schütte, K.: Proof theory, Grundlehren der mathematischen Wissenschaften, vol. 225. Springer, Heidelberg (1977)

    Google Scholar 

  40. Sieg, W.: Inductive definitions, constructive ordinals and normal derivations. In: Buchholz, W. et al. (eds.), Iterated inductive Definitions and Subsystems of Analysis: Recent Proof-theoretical Studies, Lecture Notes in Mathematics, vol.  897, pp. 143–187. Springer, Heidelberg (1981)

    Google Scholar 

  41. Spector, C.: Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In: Dekker, J.C.E. (ed.), Recursive Function Theory, Proceedings of Symposia in Pure Mathematics, vol.  5, pp. 1–27. American Mathematical Society, Providence (1962)

    Google Scholar 

  42. Stegert, J.-C.: Ordinal proof theory of Kripke–Platek set theory augmented by strong reflection principles, Ph.D. thesis, Westfälische Wilhelms-Universität, Münster (2011)

    Google Scholar 

  43. Zucker, J.I.: Iterated inductive definitions, trees, and ordinals. In: Troelstra, A.S. (ed.), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344, pp. 392–453, Springer, Heidelberg (1973)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Mathematical Logic and Foundational Research Universität Münster, Einsteinstrasses 62, D-48149, Münster, Germany

    Wolfram Pohlers

Authors
  1. Wolfram Pohlers
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wolfram Pohlers .

Editor information

Editors and Affiliations

  1. Institut für Informatik, Universität Bern, Bern, Switzerland

    Gerhard Jäger

  2. Department of Philosophy, Carnegie Mellon University Dept. Philosophy, Pittsburgh, Pennsylvania, USA

    Wilfried Sieg

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Pohlers, W. (2017). Iterated Inductive Definitions Revisited. In: Jäger, G., Sieg, W. (eds) Feferman on Foundations. Outstanding Contributions to Logic, vol 13. Springer, Cham. https://doi.org/10.1007/978-3-319-63334-3_9

Download citation

Publish with us

Policies and ethics

Search

Navigation