Skip to main content
SpringerLink
Log in

Intuitionistic Logic

  • Chapter
Handbook of Philosophical Logic

Part of the book series: Synthese Library ((SYLI,volume 166))

Abstract

Among the logics that deal with the familiar connectives and quantifiers two stand out as having a solid philosophical—mathematical justification. On the one hand there is classical logic with its ontological basis and on the other hand intuitionistic logic with its epistemic motivation. The case for other logics is considerably weaker; although one may consider intermediate logics with more or less plausible principles from certain viewpoints none of them is accompanied by a comparably compelling philosophy. For this reason we have mostly paid attention to pure intuitionistic theories.

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

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Aczel, P.: 1968, ‘Saturated intuitionistic theories’, in Schmidt, et al. [1968], pp. 1–11.

    Google Scholar 

  • Barendregt, H. P.: 1981, The Lambda Calculus. Its Syntax and Semantics, North-Holland, Amsterdam.

    Google Scholar 

  • Beeson, M.: 1979, ‘A theory of constructions and proofs’, Preprint No. 134. Dept. of Math. Utrecht University.

    Google Scholar 

  • Beeson, M.: 1985, Foundations of Constructive Mathematics. Metamathematical Studies, Springer-Verlag, Berlin.

    Book  Google Scholar 

  • Brouwer, L. E. J.: 1907, Over de Grondslagen der Wiskunde, Thesis, Amsterdam. Translation ‘On the foundations of mathematics’, in Brouwer [1975], pp. 11–101. New edition in Brouwer [ 1981 ].

    Google Scholar 

  • Brouwer, L. E. J.: 1908. J.: 1908, ‘De onbetrouwbaarheid der logische principes’, Tijdschrift voor wijsbegeerte 2, 152–158. Translation ‘The unreliability of the logical principles’ in [1975], pp. 107–111. Also in [ 1981 ].

    Google Scholar 

  • Brouwer, L. E. J.: 1918, ‘Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. I’, Koninklijke Nederlandse Akademie van Weten-schappen Verhandelingen le Sectie 12, no. 5, 43 p. Also in Brouwer [ 1975 ], pp. 150 – 190.

    Google Scholar 

  • Brouwer, L. E. J.: 1975, Collected Works, I, (A. Heyting) (ed.), North-Holland, Amsterdam.

    Google Scholar 

  • Brouwer, L. E. J.: 1981, Over de Grondslagen der Wiskunde, Aangevuld met Ongepub-liceerde Fragmenten, Correspondence met D. J. Korteweg. Recensies door G. Mannoury, etc., D. van Dalen (ed.), Mathematisch Centrum, varia 1, Amsterdam.

    Google Scholar 

  • Brouwer, L. E. J.: 1981a, Brouwer’s Cambridge Lectures on Intuitionism, D. van Dalen (ed.), Cambridge University Press, Cambridge.

    Google Scholar 

  • Burgess, J. P.: 1981, The completeness of intuitionistic propositional calculus for its intended interpretation’, Notre Dame J. Formal Logic 22, 17 – 28.

    Article  Google Scholar 

  • Chang, C. C. and Keisler, H. J.: 1973, Model Theory, North-Holland, Amsterdam.

    Google Scholar 

  • Curry, H. B. and Feys, R.: 1958, Combinatory Logic I, North-Holland, Amsterdam.

    Google Scholar 

  • Van Dalen, D.: 1973, ‘Lectures on intuitionism’, in Mathias and Rogers [1973], pp. 1–94.

    Google Scholar 

  • Van Dalen, D.: 1974, ‘A model for HAS. A topological interpretation of the theory of species of natural numbers’, Fund Math. 82, 167 – 174.

    Google Scholar 

  • Van Dalen, D.: 1977, ‘The use of Kripke’s Schema as a reduction principle’, J. Symbolic Logic 42, 238 – 240.

    Article  Google Scholar 

  • Van Dalen, D.: 1978, ‘An interpretation of intuitionistic analysis’, Ann. Math. Logic 13, 1 – 43.

    Article  Google Scholar 

  • Van Dalen, D.: 1980, Logic and Structure, Springer-Verlag, Berlin.

    Book  Google Scholar 

  • Van Dalen, D.: 1984, D.: 1984, ‘How to glue analysis models’, J. Symbolic Logic 49, pp. 1339– 1349.

    Google Scholar 

  • Van Dalen, D.: 198x, ‘Glueing of analysis models in an intuitionistic setting’. To appear.

    Google Scholar 

  • Van Dalen, D. and Statman, R.: 1979, ‘Equality in the presence of apartness’, in Hintikka et al. [ 1979 ], pp. 95 – 118.

    Google Scholar 

  • Davis, M. (ed.): 1965, The Undecidable. Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Raven Press, New York.

    Google Scholar 

  • Demuth, O. and KuSera, A.: 1979, ‘Remarks on constructive mathematical analysis’, in M. Boffa, D. van Dalen, and K. McAloon (eds.), Logic Colloquium ’78, North-Holland, Amsterdam, pp. 81 – 130.

    Google Scholar 

  • Dummett, M.: 1973, ‘The philosophical basis of intuitionistic logic’, in H. E. Rose and J. C. Sheperdson (eds.), Logic Colloquium ’73, North-Holland, Amsterdam, pp. 5–40. Also in Dummett, M.: 1978, Truth and Other Enigmas, Duckworth, London, pp. 215 – 247.

    Google Scholar 

  • Dummett, M.: 1977, Elements of Intuitionism, Oxford University Press, Oxford.

    Google Scholar 

  • Dyson, V. H. and Kreisel, G.: 1961, Analysis of Beth’s Semantic Construction of Intuitionistic Logic, Technical Report no. 3. Appl. math, and statistics lab. Stanford University, 65 pp.

    Google Scholar 

  • Feferman, S.: 1979, ‘Constructive theories of functions and classes’, in M. Boffa, D. van Dalen, and K. McAloon (eds.), Logic Colloquium ’78, North-Holland, Amsterdam, pp. 159 – 224.

    Google Scholar 

  • Fenstad, J. E. (ed.): 1971, Proceedings of the Second Scandanavian Logic Symposium, North-Holland, Amsterdam.

    Google Scholar 

  • Fine, K.: 1970, ‘An intermediate logic without the finite model property’ (unpublished).

    Google Scholar 

  • Fitting, M. C.: 1969, Intuitionistic Logic, Model Theory and Forcing, North-Holland, Amsterdam.

    Google Scholar 

  • Fourman, M.: 1982, ‘Notions of choice sequence’, in Troelstra and van Dalen [1982], pp.91–106.

    Google Scholar 

  • Fourman, M. P. and Scott, D. S.: 1979, ‘Sheaves and logic’, in Fourman, Mulvey, Scott [ 1979 ],pp. 302 – 401.

    Google Scholar 

  • Fourman, M. P., Mulvey, C. J., and Scott, D. S.: 1979, Applications of Sheaves. Proceedings Durham 1977, Lecture Notes No. 753, Springer-Verlag, Berlin.

    Google Scholar 

  • Fraenkel, A., Bar-Hillel, Y., Levy, A., and van Dalen, D.: 1973, Foundations of Set Theory, North-Holland, Amsterdam.

    Google Scholar 

  • Friedman, H.: 1975, ‘The disjunction property implies the numerical existence property’, Proc. Nat. Acad. Sci. 72, 2877 – 2878.

    Article  Google Scholar 

  • Friedman, H.: 1977, ‘The intuitionistic completeness of intuitionistic logic under Tarskian semantics’, Abstract, SUNY at Buffalo.

    Google Scholar 

  • Friedman, H.: 1977a, ‘New and old results on completeness of HPC’, Abstract, SUNY at Buffalo.

    Google Scholar 

  • Friedman, H.: 1977b, ‘Classically and intuitionistically provably recursive functions’, in Higher Set Theory, Springer-Verlag, Berlin, pp. 21 – 27.

    Google Scholar 

  • Gabbay, D. M.: 1970, ‘Decidability of the Kreisel-Putnam system’, J. Symbolic Logic 35, 431 – 437.

    Article  Google Scholar 

  • Gabbay, D. M.: 1977, ‘On some new intuitionistic propositional connectives’, Studia Logica 36, 127 – 139.

    Article  Google Scholar 

  • Gabbay, D. M.: 1981, Semantical Investigations in Hey ting’s Intuitionistic Logic, D. Reidel, Dordrecht.

    Google Scholar 

  • Gabbay, D. M. and De Jongh, D. H.: 1974, ‘Sequences of decidable finitely axiomatizable intermediate logics with the disjunction property’, J. Symbolic Logic 39, 67 – 79.

    Article  Google Scholar 

  • Gentzen, G.: 1933, ‘Über das Verhaltnis zwischen intuitionistischer und klassischer Arithmetik’, English translation in Szabo [1969], pp. 53 – 67.

    Google Scholar 

  • Girard, J. Y.: 1971, ‘Une extension de l’interpretation de Gödel a l’analyse et son application à l’élimination des coupures dans l’analyse et la théorie des types’, in Fenstad [ 1971 ] pp. 63 – 92.

    Google Scholar 

  • Glivenko, V.: 1929, ‘Sur quelques points de la logique de M. Brouwer’, Academie Royale de Belgique, Bull, de la class des sciences (5), Vol. 15, pp. 183–188.

    Google Scholar 

  • Goad, C. A.: 1978, ‘Monadic infinitary propositional logic: a special operator’, Repts Math. Logic 10, 43–50.

    Google Scholar 

  • Gödel, K.: 1932, Zum intuitionistischen AussagenkalkuF, Akademie der Wissenschaften in Wien. Math. - naturwiss. Klctsse. Anzeiger 69, 65–66. Also in Ergebnisse eines Math. Koll. 4, 42.

    Google Scholar 

  • Gödel, K.: 1933, ‘Zur intuitionistischen Arithmetik und Zahlentheorie’, Ergebnisse eines mathematischen Kolloqiums 4, 34–38. English translation in [Davis, 1965], pp. 75–81. Cf. J. Symbolic Logic 31(1966) 484 – 494.

    Google Scholar 

  • Gödel, K.: 1958, ‘Über eine bisher noch nicht beniitzte Erweiterung des finiten Stand-punktes’, Dialectica 12, 280–287. English translation in J. Philosophical Logic 9(1980) 133 – 142.

    Google Scholar 

  • Goldblatt, R.: 1979, Topoi. The Categorical Analysis of Logic, North-Holland, Amsterdam (revised edition, 1984 ).

    Google Scholar 

  • Gornemann, S.: 1971, A logic strong than intuitionism’, J. Symbolic Logic 36, 249 – 261.

    Article  Google Scholar 

  • Grayson, R.: 1981, ‘Concepts of general topology in constructive mathematics and in sheaves’, Ann. Math. Logic 20, 1 – 41.

    Article  Google Scholar 

  • Grayson, R.: 1984, ‘Heyting-valued semantics’, in G. Lolli, G. Longo, and A. Marcja (eds.), Logic Colloqium ’82, North-Holland, Amsterdam, pp. 181 – 208.

    Chapter  Google Scholar 

  • Grzegorczyk, A.: 1964, ‘A philosophically plausible interpretation of intuitionistic logic’, Indagationes Mathematicae 26, 569 – 601.

    Google Scholar 

  • Harrop, R.: 1958, ‘On the existence of finite models and decision procedures for propositional calculi’,Proc. Camb. Phil. Soc. 54,1–13.

    Google Scholar 

  • Hartog, W. den: 1978, ‘A Proof Theoretic Study. The Theory of Pseudo-Order as a Conservative Extension of the Theory of Apartness’, Dept. of Math. Rijksuniversi-teit Utrecht, Preprint no. 77.

    Google Scholar 

  • Heijenoort, J. van: 1967, From Frege to Gödel, A scource book in Mathematical Logic, 1879–1931, Harvard University Press, Cambridge Mass.

    Google Scholar 

  • Heyting, A.: 1930, A.: 1930, ‘Die formalen Regeln der intuitionistischen Logik’, Sitzungsberichte der preussischen Akademie von Wissenschaften, pp. 42–56. ‘Die formalen Regeln der intuitionistischen Mathematik’, Ibid. pp. 57–71, 158–169. Also (partly) in Two Decades of Mathematics in the Netherlands, Amsterdam, 1978.

    Google Scholar 

  • Heyting, A.: 1956, Intuitionism. An Introduction, North-Holland, Amsterdam.

    Google Scholar 

  • Hintikka, J., Niiniluoto, I., and Saarinen, E. (eds.): 1979, Essays on Mathematical and Philosophical Logic, D. Reidel, Dordrecht.

    Google Scholar 

  • Hoeven, G. van der and Moerdijk, I.: 1984, ‘Sheaf models for choice sequences’, Annals of Pure and Applied Logic 27, 63 – 107.

    Article  Google Scholar 

  • Hosoi, T.: 1967, ‘On intermediate logics, I’, J. Fac. Sci. Univ. of Tokyo 14, 293 – 312.

    Google Scholar 

  • Howard, W.: 1980, ‘The formulae-as-types notion of construction’, in Seldin and Hindley [1980], pp. 479–490.

    Google Scholar 

  • Hughes, G. E. and Cresswell, M. J.: 1968, An Introduction to Modal Logic, Methuen, London.

    Google Scholar 

  • Hull, R. C.: 1969, ‘Counterexamples in intuitionistic analysis using Kripke’s schema’, Z. Math. Logik und Grundlagen der Math. 15, 241 – 246.

    Article  Google Scholar 

  • Hyland, M.: 1982, ‘The effective topos’, in Troelstra and van Dalen [1982] pp. 165–216.

    Google Scholar 

  • Hyland, M., Johnstone, P. T. and Pitts, A. M.: 1980, ‘Tripos theory’, Math. Proc. Cambr. Phil. Soc. 88, 205 – 232.

    Article  Google Scholar 

  • Jankov, V. A.: 1968, ‘Constructing a sequence of strongly independent super-intuitionistic propositional calculi’, Soviet Math. Dok 9, 806 – 807.

    Google Scholar 

  • Jaskowski, S.: 1936, ‘Recherches sur le systeme de la logique intuitioniste’, Actes du Congrés Intern, de Phil. Scientifique. VI. Phil des mathématiques, Act. Sc. et Ind 393, Paris, pp. 58–61.

    Google Scholar 

  • Johansson, I.: 1936, ‘Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus’, Compositio Math. 4, 119 – 136.

    Google Scholar 

  • Jongh, D. H. de: 1980, ‘A class of intuitionistic connections’, in J. Barwise, H. J. Keisler and K. Kunen (eds.), The Kleene Symposium, North-Holland, Amsterdam, pp. 103 – 112.

    Chapter  Google Scholar 

  • Jongh, D. H. de and Smoryński, C.: 1976, ‘Kripke models and the intuitionistic theory of species’, Ann. Math. Logic 9, 157 – 186.

    Article  Google Scholar 

  • Kino, A., Myhill, J. and Vesley, R. E.: 1970, Intuitionism and Proof Theory. Proceedings of the Summer Conference at Buffalo, New York, 1968, North-Holland, Amsterdam.

    Google Scholar 

  • Kleene, S. C.: 1952, Introduction to Meta-mathematics, North-Holland, Amsterdam.

    Google Scholar 

  • Kleene, S. C.: 1973, ‘Readability: A retrospective survey’, in Mathias and Rogers [ 1973 ],pp. 95 – 112.

    Google Scholar 

  • Kleene, S. C. and Vesley, R. E.: 1965, The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions, North-Holland, Amsterdam.

    Google Scholar 

  • Klop, J. W.: 1980, Combinatory Reduction Systems, Thesis, Rijks Universiteit Utrecht. Also MC Tract 127. Math. Centre Amsterdam.

    Google Scholar 

  • Kolmogorov, A. N.: 1925, ‘On the principle of the excluded middle’ (Russian), Matematičeski Sbornik 32, 646–667. English translation in Van Heijenoort [ 1967 ], pp. 414 – 437.

    Google Scholar 

  • Kreisel, G.: 1958, ‘A remark on free choice sequences and the topological completeness proofs’, J. Symbolic Logic 23, 369 – 388.

    Article  Google Scholar 

  • Kreisel, G.: 1959, ‘Interpretations of analysis by means of constructive functional of finite type’, in A. Heyting (ed.), Constructivity in Mathematics, North-Holland, Amsterdam, pp. 101 – 128.

    Google Scholar 

  • Kreisel, G.: 1965, ‘Mathematical logic’, in T. L. Saaty (ed.), Lectures on Modern Mathematics III, Wiley & Sons, New York, pp. 95 – 195.

    Google Scholar 

  • Kreisel, G.: 1967, ‘Informal rigour and completeness proofs’, in I. Lakatos (ed.), Problems in the Philosophy of Mathematics, North-Holland, Amsterdam.

    Google Scholar 

  • Kreisel, G.: 1970, ‘Church’s Thesis, a kind of reducibility axiom of constructive mathematics’, in Kino et al. [1970], pp. 121–150.

    Google Scholar 

  • Kreisel, G. and Putnam, H.: 1957, ‘Eine Unableitbarkeitsbeweismethode fur den intuitionistischen Aussagenkalkul’, Archiv. f. math. Logik 3, 74 – 78.

    Article  Google Scholar 

  • Kreisel, G. and Troelstra, A. S.: 1970, ‘Formal systems for some branches of intuitionistic analysis’, Ann. Math. Logic 1, 229 – 387.

    Article  Google Scholar 

  • Kripke, S.: 1963, ‘Semantical analysis of intuitionistic logic I’, in J. Crossley and M. Dummett (eds.), Formal Systems and Recursive Functions, North-Holland, Amsterdam, pp. 92 – 129.

    Google Scholar 

  • Leivant, D.: 1976, ‘Failure of completeness properties of intuitionistic predicate logic for constructive models’, Ann. Sc. Univ. Clermont. Ser Math. 13, 93 – 107.

    Google Scholar 

  • Leivant, D.: 198x, ‘Syntactic translations and provably recursive functions’. To appear in the J. Symbolic Logic.

    Google Scholar 

  • Leivant, D.: 198y, ‘Intuitionistic formal systems’. To appear.

    Google Scholar 

  • Lemmon, E., and Scott, D. S.: 1966, ‘Intensional logics’, published in 1977 as An Introduction to Modal Logic, K. Segerberg (ed.), Blackwell, Oxford.

    Google Scholar 

  • Lifshits, V. A.: 1969, ‘Problems of decidability for some constructive theories of equalities’, in A. O. Slisenko (ed.), Studies in Constructive Mathematics and Mathematical Logic, ( Consultants Bureau, New York.

    Google Scholar 

  • Markov, A. A.: 1950, ‘Konstruktivnaja logika’, Usp. Mat. Nauk 5, 187 – 188.

    Google Scholar 

  • Martin-Lof, P.: 1977, ‘Hauptsatz for the theory of species’, in Fenstad [1971 ].

    Google Scholar 

  • Martin-Lof, P.: 1982, ‘Constructive mathematics and computer programming’, in L. J. Cohen, J. Los, H. Pfeiffer and K. P. Podewski (eds.), Logic, Methodology and Philosophy of Science VI, North-Holland, Amsterdam, pp. 153 – 179.

    Google Scholar 

  • Martin-Lof, P.: 1984, Intuitionistic Type Theory, Notes by G. Sambin of a series of lectures given in Padova, June 1982. Bibliopolis, Naples.

    Google Scholar 

  • Mathias, A. R. D. and Rogers, H. Jr.: 1973, Cambridge Summer School in Mathematical Logic, Springer Lecture Notes No. 337, Berlin.

    Google Scholar 

  • Maximova, L. L.: 1977, ‘Craig interpolation theorem and amalgamable varieties’, Soviet Math. Dok. 18, 1550 – 1553.

    Google Scholar 

  • Mine, G.: 1966, ‘Skolem’s method of elimination of positive quantifiers in sequential calculi’, Dokl. Akad. Nauk SSSR169, 861 – 864.

    Google Scholar 

  • Mine, G.: 1974, ‘On E-theorems’ (Russian), Investigation in constructive mathematics VI Zapisky Nauk. Sem. Leningrad Steklov Inst. 40,110–118.

    Google Scholar 

  • Moschovakis, J.: 1967, ‘Disjunction and existence in formalized intuitionistic analysis’, In J. N. Crossley (ed.), Sets, Models and Recursion Theory, North-Holland, Amsterdam, 309 – 331.

    Chapter  Google Scholar 

  • Moschovakis, J.: 1973, ‘A topological interpretation of second-order intuitionistic arithmetic’, Comp. Math. 26, 261 – 276.

    Google Scholar 

  • Moschovakis, J.: 1980, ‘A disjunctive decomposition theorem for classical theories’, in F. Richman (ed.), Constructive Mathematics, Springer Verlag, Berlin, pp. 250 – 259.

    Google Scholar 

  • Nelson, D.: 1949, ‘Constructive falsity’, J. Symbolic Logic 14, 16 – 26.

    Article  Google Scholar 

  • Nishimura, T.: 1966, ‘On formulas of one variable in intuitionistic propositional calculus’, J. Symbolic Logic 25, 327 – 331.

    Article  Google Scholar 

  • Ono, H.: 1972, ‘Some results on intermediate logics’, Publ. RIMS, Kyoto University8, 117 – 130.

    Article  Google Scholar 

  • Ono, H.: 1973, ‘A study of intermediate predicate logics’, Publ. RIMS Kyoto University8, 619 – 649.

    Article  Google Scholar 

  • Ono, H.: 198x, ‘Semantical analysis of predicate logics without the contraction rule’ (to appear in Studia Logica).

    Google Scholar 

  • Ono, H. and Komori, Y.: 198x, ‘Logics without the contraction rule’ (to appear in the J. Symbolic Logic).

    Google Scholar 

  • Posy, C. J.: 1976, ‘Varieties of indeterminacy in the theory of general choice sequences’, J.Phil. Logic 5, 91 – 132.

    Article  Google Scholar 

  • Posy, C. J.: 1977, ‘The theory of empirical sequences’, J. Philosophical Logic 6, 47 – 81.

    Article  Google Scholar 

  • Posy, C. J.: 1980, ‘On Brouwer’s definition of unextendable order’, History and Phil. Logic 1, 139 – 149.

    Article  Google Scholar 

  • Pottinger, G.: 1976, ‘A new way of normalizing intuitionist propositional logic’, Studia Logica 35, 387 – 408.

    Article  Google Scholar 

  • Prawitz, D.: 1965, Natural Deduction. A Proof Theoretical Study, Almqvist & Wiksell, Stockholm.

    Google Scholar 

  • Prawitz, D.: 1970, ‘Some results for intuitionistic logic with second-order quantification rules’, in Kino, Myhill, and Vesley [ 1970 ], pp. 259 – 270.

    Google Scholar 

  • Prawitz, D.: 1971, ‘Ideas and results in proof theory’, in J. E. Fenstad [1971 ].

    Google Scholar 

  • Prawitz, D.: 1977, ‘Meanings and proofs: on the conflict between classical and intuitionistic logic’, Theoria 43, 2 – 40.

    Article  Google Scholar 

  • Prawitz, D.: 1979, ‘Proofs and the meaning and the completeness of the logical constants’, in Hintikka et al. [1979], pp. 25–40.

    Google Scholar 

  • Prawitz, D and Malmnés, P.: 1968, ‘A survey of some connections between classical, intuitionistic and minimal logic’, in H. A. Schmidt et al., pp. 215–229.

    Google Scholar 

  • Rasiowa, H.: 1974, An Algebraic Approach to Non-Classical Logics, North-Holland, Amsterdam.

    Google Scholar 

  • Rasiowa, H. and Sikorski, R.: 1963, The Mathematics of Metamathematics, Panstwowe Wydawnictwo Naukowe Warszawa.

    Google Scholar 

  • Rauszer, C.: 1980, ‘An algebraic and Kripke-style approach to a certain extension of intuitionistic logic’, Dissertationes Mathematicae CLXVII, Warszawa, 67 pp.

    Google Scholar 

  • Rautenberg, W.: 1979, Klassische und nichtklassische Aussagenlogik, Vieweg & Sohn, Braunschweig/Wiesbaden.

    Book  Google Scholar 

  • Renardel de Lavalette, G. R.: 1981, ‘The interpolation theorem in fragments of logic’, Indag. Math. 43, 71 – 86.

    Google Scholar 

  • Schmidt, H. A., Schutte, K., and Thiele, H. J. (eds.): 1968, Contributions to Mathematical Logic, North-Holland, Amsterdam.

    Google Scholar 

  • Schiitte,K.: 1968, Vollständige Systeme modaler und intuitionistischer Logik, Ergebnisse der Mathematik und ihrer Grenzgebiete, 42, Springer-Verlag, Berlin.

    Book  Google Scholar 

  • Scott, D. S.: 1968, ‘Extending the topological interpretation to intuitionistic analysis’, Comp. Math. 20, 194 – 210.

    Google Scholar 

  • Scott, D. S.: 1970, ‘Extending the topological interpretation to intuitionistic analysis II’, in Kino, Myhill, and Vesley [ 1970 ], pp. 235 – 255.

    Google Scholar 

  • Scott, D. S.: ‘Identity and existence in intuitionistic logic’, in Fourman, Mulvey, and Scott[1979], pp.660–696.

    Google Scholar 

  • Segerberg, K.: 1968, ‘Propositional logics related to Heyting’s and Johansson’s’, Theoria 34, 26 – 61.

    Article  Google Scholar 

  • Seldin, J. P. and Hindley, J. R. (eds.): 1980, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, London.

    Google Scholar 

  • Shoenfield, J. R.: 1967, Mathematical Logic, Addison-Wesley, Reading, Mass.

    Google Scholar 

  • Smorynski, C.: 1973, ‘Investigation of Intuitionistic Formal Systems by Means of Kripke Models’, Diss. Univ. of Illinois.

    Google Scholar 

  • Smorynski, C.: 1973a, ‘Elementary intuitionistic theories’, J. Symbolic Logic 38, 102 – 134.

    Article  Google Scholar 

  • Smorynski, C.: 1977, ‘On axiomatizing fragments’, J. Symbolic Logic 42, 530 – 544.

    Article  Google Scholar 

  • Smorynski, C.: 1978, ‘The axiomatization problem for fragments’, Ann. Math. Logic 14, 193 – 221.

    Article  Google Scholar 

  • Smorynski, C.: 1982, ‘Non-standard models and constructivity’, in Troelstra and van Dalen [1982], 459–464.

    Google Scholar 

  • Stein, M.: 1980, ‘Interpretations of Heyting’s Arithmetic. An analysis by means of a language with set symbols’, Ann. Math. Logic 19, 1 – 31.

    Article  Google Scholar 

  • Sundholm, G.: 1983, ‘Constructions, proofs and the meanings of the logical constants’, J. Phil. Logic 12, 151 – 172.

    Article  Google Scholar 

  • Swart, H. C. M. de: 1976, ‘Another intuitionistic completeness proof’, J. Symbolic Logic 41, 644 – 662.

    Article  Google Scholar 

  • Szabo, M. E. (ed.): 1969, The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam.

    Google Scholar 

  • Tait, N.: 1975, ‘A readability interpretation of the theory of species’, in R. Parik (ed.), Logic Colloquium, Springer-Verlag, Berlin, 240 – 251.

    Chapter  Google Scholar 

  • Takahashi, M.: 1970, ‘Cut-elimination theorem and Brouwerian-valued models for intuitionistic type theory’, Comment. Math. Univ. St. Pauli 19, 55 – 72.

    Google Scholar 

  • Thomason, R. H.: 1969, ‘A semantical study of constructible falsity’, Z. Math. Logik und Grundlagen der Mathematik 15, 247 – 257.

    Article  Google Scholar 

  • Troelstra, A. S.: 1969, Principles of Intuitionism, Springer-Verlag, Berlin.

    Google Scholar 

  • Troelstra, A. S.: 1973, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer-Verlag, Berlin.

    Book  Google Scholar 

  • Troelstra, A. S.: 1973a, ‘Notes on intuitionistic second-order arithmetic’, in Mathias and Rogers [ 19 7 3 ], pp. 171–205.

    Google Scholar 

  • Troelstra, A. S.: 1977, Choice Sequences. A Chapter of Intuitionistic Mathematics, Oxford University Press, Oxford.

    Google Scholar 

  • Troelstra, A. S.: 1978, ‘Commentary on Heyting [1930]’, in Two Decades of Mathematics in the Netherlands, Part 5, Math. Centre, Amsterdam.

    Google Scholar 

  • Troelstra, A. S.: 1979, A supplement to ‘Choice Sequences’, Report 79–04 of the Math. Institute University of Amsterdam. 22 pp.

    Google Scholar 

  • Troelstra, A. S.: 1980, ‘The interplay between logic and mathematics: intuitionism’, in E. Agazzai (ed.),Modem Logic - A Survey, D. Reidel, Dordrecht, pp. 197 – 221.

    Google Scholar 

  • Troelstra, A. S.: 1981, ‘On a second-order propositional operator in intuitionistic logic’, Studia Logica 40, 113 – 140.

    Article  Google Scholar 

  • Troelstra, A. S.: 1981a, ‘Arend Heyting and his contribution to Intuitionism’, Nieuw Archief voor Wiskunde 24, pp. 1 – 23.

    Google Scholar 

  • Troelstra, A. S.: 1983, ‘Analyzing choice sequences’, J. Philosophical Logic 12, 197 – 260.

    Article  Google Scholar 

  • Troelstra, A. S. and Van Dalen, D. (eds.): 1982, The L. E. J. Brouwer Centenary Symposium, North-Holland, Amsterdam.

    Google Scholar 

  • Troelstra, A. S. and Van Dalen, D.: 198x, Constructivism in Mathematics, To appear.

    Google Scholar 

  • Veldman, W.: 1976, ‘An intuitionistic completeness theorem for intuitionistic predicate logic’, J. Symbolic Logic 41, 159 – 166.

    Article  Google Scholar 

  • Visser, A. ‘On the Completeness Principle: a study of provability in Heyting’s Arithmeticá, 1982, Annals Math. Logic 22, 263–295.

    Google Scholar 

  • Zucker, J. T. and Tragesser, R. S.: 1978, ‘The adequacy problem for inferential logic’, J. Philosophical Logic 7, 501–516.

    Google Scholar 

Download references

Authors
  1. Dirk Van Dalen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Imperial College, London, England

    D. Gabbay

  2. FNS, University of Tuebingen, West Germany

    F. Guenthner

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Van Dalen, D. (1986). Intuitionistic Logic. In: Gabbay, D., Guenthner, F. (eds) Handbook of Philosophical Logic. Synthese Library, vol 166. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-5203-4_4

Download citation

  • DOI: https://doi.org/10.1007/978-94-009-5203-4_4

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-94-010-8801-5

  • Online ISBN: 978-94-009-5203-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation