Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-26T06:55:50.207Z Has data issue: false hasContentIssue false
  • English
  • Français

Interpreting classical theories in constructive ones

Published online by Cambridge University Press:  12 March 2014

Jeremy Avigad
Jeremy Avigad*
Affiliation:
Department of Philosophy, Carnegie-Mellon University, Pittsburgh, PA 15213, USA, E-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

A number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 65 , Issue 4 , December 2000 , pp. 1785 - 1812
Copyright
Copyright © Association for Symbolic Logic 2000

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 strength of Martin-Löf's intuitionistic type theory with one universe, Proceedings of the symposiums of mathematical logic, Oulu 1974 and Helsinki 1975 (Miettinen, Seppo and Väänänen, Jouko, editors), Department of Philosophy, University of Helsinki, 1977.Google Scholar
[2]Aczel, Peter, The type theoretic interpretation of constructive set theory, Logic colloquium '77 (Macintyre, A., Pacholski, L., and Paris, J., editors), North-Holland, Amsterdam, 1978, pp. 55–66.CrossRefGoogle Scholar
[3]Aczel, Peter, The type theoretic interpretation of constructive set theory: choice principles, L. E. J. Brouwer centenary symposium (Troelstra, A. S. and van Dalen, D., editors), North-Holland, Amsterdam, 1982, pp. 1–40.Google Scholar
[4]Avigad, Jeremy and Sommer, Richard, The model-theoretic ordinal analysis of predicative theories, this Journal, vol. 64 (1999), pp. 327–349.Google Scholar
[5]Barwise, Jon, Admissible sets and structures, Springer, Berlin, 1975.CrossRefGoogle Scholar
[6]Beeson, Michael J., Foundations of constructive mathematics, Springer, Berlin, 1985.CrossRefGoogle Scholar
[7]Buchholz, Wilfried, The Ωμ+1-rule, [8], 1981, pp. 188–233.CrossRefGoogle Scholar
[8]Buchholz, Wilfried, Feferman, Solomon, Pohlers, Wolfram, and Sieg, Wilfried, Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies, Lecture Notes in Mathematics, no, 897, Springer, Berlin, 1981.Google Scholar
[9]Burr, Wolfgang, Fragments of Heyting-arithmetic, preprint, 1998.Google Scholar
[10]Cook, Stephen A. and Urquhart, Alasdair, Functional interpretations of feasibly constructive arithmetic, Annals of Pure and Applied Logic, vol. 63 (1993), pp. 103–200.CrossRefGoogle Scholar
[11]Coquand, Thierry and Hofmann, Martin, A new method for establishing conservativity of classical systems over their intuitionistic version, Mathematical Structures in Computer Science, vol. 9 (1999), pp. 323–333.CrossRefGoogle Scholar
[12]Friedman, Harvey M., Subsystems of set theory and analysis, Ph.D. thesis, Massachusetts Institute of Technology, 1967.Google Scholar
[13]Friedman, Harvey M., The consistency of classical set theory relative to a set theory with intuitionistic logic, this Journal, vol. 38 (1973), no. 2, pp. 315–319.Google Scholar
[14]Friedman, Harvey M., Classically and intuitionistically provable functions, Higher set theory (Miiller, H. and Scott, D., editors). Lecture Notes in Mathematics, no. 669, Springer, Berlin, 1978, pp. 21–27.CrossRefGoogle Scholar
[15]Griffor, E. and Rathjen, M., The strength of some Martin-Löf type theories, Archive for Mathematical Logic, vol. 33 (1994), pp. 347–385.CrossRefGoogle Scholar
[16]Jäger, Gerhard, Theories for admissible sets: A unifying approach to proof theory, Bibliopolis, Napoli, 1986.Google Scholar
[17]Martin-Löf, Per, An intuitionistic theory of types, 1972, manuscript, reprinted in Twenty-five years of constructive type theory, Oxford University Press, 1998, pp. 127–172.Google Scholar
[18]Palmgren, Erik, Type-theoretic interpretation of iterated, strictly positive inductive definitions, Archive for Mathematical Logic, vol. 32 (1992), pp. 75–99.CrossRefGoogle Scholar
[19]Parikh, Rohit, Existence and feasibility in arithmetic, this Journal, vol. 36 (1971), pp. 494–508.Google Scholar
[20]Rathjen, Michael, The proof-theoretic characterization of the primitive recursive set functions, this Journal, vol. 57 (1992), pp. 954–969.Google Scholar
[21]Simpson, Stephen G., Subsystems of second-order arithmetic, Springer, Berlin, 1998.Google Scholar
[22]Troelstra, A. S., Metamathematical investigation ofintuitionistic arithmetic and analysis, Lecture Notes in Mathematics, no. 344, Springer, Berlin, 1973.CrossRefGoogle Scholar
[23]van Dalen, Dirk, Logic and structure, third ed., Springer, Berlin, 1997.Google Scholar