Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-27T20:58:36.796Z Has data issue: false hasContentIssue false
  • English
  • Français

Lifschitz' realizability

Published online by Cambridge University Press:  12 March 2014

Jaap van Oosten
Jaap van Oosten*
Affiliation:
Faculteit Wiskunde en Informatica, Universiteit Van Amsterdam, 1018 TV Amsterdam, The Netherlands
Get access Rights & Permissions [Opens in a new window]

Abstract

V. Lifschitz defined in 1979 a variant of realizability which validates Church's thesis with uniqueness condition, but not the general form of Church's thesis. In this paper we describe an extension of intuitionistic arithmetic in which the soundness of Lifschitz' realizability can be proved, and we give an axiomatic characterization of the Lifschitz-realizable formulas relative to this extension. By a “q-variant” we obtain a new derived rule. We also show how to extend Lifschitz' realizability to second-order arithmetic. Finally we describe an analogous development for elementary analysis, with partial continuous application replacing partial recursive application.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 55 , Issue 2 , June 1990 , pp. 805 - 821
Copyright
Copyright © Association for Symbolic Logic 1990

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

Dragalin, A. G. [1979], Mathematical intuitionisnu introduction to proof theory, “Nauka”, Moscow; English translation, American Mathematical Society, Providence, Rhode Island, 1988.Google Scholar
Hyland, J. M. E. [1982], The effective topos, The L.E.J. Brouwer centenary symposium (Troelstra, A. S. and van Dalen, D., editors), North-Holland, Amsterdam, pp. 165–216.Google Scholar
Kleene, S. C. [1969], Formalized recursive functionals and formalized realizability, Memoirs of the American Mathematical Society, no. 89 (1969).Google Scholar
Kleene, S. C. and Vesley, R. E. [1965], The foundations of intuitionistic mathematics, North-Holland, Amsterdam.Google Scholar
Lifschitz, V. [1979], CT0is stronger than CT0!, Proceedings of the American Mathematical Society, vol. 73, pp. 101–106.Google Scholar
Troelstra, A. S. (editor) [1973], Metamathematical investigation of intuitionistic arithmetic and analysis, Lectures Notes in Mathematics, vol. 344, Springer-Verlag, Berlin.CrossRefGoogle Scholar
Troelstra, A. S. and van Dalen, D. [1988], Constructivism in mathematics, North-Holland, Amsterdam.Google Scholar