Hostname: page-component-586b7cd67f-rcrh6 Total loading time: 0 Render date: 2024-11-22T23:09:30.205Z 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: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

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

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

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