Realizability algebras II : new models of ZF + DC

Jean-Louis Krivine

doi:10.2168/LMCS-8(1:10)2012

Jean-Louis Krivine - Realizability algebras II : new models of ZF + DC

lmcs:1072 - Logical Methods in Computer Science, February 27, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:10)2012

Realizability algebras II : new models of ZF + DCArticle

Authors: Jean-Louis Krivine

Using the proof-program (Curry-Howard) correspondence, we give a new method to obtain models of ZF and relative consistency results in set theory. We show the relative consistency of ZF + DC + there exists a sequence of subsets of R the cardinals of which are strictly decreasing + other similar properties of R. These results seem not to have been previously obtained by forcing.

https://doi.org/10.2168/LMCS-8(1:10)2012

Source: arXiv.org:1007.0825

Volume: Volume 8, Issue 1

Published on: February 27, 2012

Imported on: August 24, 2010

Keywords: Mathematics - Logic,Computer Science - Logic in Computer Science,F.4.1

Licence: arXiv.org - Non-exclusive license to distribute

Bibliographic References

14 Documents citing this article

Guillaume Geoffroy, arXiv (Cornell University), A first-order completeness result about characteristic Boolean algebras in classical realizability, 2022, Haifa Israel, 10.1145/3531130.3532484, https://arxiv.org/abs/2209.08838.

Liron Cohen;Etienne Miquey;Ross Tate, Evidenced Frames: A Unifying Framework Broadening Realizability Models, 2021, Rome, Italy, 10.1109/lics52264.2021.9470514, https://hal.inria.fr/hal-03422961.

Alexandre Miquel, 2020, Implicative algebras: a new foundation for realizability and forcing, arXiv (Cornell University), 30, 5, pp. 458-510, 10.1017/s0960129520000079, https://arxiv.org/abs/1802.00528.

Laura Fontanella;Guillaume Geoffroy, 2020, Preserving cardinals and weak forms of Zorn’s lemma in realizability models, Mathematical Structures in Computer Science, 30, 9, pp. 976-996, 10.1017/s0960129521000013.

ASAF KARAGILA, 2019, REALIZING REALIZABILITY RESULTS WITH CLASSICAL CONSTRUCTIONS, arXiv (Cornell University), 25, 4, pp. 429-445, 10.1017/bsl.2019.59, http://arxiv.org/abs/1905.08202.

Guillaume Geoffroy, Classical realizability as a classifier for nondeterminism, pp. 462-471, 2018, Oxford United Kingdom, 10.1145/3209108.3209140, https://hal.archives-ouvertes.fr/hal-01802215.

WALTER FERRER SANTOS;MAURICIO GUILLERMO;OCTAVIO MALHERBE, 2018, Realizability in ordered combinatory algebras with adjunction, Mathematical Structures in Computer Science, 29, 3, pp. 430-464, 10.1017/s0960129518000075.

Étienne Miquey, Formalizing Implicative Algebras in Coq, pp. 459-476, 2018, 10.1007/978-3-319-94821-8_27, https://hal.inria.fr/hal-01703524.

JEAN-LOUIS KRIVINE, 2016, Realizability algebras III: some examples, 28, 1, pp. 45-76, 10.1017/s0960129516000050, https://hal.archives-ouvertes.fr/hal-00743120.

Mauricio Guillermo;Étienne Miquey, 2016, Classical realizability and arithmetical formulæ, 27, 6, pp. 1068-1107, 10.1017/s0960129515000559, https://hal.inria.fr/hal-01247989.

Alberto Naibo;Mattia Petrolo;Thomas Seiller, Logic, argumentation & reasoning, Verificationism and Classical Realizability, pp. 163-197, 2015, 10.1007/978-3-319-20762-9_9.

Guillaume Munch-Maccagnoni, Formulae-as-types for an involutive negation, 27, pp. 1-10, 2014, Vienna Austria, 10.1145/2603088.2603156, https://hal.inria.fr/hal-00996742.

Federico Aschieri, 2013, Strong Normalization for HA + EM1 by Non-Deterministic Choice, arXiv (Cornell University), 127, pp. 1-14, 10.4204/eptcs.127.1.

Federico Aschieri;Margherita Zorzi, 2012, Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic, arXiv (Cornell University), 97, pp. 1-18, 10.4204/eptcs.97.1.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1571 times.

This article's PDF has been downloaded 456 times.