Advertisement

The Unintended Interpretations of Intuitionistic Logic

  • Wim Ruitenburg

Abstract

We present an overview of the unintended interpretations of intuitionistic logic that arose after Heyting formalized the “observed regularities” in the use of formal parts of language, in particular, first-order logic and Heyting Arithmetic. We include unintended interpretations of some mild variations on “official” intuitionism, such as intuitionistic type theories with full comprehension and higher order logic without choice principles or not satisfying the right choice sequence properties. We conclude with remarks on the quest for a correct interpretation of intuitionistic logic.

Keywords

Recursive Function Predicate Logic Intuitionistic Logic Kripke Model Axiom Schema 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barendregt, H.P. (1984), The Lambda Calculus, Its Syntax and Semantics, rev. ed., Studies in Logic and the Foundations of Mathematics, Vol. 103, North-Holland, Amsterdam.MATHGoogle Scholar
  2. Barwise, J. (ed.) (1977), Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Vol. 90, North-Holland, Amsterdam.Google Scholar
  3. Barzin, M. and Errera, A. (1927), Sur la logique de M. Brouwer, Acad. Roy. Belg. Bull. CI. Sci. 5, No. 13, 56–71.Google Scholar
  4. Beeson, M.J. (1985), Foundations of Constructive Mathematics, Ergebnisse der Mathematik und ihrer Grenzgebiete 3. Folge, Band 6, Springer-Verlag, Berlin.MATHGoogle Scholar
  5. Bertin, E.M.J., Bos, H.J.M. and Grootendorst, A.W. (eds.), (1978), Two Decades of Mathematics in the Netherlands 1920–1940, Part I. Centre for Mathematics and Computer Science, Amsterdam.Google Scholar
  6. Beth, E.W. (1956), Semantic construction of intuitionistic logic, Med. Konink. Nederl. Akad. Wetensch., new series 19, No. 11.Google Scholar
  7. Beth, E.W. (1959), The Foundations of Mathematics, North-Holland, Amsterdam.MATHGoogle Scholar
  8. Bishop, E. (1967), Foundations of Constructive Analysis, McGraw-Hill, New York.MATHGoogle Scholar
  9. Brouwer, L.E.J. (1925), Intuitionistische Zerlegung mathematischer Grundbegriffe, Jahresber. Deutsch. Math.-Verein. 33, 251–256.MATHGoogle Scholar
  10. Brouwer, L.E.J. (1975a), Collected Works, Vol. I, Philosophy and Foundations of Mathematics, A. Heyting (ed.), North-Holland, Amsterdam.Google Scholar
  11. Brouwer, L.E.J. (1975b), Collected Works, Vol. II, Geometry, Analysis, Topology, and Mechanics, H. Freudenthal (ed.), North-Holland, Amsterdam.Google Scholar
  12. Brouwer, L.E.J. (1981a), Over de Grondslagen der Wiskunde, Ph.D. 1907, with additions from D.J. Korteweg, G. Mannoury, and D. van Dalen (ed.), (1981a), CWI Varia, Vol. 1, Centre for Mathematics and Computer Science, Amsterdam.Google Scholar
  13. Brouwer, L.E.J. (1981b), Brouwer’s Cambridge Lecture Notes, with preface and notes by D. van Dalen (ed.), Cambridge University Press, Cambridge, UK.Google Scholar
  14. Buss, S.R. (1985a), Bounded Arithmetic, Ph.D. Thesis.Google Scholar
  15. Buss, S.R. (1985b), The polynomial hierarchy and intuitionistic bounded arithmetic, preprint.Google Scholar
  16. Cohen, P.J. (1966), Set Theory and the Continuum Hypothesis, Benjamin, New York.MATHGoogle Scholar
  17. Crossley, J.N. Dummett, M.A.E. (eds.), (1965), Formal Systems and Recursive Functions, North-Holland, Amsterdam.MATHGoogle Scholar
  18. van Dalen, D. (1982), Braucht die konstruktive Mathematik Grundlagen?, Jahresber. Deutsch. Math.-Verein. 84, 57–78.MATHMathSciNetGoogle Scholar
  19. Fourman, M.P. Mulvey, C.J. Scott, D.S. (eds.), (1979), Applications of Sheaves, Lecture Notes in Mathematics 753, Springer, New York.MATHGoogle Scholar
  20. Freyd, P. (1964), Abelian Categories, Harper and Row, New York.MATHGoogle Scholar
  21. Freyd, P. (1972), Aspects of topoi, Bull. Austral. Math. Soc. 7, 1–76.MATHCrossRefMathSciNetGoogle Scholar
  22. Glivenko, V. (1928), Sur la logique be M. Brouwer, Acad. Roy. Belg. Bull. CI. Sci. 5, No. 14, 225–228.Google Scholar
  23. Glivenko, V. (1929), Sur quelques points de la logique de M. Brouwer, Acad. Roy. Belg. Bull. CI. Sci. 5, No. 15, 183–188.Google Scholar
  24. Gödel, K. (1932), Zum intuitionistischen Aussagenkalkül, Anzeiger der Akademie der Wissenschaften in Wien, 69, 65–66.Google Scholar
  25. Gödel, K. (1933a), Zur intuitionistischen Arithmetik und Zahlentheorie, Ergebnisse eines mathematischen Kolloquiums 4, 34–38.Google Scholar
  26. Gödel, K. (1933b), Eine Interpretation des intuitionistischen Aussagenkalküls, Ergebnisse eines mathematischen Kolloquiums 4, 39–40.Google Scholar
  27. Gödel, K. (1958), Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica 12, 280–287.MATHCrossRefMathSciNetGoogle Scholar
  28. Gödel, K. (1986), Kurt Gödel, Collected Work, Vol. I, S. Feferman, J.W. Dawson, S.C. Kleene, G.H. Moore, R.M. Solovay, J. van Heijenoort (eds.), Oxford University Press/Clarendon Press, Oxford.Google Scholar
  29. Goldblatt, R. (1978), Arithmetical necessity, provability, and intuitionistic logic, Theoria 44, 38–46.MATHMathSciNetCrossRefGoogle Scholar
  30. Goldblatt, R. (1979), Topoi, the Categorial Analysis of Logic, Studies in Logic and the Foundations of Mathematics, vol. 98, North-Holland, Amsterdam.MATHGoogle Scholar
  31. Gray, J.W. (1979), Fragments of the history of sheaf theory, in Fourman et al. (1979), pp. 1–79.CrossRefGoogle Scholar
  32. Heyting, A. (1930a), Die formalen Regeln der intuitionistischen Logik, Sitzungsberichte der preußischen Akademie von Wissenschaften, Physikalisch-mathematische Klasse, pp. 42–56.Google Scholar
  33. Heyting, A. (1930b), Die formalen Regeln der intuitionistischen Mathematik II, Sitzungsberichte der preußischen Akademie von Wissenschaften, Physikalisch-mathematische Klasse, pp. 57–71.Google Scholar
  34. Heyting, A. (1930c), Die formalen Regeln der intuitionistischen Mathematik III, Sitzungsberichte der preußischen Akademie von Wissenschaften, Physikalisch-mathematische Klasse, pp. 158–169.Google Scholar
  35. Heyting, A. (1934), Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie, Ergebnisse der Mathematik und ihrer Grenzgebiete 3. Folge, Band 4, Springer-Verlag, Berlin.Google Scholar
  36. Heyting, A. (1956), Intuitionism, an Introduction, Studies in Logic and the Foundations of Mathematics, Vol. 34, North-Holland, Amsterdam.MATHGoogle Scholar
  37. Hilbert, D. and Bernays, P. (1934), Grundlagen der Mathematik, Vol. 1, Springer-Verlag, Berlin.Google Scholar
  38. Hyland, J.M.E. (1982), The effective topos, in Troelstra and van Dalen (1982), pp. 165–216.Google Scholar
  39. Hyland, J.M.E., Johnstone, P.T. and Pitts, A.M. (1980), Tripos theory, Math. Proc. Comb. Philos. Soc. 88, 205–232.MATHCrossRefMathSciNetGoogle Scholar
  40. Johnstone, P.T. (1977), Topos Theory, L.M.S. Monographs, Vol. 10, Academic Press, New York.MATHGoogle Scholar
  41. Keisler, H.J. (1973), Forcing and the omitting types theorem, in Morley (1973), pp. 96–133.Google Scholar
  42. Kleene, S.C. (1945), On the interpretation of intuitionistic number theory, J. Symbolic Logic 10, 109–124.MATHCrossRefMathSciNetGoogle Scholar
  43. Kleene, S.C. (1973), Realizability: A retrospective survey, in Mathias and Rogers (1973), pp. 95–112.CrossRefGoogle Scholar
  44. Kock, A. (1981), Synthetic Differential Geometry, London Mathematical Society Lecture Note Series, Vol. 51, Cambridge University Press, Cambridge, UK.MATHGoogle Scholar
  45. Kolmogorov, A.N. (1925), O principe tertium non datur (Sur le principe de tertium non datur), Mat. Sbornik (Recueil mathematique de la societé mathematique de Moscou) 32, 646–667. (English translation in van Heijenoort (1967))MATHGoogle Scholar
  46. Kreisel, G. (1962), Foundations of intuitionistic logic, in Nagel et al. (1962), pp. 198–210.Google Scholar
  47. Kripke, S.A. (1959), Semantical analysis of modal logic, J. Symbolic Logic 24, 323–324.MathSciNetGoogle Scholar
  48. Kripke, S.A. (1965), Semantical analysis of intuitionistic logic I, in Crossley and Dummett (1965), pp. 92–130.CrossRefGoogle Scholar
  49. Lawvere, F.W. (ed.), (1972), Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, Springer-Verlag, New York.MATHGoogle Scholar
  50. Mac Lane, S. (1971), Categories for the Working Mathematician, Graduate Texts in Mathematics, vol. 5, Springer-Verlag, New York.MATHGoogle Scholar
  51. Maehara, S. (1954), Eine Darstellung der intuitionistischen Logik in der Klassischen, Nagoya Math. J. 7, 45–64.MATHMathSciNetGoogle Scholar
  52. Markov, A.A. (1962), On constructive mathematics, Trudy Mat. Inst. Steklov 67, 8–14; English translation in Amer. Math. Soc. Transl. 98, 2nd series (1971), 1–9.MATHMathSciNetGoogle Scholar
  53. Mathias, A.R.D. and Rogers, H. (eds.), (1973), Cambridge Summer School in Mathematical Logic, Lecture Notes in Mathematics 337, Springer-Verlag, New York.MATHGoogle Scholar
  54. McKinsey, J.C.C. and Tarski, A. (1948), Some theorems about the sentential calculi of Lewis and Heyting, J. Symbolic Logic 13, 1–15.MATHCrossRefMathSciNetGoogle Scholar
  55. Mikkelsen, C.J. (1976), Lattice-Theoretic and Logical Aspects of Elementary Topoi, Århus Universitet Various Publications 25, Aarhus University.Google Scholar
  56. Mitchell, W. (1972), Boolean topoi and the theory of sets, J. Pure Appl. Algebra 2, 261–274.MATHCrossRefMathSciNetGoogle Scholar
  57. Morley, M.D. (ed.), (1973), Studies in Model Theory, MAA Studies in Mathematics 8, The Mathematical Association of America, New York.MATHGoogle Scholar
  58. Mostowski, A. (1948), Proof on non-deducibility in intuitionistic functional calculus, J. Symbolic Logic 13, 204–207.MATHCrossRefMathSciNetGoogle Scholar
  59. Nagel, E., Suppes, P. and Tarski, A. (eds.), (1962), Logic Methodology, and Philosophy of Science, Stanford University Press, Stanford, CA.MATHGoogle Scholar
  60. Paré, R. (1974), Colimits in topoi, Bull. Amer. Math. Soc. 80, 556–561.MATHCrossRefMathSciNetGoogle Scholar
  61. Prawitz, D. (1965), Natural Deduction, A Proof-Theoretical Study, Almqvist & Wiksell, Stockholm.MATHGoogle Scholar
  62. Rasiowa, H. and Sikorski, R. (1953a), On satisfiability and deducibility in non-classical functional calculi, Bull. Acad. Polon. Sci. CI. 3, 229–231.MathSciNetGoogle Scholar
  63. Rasiowa, H. and Sikorski, R. (1953b), Algebraic treatment of the notion of satisfiability, Fund. Math. 40, 62–95.MATHMathSciNetGoogle Scholar
  64. Rasiowa, H. and Sikorski, R. (1963), The Mathematics of Metamathematics, PWN-Polish Scientific Publishers, Warsaw.MATHGoogle Scholar
  65. Šanin, N.A. (1958), On the constructive interpretation of mathematical judgments, Trudy Mat. Inst. Steklov 52, 226–311; English translation in Amer. Math. Soc. Transl. 23, 2nd series (1963), 109–189.MathSciNetGoogle Scholar
  66. Ščedrov, A. (1984), Forcing and Classifying Topoi, Mem. Amer. Math. Soc, Vol. 48, Nr. 295, American Mathematical Society, Providence, RI.Google Scholar
  67. Scott, D.S. (1979), Identity and existence in intuitionistic logic, in Fourman et al. (1979), pp. 660–696.CrossRefGoogle Scholar
  68. Smoryński, C. (1973), Applications of Kripke models, in Troelstra (1973), pp. 324–391.Google Scholar
  69. Solovay, R.M. (1976), Provability interpretations of modal logic, Israel J. Math. 25, 287–304.MATHCrossRefMathSciNetGoogle Scholar
  70. van Stigt, W.P. (1982), L.E.J. Brouwer, the signific interlude, in Troelstra and van Dalen (1982), pp. 505–512.Google Scholar
  71. Stockmeyer, L.J. (1976), The polynomial-time hierarchy, Theoret. Comput. Sci. 3, 1–22.CrossRefMathSciNetGoogle Scholar
  72. Stone, M.H. (1937), Topological representation of distributive lattices and Brouwerian logics, Casopis Pest. Mat. Fys. 67, 1–25.Google Scholar
  73. Tarski, A. Der Aussagenkalkül und die Topologie, Fund. Math. 31, 103–134.Google Scholar
  74. Tierney, M. (1972), Sheaf theory and the continuum hypothesis, in Lawvere (1972), pp. 13–42.CrossRefGoogle Scholar
  75. Troelstra, A.S. (ed.), (1973), Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics 344, Springer-Verlag, New York.MATHGoogle Scholar
  76. Troelstra, A.S. (1977), Aspects of constructive mathematics, in Barwise (1977), pp. 973–1052.CrossRefGoogle Scholar
  77. Troelstra, A.S. (1978), A. Heyting on the formalization of intuitionistic mathematics, in Bertin et al. (1978), pp. 153–175.Google Scholar
  78. Troelstra, A.S. (1981), Arend Heyting and his contribution to intuitionism, Nieuw Arch. Wisk. 29, 3rd series, No. 1, 1–23.MATHMathSciNetGoogle Scholar
  79. Troelstra, A.S. and van Dalen, D. (eds.), (1982), The L.E.J. Brouwer Centenary Symposium, Studies in Logic and the Foundations of Mathematics, Vol. 110, North-Holland, Amsterdam.MATHGoogle Scholar
  80. van Heijenoort, J. (ed.), (1967), From Frege to Gödel. A Source Book in Mathematical Logic, 1879–1931, Harvard University Press, Cambridge, MA.MATHGoogle Scholar
  81. Whitehead, A.N. and Russell, B. (1925), Principia Mathematica, “Second edition, vol. I, Cambridge University Press, 1925; “Second edition, vol. II,” Cambridge University Press, 1927; “Second edition, vol. III,” Cambridge University Press, 1927. Cambridge, UK.Google Scholar

Copyright information

© Birkhäuser Boston 2008

Authors and Affiliations

  • Wim Ruitenburg
    • 1
  1. 1.Department of Mathematics, Statistics, and Computer ScienceMarquette UniversityMilwaukeeUSA

Personalised recommendations