Skip to main content
SpringerLink
Log in

Constructive Kripke Semantics and Realizability

  • Conference paper
Logic from Computer Science

Part of the book series: Mathematical Sciences Research Institute Publications ((MSRI,volume 21))

Abstract

What is the truth-value structure of realizability? How can realizability style models be integrated with forcing techniques from Kripke and Beth semantics, and conversely? These questions have received answers in Hyland’s [33], Läuchli’s [43] and in other, related or more syntactic developments cited below. Here we re-open the investigation with the aim of providing more constructive answers to both questions. A special, constructive class of so-called fallible Beth models has been shown intuitionistically to be complete for intuitionistic logic by Friedman, Veldman and others. Here we build such intuitionistic Beth models elementarily equivalent to a natural and broad class of readabilities, thus showing that realizability interpretations correspond to the particularly effective kind of models yielded by the Veldman — Friedman — de Swart completeness theorem. In the other direction, an abstract realizability is shown constructively to be complete for intuitionistic logic. This extends earlier results along these lines due to Läuchli and others.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

  1. Beeson, M. J. [1985], Foundations of Constructive Mathematics, Springer-Verlag, Berlin.

    MATH  Google Scholar 

  2. Beeson, M. J. [1982], “Recursive models of constructive set theories”, Annals of Mathematical Logic 23, 127–178.

    Article  MathSciNet  MATH  Google Scholar 

  3. Beth, E. W. [1956], “Semantic construction of intuitionistic logic”, Koninklijke Nederlandse Akademie van Wetenschappen, Niewe Serie 19/11, 357–388.

    MathSciNet  Google Scholar 

  4. Beth, E. W. [1947], “Semantical considerations on intuitionistic mathematics”, Koninklijke Nederlandse Akademie van Wetenschappen, Proceedings of the Section of Sciences.

    Google Scholar 

  5. Boileau, A. and A. Joyal [1981], “La logique des topos”, Journal of Symbolic Logic 46, 6–16.

    Article  MathSciNet  MATH  Google Scholar 

  6. Buss, S. [1989], “On model theory for intuitionistic bounded arithmetic with applications to independence results”, to appear.

    Google Scholar 

  7. Cohen, P. J. [1966], Set Theory and the Continuum Hypothesis, W. A. Benjamin Inc., New York.

    MATH  Google Scholar 

  8. Cohen, P. J. [1963], “The independence of continuum hypothesis”, Proceedings of the National Academy of Science, USA 50, 1143–1148.

    Article  Google Scholar 

  9. Constable, R. L., et al [1986], Implementing Mathematics with the NUPRL Development System, Prentice-Hall, N.J.

    Google Scholar 

  10. Constable, R. L. [1986], “The semantics of evidence”, Cornell CS Technical Report, Ithaca, N.Y.

    Google Scholar 

  11. Constable, R. L. [1983], “Programs as proofs”, Information Processing Letters, 16(3), 105–112.

    Article  MathSciNet  MATH  Google Scholar 

  12. Cook, S. A. and Urquhart [1988], “Functional interpretations of feasible constructive arithmetic”, Technical Report 210/88, Department of Computer Science, University of Toronto, June 1988.

    Google Scholar 

  13. Coquand, T. [1990], “On the analogy between propositions and types”, in: Logic Foundations of Functional Programming, Addison-Wesley, Reading, MA.

    Google Scholar 

  14. Coquand, T. and G. Huet [1985], “Constructions: A higher order proof system for mechanizing mathematics”, EUROCAL 85, Linz, Austria.

    Google Scholar 

  15. Dragalin, A. G. [1987], Mathematical Intuitionism: Introduction to Proof Theory, Translations of Mathematical Monographs 67, AMS, Providence, R.I.

    Google Scholar 

  16. Dragalin, A. G. [1979], “New kinds of realizability”, Sixth International Congress, Logic, Methodology and Philosophy of Science (Hannover, August 1979), Abstracts of Reports, Hannover.

    Google Scholar 

  17. Dummett, M. [1977], Elements of Intuitionism, Clarendon Press, Oxford.

    MATH  Google Scholar 

  18. Dyson, V. H. and G. Kreisel [1961], “Analysis of Beth’s semantic construction of intuitionistic logic”, Technical Report No. 3, Applied Mathematics and Statistics Laboratories, Stanford University.

    Google Scholar 

  19. Feferman, S. [1979], “Constructive theories of functions and classes”, in Boffa, M., D. van Dalen and K. McAloon (eds.), Logic Colloquium ’78: Proceedings of the Logic Colloquium at Mons, 1978, 159–224, North-Holland, Amsterdam.

    Google Scholar 

  20. Feferman, S. [1975], “A language and axioms for explicit mathematics”, in: Algebra and Logic, Lecture Notes in Mathematics 450, 87–139, Springer, Berlin.

    Google Scholar 

  21. Fitting, M. [1983], Proof Methods for Modal and Intuitionistic Logics, D. Reidel, Dordrecht, The Netherlands.

    MATH  Google Scholar 

  22. Fourman, M. P. and D. S. Scott [1979], “Sheaves and logic”, in: Fourman, Mulvey and Scott, (eds.), Applications of Sheaves, Mathematical Lecture Notes 753, 302–401, Springer-Ver lag, Berlin.

    Chapter  Google Scholar 

  23. Friedman, H. [1977], “The intuitionistic completeness of intuitionistic logic under Tarskian Semantics”, unpublished abstract, State University of New York at Buffalo.

    Google Scholar 

  24. Friedman, H. [1975], x201C;“Intuitionistic completeness of Heyting’s Predicate Calculus”, Notices of the American Mathematical Society, 22 A-648.

    Google Scholar 

  25. Friedman, H. [1973], “Some applications of Kleene’s methods for intuitionistic systems”, in: A. R. D. Mathias (ed.), Cambridge Summer School in Mathematical Logic, Cambridge, Aug. 1971, Lecture Notes in Mathematics 337, Springer-Verlag, Berlin.

    Google Scholar 

  26. Gabbay, D. G. [1981], Semantical Investigations in Heyting’s Intuitionistic Logic, D. Reidel, Dordrecht, The Netherlands.

    MATH  Google Scholar 

  27. Goodman, N. [1978], “Relativized realizability intuitionistic arithmetic of all finite types”, Journal of Symbolic Logic 43, 23–44.

    Article  MathSciNet  MATH  Google Scholar 

  28. Grayson, R. J. [1983], “Forcing in intuitionistic systems without power set”, Journal of Symbolic Logic 48, 670–682.

    Article  MathSciNet  MATH  Google Scholar 

  29. Hayashi, S. and H. Nakano [1989], PX: A Computational Logic, The MIT Press, Cambridge.

    Google Scholar 

  30. Heyting, A. [1956], Intuitionism: an Introduction, North-Holland, Amsterdam.

    MATH  Google Scholar 

  31. Hyland, J. M. E., E. P. Robinson and G. Rosolini [1988], “The discrete objects in the effective topos”, Manuscript.

    Google Scholar 

  32. Hyland, J. M. E. [1987], “A small complete category”, Lecture delivered at the Conference “Church’s Thesis after 50 years”, to appear in Annals of Pure and Applied Logic.

    Google Scholar 

  33. Hyland, J. M. E. [1982], “The effective topos”, in: Troelstra, A. S. and D. S. van Dalen (eds.), L. E. J. Brouwer Centenary Symposium, North-Holland, Amsterdam.

    Google Scholar 

  34. Hyland, J. M. E., P. T. Johnstone and A. M. Pitts [1980], “Tripos Theory”, Math. Proceedings of the Cambridge Phil. Society 88, 205–252.

    Article  MathSciNet  MATH  Google Scholar 

  35. Jaskowsky, S. [1936], “Recherches sur le Systeme de la logique intuitioniste”, in: Actes du Congres International de Philosophie Scientifique, Paris, Septembre, 1935, Vol. VI, 58–61, translation: Studia Logica 34, (1975), 117–120.

    Google Scholar 

  36. Kleene, S. C. [1973], “Realizability: A retrospective survey”, in: Mathias, A. R. D. (ed.), Cambridge Summer School in Mathematical Logic, Cambridge, Aug. 1971, Lecture Notes in Mathematics 337, Springer-Verlag, Berlin.

    Google Scholar 

  37. Kleene, S. C. [1969], “Formalized recursive functionals and formalized realizability”, Memoirs of the American Mathematical Society No. 89, American Mathematics Society, Providence, R.I.

    Google Scholar 

  38. Kleene, S. C. [1952], Introduction to Metamathematics, North-Holland (1971 edition), Amsterdam.

    Google Scholar 

  39. Kleene, S. C. [1945], “On the interpretation of intuitionistic number theory”, Journal of Symbolic Logic 10, 109–124.

    Article  MathSciNet  MATH  Google Scholar 

  40. Kreisel, G. and A. S. Troelstra [1970], “Formal systems for some branches of intuitionistic analysis”, Annals of Mathematical Logic 1, 229–387.

    Article  MathSciNet  MATH  Google Scholar 

  41. Kripke, S. [1965], “Semantical analysis of intuitionistic logic I”, in: Crossley, J. N. and M. Dummett (eds.), Formal Systems and Recursive Functions, Proceedings of the Eighth Logic Colloquium, Oxford, 1963, North-Holland, Amsterdam, 92–130.

    Chapter  Google Scholar 

  42. Lambek, J. and P. J. Scott [1986], Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics 7, Cambridge.

    MATH  Google Scholar 

  43. Läuchli, H. [1970], “An abstract notion of realizability for which predicate calculus is complete”, in: Myhill, J., A. Kino, and R. E. Vesley (eds.), Intuitionism and Proof Theory, North-Holland, Amsterdam, 227–234.

    Google Scholar 

  44. Lawvere, W. [1971], “Quantifiers and sheaves”, in: Actes du Congres International des Mathematiciens, 1–10, Septembre 1970, Nice, France, Vol. I., 329–334, Gauthier-Villars, Paris.

    Google Scholar 

  45. Leivant, D. [1976], “Failure of completeness properties of intuitionistic predicate logic for constructive models”, Annales Scientifiques de l’Universite de Clermont No. 60 (Math. No. 13), 93–107.

    MathSciNet  Google Scholar 

  46. Lipton, J. [1990], “Relating Kripke Models and readability”, Ph. D. dissertation, Cornell University.

    Google Scholar 

  47. Lipton, J. [1990], “Realizability and Kripke Forcing”, to appear in the Annals of Mathematics and Artificial Intelligence, Vol. 4, North Holland, published in revised and expanded form as Technical Report TR 90–1163, Dept. of Computer Science, Cornell.

    Google Scholar 

  48. Lipton, J. [1990], Some Kripke Models for “one-universe” Martin-Löf Type Theory, Technical Report TR 90–1162, Dept. of Computer Science, Cornell University, Oct. 1990.

    Google Scholar 

  49. Lipton, J. [1991], Constructive Kripke Models, Realizability and Deduction, technical report, to appear.

    Google Scholar 

  50. Lopez-Escobar, E. G. K. and W. Veldman [1975], “Intuitionistic completeness of a restricted second-order logic”, ISLIC Proof Theory Symposium (Kiel, 1974), Lecture Notes in Mathematics 500, Springer-Verlag, 198–232.

    Google Scholar 

  51. McCarty, D. C. [1986], “Realizability and recursive set theory”, Annals of Pure and Applied Logic 32, 11–194.

    Article  MathSciNet  Google Scholar 

  52. McCarty, D. C. [1984], “Realizability and recursive mathematics”, Doctoral Dissertation, Computer Science Department, Carnegie-Mellon University.

    Google Scholar 

  53. McKinsey, J. C. C. and A. Tarski [1948], “Some theorems on the sentential calculi of Lewis and Heyting”, Journal of Symbolic Logic 13, 1–15.

    Article  MathSciNet  MATH  Google Scholar 

  54. Makkai, M. and G. Reyes [1977], “First order categorical logic”, Lecture Notes in Mathematics 611, Springer-Verlag, Berlin.

    Google Scholar 

  55. Mitchell, J. and E. Moggi [1987], “Kripke-style models for typed lambda calculus”, Proceedings from Symposium on Logic in Computer Science, Cornell University, June 1987, IEEE, Washington, D.C.

    Google Scholar 

  56. Mulry, P. S. [1985], “Adjointness in recursion”, Annals of Pure and Applied Logic 32, 281–289.

    Article  MathSciNet  Google Scholar 

  57. Mulry, P. S. [1980], “The topos of recursive sets”, Doctoral Dissertation, SUNY-Buffalo.

    Google Scholar 

  58. Murthy, C, [1990], “Extracting constructive content from classical proofs: Compilation and the foundations of mathematics”, Ph. D. dissertation, Cornell University.

    Google Scholar 

  59. Nerode, A., J. B. Remmel and A. Scedrov [1989], “Polynomially graded logic I: A graded version of System T”, MSI Technical Report 89-21, Cornell University, Ithaca, N.Y, to appear in the proceedings of the Summer Workshop on Feasible Mathematics, Cornell.

    Google Scholar 

  60. Nerode, A. [1989], “Lectures on Intuitionistic Logic II”, MSI Technical Report 89–56, Cornell University, Ithaca, N.Y.

    Google Scholar 

  61. Nerode, A. [1989], “Some lecures on Intuitionistic Logic I”, Proceedings on Summer School on Logical Foundations of Computer Science, CIME, Montecatini, 1988, Springer-Verlag, Berlin.

    Google Scholar 

  62. Odifreddi, G. [1989], Classical Recursion Theory, North-Holland, Amsterdam.

    MATH  Google Scholar 

  63. Piotkin, G. , [1980], “Lambda definability in the full type hierarchy”, in: Seldin, J.P. and J. R. Hindley (eds.), To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, Academic Press, New York.

    Google Scholar 

  64. Robinson, E. [1988], “How complete is PER?”, Technical Report 88–229, Queen’s University, Department of Computing and Information Science.

    Google Scholar 

  65. Rosolini, G., [1986], “Continuity and Effectiveness in Topoi”, Ph. D. Dissertation, Oxford Univ.; also, report CMU-CS-86–123, department of Computer Science, Carnegie-Mellon University.

    Google Scholar 

  66. Scedrov, A. [1990], “Recursive realizability semantics for the calculus of constructions”, in: Logical Foundations of Functional Programming, Addison-Wesley, Reading, MA.

    Google Scholar 

  67. Scedrov, A. [1985], “Intuitionistic Set Theory”, in Harvey Friedman’s Research on the Foundations of Mathematics, North-Holland, Amsterdam.

    Google Scholar 

  68. Smorynski, C. A. [1973], “Applications of Kripke models”, in: A. S. Troelstra (ed.), Metamathematical Investigations of Intuitionistic Arithmetic and Analysis, Lecture Notes in Math. 344, Springer-Verlag, Amsterdam, 324–391.

    Chapter  Google Scholar 

  69. Smullyan, R. M. [1968], First-Order Logic, Springer-Ver lag, Berlin.

    MATH  Google Scholar 

  70. Stein, M. [1980], “Interpretation of Heyting’s arithmetic—an analysis by means of a language with set symbols”, Annals of Mathematical Logic 19, North-Holland, Amsterdam.

    Google Scholar 

  71. Swart, H. C. M. de [1978], “First steps in intuitionistic model theory”, Journal of Symbolic Logic 43, 3–12.

    Article  MathSciNet  MATH  Google Scholar 

  72. Swart, H. C. M. de [1976], “Another intuitionistic completeness proof”, Journal of Symbolic Logic 41, 644–662.

    Article  MathSciNet  MATH  Google Scholar 

  73. Szabo, M. E. [1978], “Algebra of proofs”, Studies in Logic and the Foundations of Mathematics, Vol. 88, North-Holland, Amsterdam.

    Google Scholar 

  74. Tait, W. W. [1975], “A realizability interpretation of the theory of species”, Logic Colloquium (Boston, Mass., 1972/73), Lecture Notes in Mathematics 453, Springer-Verlag, 240–251.

    Google Scholar 

  75. Tarski, A. [1956], Sentenial Calculus and Topology in Logic, Semantics, and Meta-mathematics, Clarendon Press, Oxford.

    Google Scholar 

  76. Troelstra, A. S. and D. van Dalen [1988], Constructivism in Mathematics: An Introduction, Vol. II, Studies in Logic and the Foundations of Mathematics, Vol. 123, North-Holland, Amsterdam.

    Google Scholar 

  77. Troelstra, A. S. [1977], Choice Sequences: A Chapter of Intuitionistic Mathematics, Clarendon Press, Oxford.

    MATH  Google Scholar 

  78. Troelstra, A. S. [1977], “Completeness and validity for intuitionistic predicate logic”, Colloque International de Logique (Clermont-Ferrand, 1975), Colloques Interna-tionaux du CNRS, no. 249, DNRS, Paris, 39–98.

    Google Scholar 

  79. Troelstra, A. S. [1973], Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Mathematical Lecture Notes 344, Springer-Verlag, Berlin.

    Book  Google Scholar 

  80. Troelstra, A. S. [1971], “Notions of realizability for intuitionistic arithmetic and intuitionistic arithmetic in all finite types”, in: J. E. Fenstad (ed.), Proceedings of the Second Scandinavian Logic Symposium, Oslo, 1970, North-Holland, 369–405.

    Google Scholar 

  81. Veldman, W. [1976], “An intuitionistic completeness theorem for intuitionistic predicate logic”, Journal of Symbolic Logic 41, 159–166.

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, Cornell University, UK

    James Lipton

  2. Dept. of Mathematics, University of Pennsylvania, 19104, Philadephia, PA, USA

    James Lipton

Authors
  1. James Lipton
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Mathematics, University of California at Los Angeles, 90024-1766, Los Angeles, CA, USA

    Yiannis N. Moschovakis

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag New York, Inc

About this paper

Cite this paper

Lipton, J. (1992). Constructive Kripke Semantics and Realizability. In: Moschovakis, Y.N. (eds) Logic from Computer Science. Mathematical Sciences Research Institute Publications, vol 21. Springer, New York, NY. https://doi.org/10.1007/978-1-4612-2822-6_13

Download citation

  • DOI: https://doi.org/10.1007/978-1-4612-2822-6_13

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4612-7685-2

  • Online ISBN: 978-1-4612-2822-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation