Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2024-12-26T13:25:12.287Z Has data issue: false hasContentIssue false
  • English
  • Français

Induction and inductive definitions in fragments of second order arithmetic

Published online by Cambridge University Press:  12 March 2014

Klaus Aehlig
Klaus Aehlig*
Affiliation:
Mathematisches Institut, Universität München, Theresienstr. 39, 80333 München, Germany,, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

A fragment with the same provably recursive functions as n iterated inductive definitions is obtained by restricting second order arithmetic in the following way. The underlying language allows only up to n + 1 nested second order quantifications and those are in such a way. that no second order variable occurs free in the scope of another second order quantifier. The amount of induction on arithmetical formulae only affects the arithmetical consequences of these theories, whereas adding induction for arbitrary formulae increases the strength by one inductive definition.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 70 , Issue 4 , December 2005 , pp. 1087 - 1107
Copyright
Copyright © Association for Symbolic Logic 2005

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

[1]Aczel, P., An introduction to inductive definitions, Handbook of Mathematical Logic (Barwise, J., editor), Studies in Logic and the Foundations of Mathematics, vol. 90, chapter C.7, North-Holland Publishing Company, 1977, pp. 739–782.CrossRefGoogle Scholar
[2]Aehlig, K., On fragments of analysis with strengths of finitely iterated inductive definitions, Ph.D. thesis, Ludwig-Maximilians-Universität München, 07 2003.Google Scholar
[3]Aehlig, K. and Johannsen, J., An elementary fragment of second-order lambda-calculus, ACM Transactions on Computational Logic, vol. 6 (2005), no. 2, pp. 468–480.CrossRefGoogle Scholar
[4]Altenkirch, T. and Coquand, T., A finitary subsystem of the polymorphic lambda-calculus, Proceedings of the 5th international conference on typed lambda caculi and applications (TLCA '01) (Abramsky, S., editor), Lecture Notes in Computer Science, vol. 2044, Springer Verlag, Berlin, 2001, pp. 22–28.CrossRefGoogle Scholar
[5]Arai, T., A slow growing analogue to Buchholz' proof, Annals of Pure and Applied Logic, vol. 54 (1991), pp. 101–120.CrossRefGoogle Scholar
[6]Buchholz, W., The Ωμ+1-rule, In Buchholz et al. [7], chapter IV, pp. 189–233.Google Scholar
[7]Buchholz, W., Feferman, S., Pohlers, W., and Sieg, W., Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies, Lecture Notes in Mathematics, vol. 897, Springer-Verlag, Berlin, 1981.Google Scholar
[8]Buchholz, W. and Schütte, K., Proof theory of impredicative subsystems of analysis, Studies in Proof Theory, vol. 2, Bibliopolis, Naples, 1988.Google Scholar
[9]Feferman, S., Formal theories for transfinite iterations of generalized inductive definitions, Intuitionism and proof theory (proceedings of the summer conference at Buffalo N. Y. 1968) (Kino, A., Myhill, J., and Vesley, R. E., editors), Studies in Logic and the Foundation of Mathematics, North-Holland Publishing Company, Amsterdam, 1970, pp. 303–326.CrossRefGoogle Scholar
[10]Grzegorczyk, A., Some classes of recursive functions, Rozprawy Matematyczne, vol. 4 (1953).Google Scholar
[11]Kalmár, L., Egyszerű példa eldönthetetlen aritmetikai problémára, Matematikai és Fizikai Lapok, vol. 50 (1943), pp. 1–23.Google Scholar
[12]Leivant, D., Finitely stratified polymorphism, Information and Computation, vol. 93 (1991), pp. 93–113.CrossRefGoogle Scholar
[13]Matthes, R., Extensions of system F by iteration and primitive recursion on monotone inductive types, Ph.D. thesis, Fakultät für Mathematik und Informatik der Ludwig-Maximilians-Universität München, 05 1998.Google Scholar
[14]Tait, W. W., Intensional interpretations of functional of finite type, I, this Journal, vol. 32 (1967), no. 2, pp. 198–212.Google Scholar
[15]Takeuti, G., Consistency proofs of subsystems of classical analysis, Annals of Mathematics, vol. 86 (1967), pp. 299–348.CrossRefGoogle Scholar