Hostname: page-component-78c5997874-4rdpn Total loading time: 0 Render date: 2024-11-19T03:15:29.976Z Has data issue: false hasContentIssue false
  • English
  • Français

Functional interpretation and inductive definitions

Published online by Cambridge University Press:  12 March 2014

Jeremy Avigad  and
Henry Towsner
Jeremy Avigad
Affiliation:
Department of Philosophy and Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, Pa 15213, USA, E-mail: [email protected]
Henry Towsner
Affiliation:
University of California, Los Angeles 520 Portola Plaza Math Sciences Building 6363 Mailcode: 155505 Los Angeles, Ca 90095, USA, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Extending Gödel's Dialectica interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 74 , Issue 4 , December 2009 , pp. 1100 - 1120
Copyright
Copyright © Association for Symbolic Logic 2009

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, Peter, The type theoretic interpretation of constructive set theory, Logic Colloquium '77, North-Holland, Amsterdam, 1978, pp. 55–66.CrossRefGoogle Scholar
[2]Aehlig, Klaus, On fragments of analysis with strengths of finitely iterated inductive definitions, Ph.D. thesis, University of Munich, 2003.Google Scholar
[3]Avigad, Jeremy, A variant of the double-negation translation, Technical Report CMU-PHIL 179, Carnegie Mellon.Google Scholar
[4]Avigad, Jeremy, Predicative functionals and an interpretation of , Annals of Pure and Applied Logic, vol. 92 (1998), pp. 1–34.CrossRefGoogle Scholar
[5]Avigad, Jeremy, Interpreting classical theories in constructive ones, this Journal, vol. 65 (2000), pp. 1785–1812.Google Scholar
[6]Avigad, Jeremy and Feferman, Solomon, Gödel'sfunctional (“Dialectica”) interpretation, Handbook of proof theory, North-Holland, Amsterdam, 1998, pp. 337–405.CrossRefGoogle Scholar
[7]Buchholz, Wilfried, The Ωμ+1-rule, In Buchholz et al. [9], pp. 188–233.CrossRefGoogle Scholar
[8]Buchholz, Wilfried, Ordinal analysis of IDν, In Buchholz et al. [9], pp. 234–260.CrossRefGoogle Scholar
[9]Buchholz, Wilfried, Feferman, Solomon, Pohlers, Wolfram, and Sieg, Wilfried, Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies, Lecture Notes in Mathematics, vol. 897, Springer, Berlin, 1981.Google Scholar
[10]Burr, Wolfgang, A Diller-Nahm-style functional interpretation of KPω, Archive for Mathematical Logic, vol. 39 (2000), pp. 599–604.CrossRefGoogle Scholar
[11]Diller, J. and Nahm, W., Eine Variante zur Dialectica Interpretation der Hey ting-Arithmetik endlicher Typen, Archiv für mathematische Logik und Grundlagenforschung, vol. 16 (1974), pp. 49–66.CrossRefGoogle Scholar
[12]Feferman, Solomon, Ordinals associated with theories for one inductively defined set, unpublished paper, 1968.Google Scholar
[13]Ferreira, Fernando and Oliva, Paulo, Bounded functional interpretation, Annals of Pure and Applied Logic, vol. 135 (2005), pp. 73–112.CrossRefGoogle Scholar
[14]Friedman, Harvey M., Classically and intuitionistically provable functions, Higher set theory (Müller, H. and Scott, D., editors), Lecture Notes in Mathematics, vol. 669, Springer, Berlin, 1978, pp. 21–27.CrossRefGoogle Scholar
[15]Gödel, Kurt, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, vol. 12 (1958), pp. 280–287, reprinted with English translation in [16], pp. 241–251.CrossRefGoogle Scholar
[16]Gödel, Kurt, Collected works, (Feferman, Solomonet al., editors), vol. II, Oxford University Press, New York, 1990.Google Scholar
[17]Howard, W. A., Functional interpretation of bar induction by bar recursion, Compositio Mathematica, vol. 20 (1968), pp. 107–124.Google Scholar
[18]Howard, W. A., A system of abstract constructive ordinals, this Journal, vol. 37 (1972), pp. 355–374.Google Scholar
[19]Jäger, Gerhard, Theories for admissible sets: A unifying approach to proof theory, Bibliopolis, Napoli, 1986.Google Scholar
[20]Kleene, S. C., Arithmetical predicates and function quantifiers, Transactions of the American Mathematical Society, vol. 79 (1955), pp. 312–340.CrossRefGoogle Scholar
[21]Kleene, S. C., Hierarchies of number-theoretic predicates, Bulletin of the American Mathematical Society, vol. 61 (1955), pp. 193–213.CrossRefGoogle Scholar
[22]Kohlenbach, Ulrich, Some logical metatheorems with applications in functional analysis, Transactions of the American Mathematical Society, vol. 357 (2005), pp. 89–128.CrossRefGoogle Scholar
[23]Kohlenbach, Ulrich, Applied proof theory: Proof interpretations and their use in mathematics, Springer, to appear.Google Scholar
[24]Kohlenbach, Ulrich and Oliva, Paulo, Proof mining: a systematic way of analyzing proofs in mathematics, Trudy Matematicheskogo Instituia Imeni V. A. Steklova, vol. 242 (2003), pp. 147–175, (Mat. Logika i Algebra).Google Scholar
[25]Kreisel, Georg, Generalized inductive definitions, Stanford Report on the Foundations of Analysis (mimeographed), 1963.Google Scholar
[26]Pohlers, Wolfram, An upper bound for the provability of transfinite induction in systems with N-times iterated inductive definitions, ISILCproof theory Symposion, Lecture Notes in Mathematics, vol. 500, Springer, Berlin, 1975, pp. 271–289.CrossRefGoogle Scholar
[27]Pohlers, Wolfram, Proof theoretical analysis of IDν by the method of local predicativity, In Buchholz et al. [9], pp. 261–357.CrossRefGoogle Scholar
[28]Schwichtenberg, Helmut, Proof theory: Some aspects of cut-elimination, Handbook of mathematical logic (Barwise, Jon, editor), North-Holland, Amsterdam, 1977, pp. 867–895.CrossRefGoogle Scholar
[29]Shoenfield, Joseph R., Mathematical logic, Association for Symbolic Logic, Urbana, IL, 2001, reprint of the 1973 second printing.Google Scholar
[30]Sieg, Wilfried, Trees in metamathematics: theories of inductive definitions and subsystems of analysis, Ph.D. thesis, Stanford University.Google Scholar
[31]Sieg, Wilfried, Inductive definitions, constructive ordinals, and normal derivations, In Buchholz et al. [9], pp. 143–187.CrossRefGoogle Scholar
[32]Stein, Martin, Interpretationen der Heyting-Arithmetik endlicher Typen, Archiv für mathematische Logik und Grundlagenforschung, vol. 19 (1978),pp. 175–189.CrossRefGoogle Scholar
[33]Streicher, Thomas and Kohlenbach, Ulrich, Shoenfield is Gödel after Krivine, Mathematical Logic Quarterly, vol. 53 (2007), pp. 176–179.CrossRefGoogle Scholar
[34]Tait, William, Applications of the cut elimination theorem to some subsystems of classical analysis, Intuition and proof theory (Kino, A., Myhill, J., and Vesley, R. E., editors), North-Holland, Amsterdam, 1970, pp. 475–488.Google Scholar
[35]Troelstra, A. S., Introductory note to 1958 and 1972, In Feferman et al. [16], pp. 217–241.Google Scholar
[36]Zucker, J. I., Iterated inductive definitions, trees, and ordinals, Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer, Berlin, 1973, pp. 392–453.CrossRefGoogle Scholar