Skip to main content
Log in

Realizability and intuitionistic logic

  • Published:
Synthese Aims and scope Submit manuscript

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

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Bibliography

  • Aczel, P. H. G.: 1980, ‘The Type Theoretic Interpretation of Constructive Set Theory, in A. Macintyre, L. Pacholski, and J. Paris (eds), Logic Colloquium 77, North-Holland Publ. Co., Amsterdam, pp. 55–66.

    Google Scholar 

  • Beeson, M.: 1979, ‘Goodman's Theorem and Beyond’, Pacific Journal of Mathematics 84, 1–16.

    Google Scholar 

  • Beeson, M.: 1979A, ‘A Theory of Constructions and Proofs’. Preprint no. 134, Department of Mathematics, Utrecht University.

  • Beeson, M.: 1980, ‘Recursive Models for Constructive Set Theories’. Preprint 129, Department of Mathematics, Utrecht University.

  • Bruijn, N. G. de: 1970, ‘The Mathematical Language AUTOMATH, Its Usage, and Some of Its Extensions’, in M. Laudet, D. lacombe, L. Nolin, and M. Schützenberger (eds), Symposium on Automatic Demonstration, Springer Verlag, Berlin, pp. 29–61.

    Google Scholar 

  • Celluci, C.: 1981, ‘A Calculus of Constructions as a Representation of Intuitionistic Logical Proofs’, in S. Bernini (ed.), Atti del congresso nazionale di logica, Montecatini Terme, 1–5 ottobre 1979, Bibliopolis, Napoli, pp. 175–193

    Google Scholar 

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

    Google Scholar 

  • Diller, J.: 1980, ‘Modified Realisation and the Formulae-as-Types Notion’, in J. P. Seldin, J. R. Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, pp. 491–501.

    Google Scholar 

  • Dummett, M. A. E.: 1977, Elements of Intuitionism, Clarendon Press, Oxford.

    Google Scholar 

  • Feferman, S.: 1975, ‘A Language and Axioms for Explicit Mathematics’, in J. Crossley (ed.), Algebra and Logic, Springer, Berlin, pp. 87–139.

    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 

  • Gödel, K.: 1958, ‘Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica 12, 280–287.

    Google Scholar 

  • Goodman, N.: 1970, ‘A Theory of Constructions Equivalent to Arithmetic’, in A. Kino, J. Myhill and R. E. Vesley (eds.), Intuitionism and Proof Theory, North-Holland Publ. Co., Amsterdam, pp. 101–120.

    Google Scholar 

  • Hilbert D., and P. Bernays: 1934, Grundlagen der Mathematik I, Springer-Verlag, Berlin, 19682.

    Google Scholar 

  • Heyting, A.: 1934, Mathematische Grundlagenforschung, Intuitionismus, Beweistheorie, Springer, Berlin. Reprinted 1974.

    Google Scholar 

  • Heyting, A.: 1956, Intuitionism, An Introduction, North-Holland Publ. Co., Amsterdam, 19662, 19713.

    Google Scholar 

  • Heyting, A.: 1958, ‘Intuitionism in Mathematics’, in R. Klibansky (ed.) Philosophy in the Mid-century. A Survey, La nuova editrice, Firenza, pp. 101–115.

  • Heyting, A.: 1974, ‘Intuitionistic Views on the Nature of Mathematics’, Bolletino dell' Unione Mathematica Italiana (4)9, Supplemento, 122–134. Also in Synthese 27 1974, 79–81.

  • Howard, W. A.: 1980, ‘The Formulae-As-Types Notion of Construction’, in J. P. Seldin, and J. R. Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, London-New York, pp. 479–490.

    Google Scholar 

  • Kleene, S. C.: 1945, ‘On the Interpretation of Intuitionistic Number Theory’, J. Symbolic Logic 10, 109–124.

    Google Scholar 

  • Kleene, S. C.: 1960, ‘Realizability and Šanin's Algorithm for the Constructive Deciphering of Mathematical Sentences’, Logique et Analyse 3, 154–165.

    Google Scholar 

  • Kleene, S. C. and R. E. Vesley: 1965, The Foundations of Intuitionistic Mathematics, North-Holland Publ. Co. Amsterdam.

    Google Scholar 

  • Kleene, S. C.: 1973, ‘Realizability: A Retrospective Survey’, in A. R. D. Mathias and H. Rogers (eds.), Cambridge Summer School in Mathematical Logic, Springer, Berlin, pp. 95–112.

    Google Scholar 

  • Kolmogorov, A. N.: 1932, ‘Zur Deutung der intuitionistischen Logik’, Math. Zeitschrift 35, 58–65.

    Google Scholar 

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

    Google Scholar 

  • Kreisel, G.: 1970, ‘Church's Thesis: A Kind of Reducibility Axiom for Constructive Mathematics’, in A. Kino, J. Myhill and R. E. Vesley (eds.), Intuitionism and Proof Theory, North-Holland, Amsterdam, pp. 121–150.

    Google Scholar 

  • Kreisel, G.: 1971, ‘A Survey of Proof Theory II’, in J. E. Fendstad (ed.), Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam, pp. 109–170.

    Google Scholar 

  • Läuchli, H.: 1970, ‘An Abstract Notion of Realizability for Which Intuitionistic Predicate Calculus is Complete’, in A. Kino, J. Myhill, and R. E. Vesley (eds.), Intuitionism and Proof theory, North-Holland Publ. Co., Amsterdam, pp. 227–234.

    Google Scholar 

  • Martin-Löf, P.: 1975, ‘An intuitionistic Theory of Types: Predicative Part’, in H. E. Rose and J. C. Shepherdson (eds.), Logic colloquium '73, North-Holland Publ. Co., Amsterdam, pp. 73–118.

    Google Scholar 

  • Martin-Löf, P: 1975A, ‘About Models for Intuitionistic Type Theories and the Notion of Definitional Equality’, in S. Kanger (ed.) Proceedings of the Third Scandinavian Logic Symposium, North-Holland Publ. Co., Amsterdam, pp. 81–109.

    Google Scholar 

  • Martin-Löf, P.: 1982, ‘Constructive Mathematics and Computer Programming’. Reports of the Dept. of Mathematics, University of Stockholm, 1979, no. 11. Appeared in L. S. Cohen, J. Los, H. Pfeiffer and K. P. Podewski (eds.), Logic, Methodology and Philosophy of Science VI, North-Holland Publ. Co., Amsterdam, pp. 153–175.

    Google Scholar 

  • Pitts, A. M.: 1981, ‘The Theory of Triposes’, Ph.D. thesis, Cambridge University, U.K.

    Google Scholar 

  • Šanin, N. A.: 1958, ‘On the Constructive Interpretation of Mathematical Judgments’, Trudy Mat. Inst. Steklov 52, 226–311 (Russian). English translation: Am. Math. Soc. Transl. (2) 23 (1963), 109–189.

    Google Scholar 

  • Scott, D. A.: 1970, ‘Constructive Validity’, in M. Laudet, D. Lacombe, L. Nolin, and M. Schützenberger (eds.), Symposium on Automatic Demonstration, Springer Verlag, Berlin, pp. 237–275.

    Google Scholar 

  • Sundholm, G.: 1983, ‘Constructions, Proofs and the Meaning of Logical Constants’, J. Philosophical Logic 12, 151–172.

    Google Scholar 

  • Troelstra, A. S.: 1973, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer, Berlin, Ch. I–IV.

    Google Scholar 

  • Troelstra, A. S.: 1977, ‘A Note on Non-extensional Operations in Connection with Continuity and Recursiveness’, Indag. Math, 39, 455–462.

    Google Scholar 

  • Troelstra, A. S.: 1980, ‘The Interplay between Logic and Mathematics: Intuitionism’, in E. Agazzi (ed.), Modern Logic — A Survey, D. Reidel, Dordrecht, pp. 197–221.

    Google Scholar 

  • van Dalen, D.: 1973, ‘Lectures on Intuitionism’, in A. R. D. Mathias and H. Rogers (eds.), Cambridge Summer School in Mathematical Logic. Springer, Berlin, pp. 1–94.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints and permissions

About this article

Cite this article

Diller, J., Troelstra, A.S. Realizability and intuitionistic logic. Synthese 60, 253–282 (1984). https://doi.org/10.1007/BF00485463

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00485463

Keywords

Navigation