Hostname: page-component-74656f9884-c52kr Total loading time: 0 Render date: 2026-11-07T21:45:35.711Z Has data issue: false hasContentIssue false
  • English
  • Français

Realizability algebras III: some examples

Published online by Cambridge University Press:  03 May 2016

JEAN-LOUIS KRIVINE
JEAN-LOUIS KRIVINE*
Affiliation:
University Paris-Diderot - C.N.R.S., France Email: jean-louis.krivine@pps.univ-paris-diderot.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We use the technique of “classical realizability” to build new models of ZF + DC in which R is not well ordered. This gives new relative consistency results, which are not obtainable by forcing. This gives also a new method to get programs from proofs of arithmetical formulas with dependent choice.

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 28 , Issue 1 , January 2018 , pp. 45 - 76
Copyright
Copyright © Cambridge University Press 2016 

References

Berardi, S., Bezem, M. and Coquand, T. (1998). On the computational content of the axiom of choice. Journal of Symbolic Logic 63 (2) 600–622.Google Scholar
Curry, H.B. and Feys, R. (1958). Combinatory Logic, North-Holland.Google Scholar
Friedman, H. (1973). The consistency of classical set theory relative to a set theory with intuitionistic logic. Journal of Symbolic Logic 38 (2) 315–319.Google Scholar
Friedman, H. (1977). Classically and intuitionistically provably recursive functions. In: Muller, G.H. and Scott, D.S. (eds.) Higher Set Theory. Springer Lect. Notes in Math., volume 669 21–27.Google Scholar
Girard, J.-Y. (1971). Une extension de l'interprétation fonctionnelle de Gödel à l'analyse. Proc. 2nd Scand. Log. Symp., North-Holland 63–92.Google Scholar
Griffin, T. (1990). A formulæ-as-type notion of control. In: Conf. record 17th A.C.M. Symp. on Principles of Progr. Languages, San Francisco, A.C.M. Press 47–58.Google Scholar
Howard, W. (1980). The formulas–as–types notion of construction. In: Seldin, J.P. and Hindley, J.R. (eds.) Essays on Combinatory Logic, λ-Calculus, and Formalism, Acad. Press 479–490.Google Scholar
Hyland, J.M.E. (1981). The effective topos. The L.E.J. Brouwer Centenary Symposium, Noordwijkerhout 165–216, Stud. Logic Foundations Math., 110, North-Holland, Amsterdam-New York, 1982.Google Scholar
Kreisel, G. (1951). On the interpretation of non-finitist proofs I. Journal of Symbolic Logic 16 248–26.Google Scholar
Kreisel, G. (1952). On the interpretation of non-finitist proofs II. Journal of Symbolic Logic 17 43–58.CrossRefGoogle Scholar
Krivine, J.-L. (2001). Typed lambda-calculus in classical Zermelo-Fraenkel set theory. Archive for Mathematical Logic 40 (3) 189–205. http://www.pps.univ-paris-diderot.fr/~krivine/articles/zf_epsi.pdf Google Scholar
Krivine, J.-L. (2003). Dependent choice, ‘quote’ and the clock. Theoretical Computer Science 308 259–276. http://www.pps.univ-paris-diderot.fr/~krivine/articles/quote.pdf Google Scholar
Krivine, J.-L. (2007). Realizability: A machine for Analysis and set theory. Geocal'06 (febr. 2006 - Marseille); Mathlogaps'07 (June 2007 - Aussois). http://www.pps.univ-paris-diderot.fr/~krivine/articles/Mathlog07.pdf Google Scholar
Krivine, J.-L. (2009). Realizability in classical logic. In: Interactive Models of Computation and Program Behaviour. Panoramas et synthèses, volume 27, Société Mathématique de France 197–229. http://www.pps.univ-paris-diderot.fr/~krivine/articles/Luminy04.pdf Google Scholar
Krivine, J.-L. (2011). Realizability algebras: A program to well order ℝ. Logical Methods in Computer Science 7 (3:02) 1–47.Google Scholar
Krivine, J.-L. (2012). Realizability algebras II: New models of ZF + DC. Logical Methods in Computer Science 8 (1:10) 1–28.Google Scholar
Miquel, A. (2011). Forcing as a program transformation. In: Logic in Computer Science (LICS'11), Toronto, Canada 197–206.Google Scholar