{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:12Z","timestamp":1753889772773,"version":"3.41.2"},"reference-count":18,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,2,27]],"date-time":"2012-02-27T00:00:00Z","timestamp":1330300800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Using the proof-program (Curry-Howard) correspondence, we give a new method\nto obtain models of ZF and relative consistency results in set theory. We show\nthe relative consistency of ZF + DC + there exists a sequence of subsets of R\nthe cardinals of which are strictly decreasing + other similar properties of R.\nThese results seem not to have been previously obtained by forcing.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:10)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":13,"title":["Realizability algebras II : new models of ZF + DC"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Jean-Louis","family":"Krivine","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,2,27]]},"reference":[{"key":"10.2168\/LMCS-8(1:10)2012_berardi","doi-asserted-by":"publisher","DOI":"10.2307\/2586854"},{"key":"10.2168\/LMCS-8(1:10)2012_curry","unstructured":"H.B. Curry, R. Feys.Combinatory Logic.North-Holland (1958)."},{"key":"10.2168\/LMCS-8(1:10)2012_easton","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(70)90012-4"},{"key":"10.2168\/LMCS-8(1:10)2012_fri1","doi-asserted-by":"publisher","DOI":"10.2307\/2272068"},{"key":"10.2168\/LMCS-8(1:10)2012_fri2","unstructured":"H. Friedman.Classically and intuitionistically provably recursive functions.In: Higher set theory. Springer Lect. Notes in Math. 669 (1977) p. 21-27."},{"key":"10.2168\/LMCS-8(1:10)2012_girard","doi-asserted-by":"crossref","unstructured":"J.Y. Girard.Une extension de l'interpr\u00e9tation fonctionnelle de G\u00f6del \u00e0 l'analyse.Proc. 2nd Scand. Log. Symp. (North-Holland) (1971) p. 63-92.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"10.2168\/LMCS-8(1:10)2012_griffin","doi-asserted-by":"crossref","unstructured":"T. Griffin.A formulae -as-type notion of control.Conf. record 17th A.C.M. Symp. on Principles of Progr. Languages (1990).","DOI":"10.1145\/96709.96714"},{"key":"10.2168\/LMCS-8(1:10)2012_grigorieff","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(71)90011-8"},{"key":"10.2168\/LMCS-8(1:10)2012_howard","unstructured":"W. Howard.The formulas-as-types notion of construction.Essays on combinatory logic,lbd-calculus, and formalism, J.P. Seldin and J.R. Hindley ed., Acad. Press (1980) p. 479-490."},{"key":"10.2168\/LMCS-8(1:10)2012_hyland","doi-asserted-by":"crossref","unstructured":"J. M. E. Hyland.The effective topos.The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), 165-216, Stud. Logic Foundations Math., 110, North-Holland, Amsterdam-New York, 1982.","DOI":"10.1016\/S0049-237X(09)70129-6"},{"key":"10.2168\/LMCS-8(1:10)2012_kreisel1","doi-asserted-by":"publisher","DOI":"10.2307\/2267908"},{"key":"10.2168\/LMCS-8(1:10)2012_kreisel2","doi-asserted-by":"publisher","DOI":"10.2307\/2267457"},{"key":"10.2168\/LMCS-8(1:10)2012_krivine1","doi-asserted-by":"publisher","DOI":"10.1007\/s001530000057"},{"key":"10.2168\/LMCS-8(1:10)2012_krivine2","unstructured":"J.-L. Krivine.Dependent choice, `quote' and the clock.Th. Comp. Sc., 308, p. 259-276 (2003). http:\/\/hal.archives-ouvertes.fr\/hal-00154478 Updated version at : http:\/\/www.pps.jussieu.fr\/ krivine\/articles\/quote.pdf"},{"key":"10.2168\/LMCS-8(1:10)2012_krivine3","unstructured":"J.-L. Krivine.Realizability in classical logic.InInteractive models of computation and program behaviour.Panoramas et synth\u00e8ses, Soci\u00e9t\u00e9 Math\u00e9matique de France, 27, p. 197-229 (2009). http:\/\/hal.archives-ouvertes.fr\/hal-00154500 Updated version at : http:\/\/www.pps.jussieu.fr\/ krivine\/articles\/Luminy04.pdf"},{"key":"10.2168\/LMCS-8(1:10)2012_krivine4","unstructured":"J.-L. Krivine.Realizability : a machine for Analysis and set theory.Geocal'06 (febr. 2006 - Marseille); Mathlogaps'07 (june 2007 - Aussois). http:\/\/cel.archives-ouvertes.fr\/cel-00154509 Updated version at : http:\/\/www.pps.jussieu.fr\/ krivine\/articles\/Mathlog07.pdf"},{"key":"10.2168\/LMCS-8(1:10)2012_krivine5","unstructured":"J.-L. Krivine.Structures de r\u00e9alisabilit\u00e9, RAM et ultrafiltre surNN.(2008) http:\/\/hal.archives-ouvertes.fr\/hal-00321410 Updated version at : http:\/\/www.pps.jussieu.fr\/ krivine\/articles\/Ultrafiltre.pdf"},{"key":"10.2168\/LMCS-8(1:10)2012_krivine6","doi-asserted-by":"crossref","unstructured":"J.-L. Krivine.Realizability algebras : a program to well orderR.Logical Methods in Computer Science, vol. 7, 3:02, p. 1-47 (2011) http:\/\/hal.archives-ouvertes.fr\/hal-00483232 Updated version at : http:\/\/www.pps.jussieu.fr\/ krivine\/articles\/Wellorder.pdf","DOI":"10.2168\/LMCS-7(3:2)2011"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1072\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1072\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:02:57Z","timestamp":1681243377000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1072"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,27]]},"references-count":18,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:10)2012","relation":{"references":[{"id-type":"doi","id":"10.2307\/2267908","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1007.0825","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1007.0825","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,2,27]]},"article-number":"1072"}}