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.

Comment: 28 p

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

Source: arXiv.org:1007.0825

Volume: Volume 8, Issue 1

Secondary volumes: Selected Papers of the 9th Conference on Typed Lambda Calculi and Applications (TLCA 2009)

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

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

14 Documents citing this article

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

Liron Cohen;Etienne Miquey;Ross Tate, 2021, Evidenced Frames: A Unifying Framework Broadening Realizability Models, pp. 1-13, 10.1109/lics52264.2021.9470514, https://inria.hal.science/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, http://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, UEA Digital Repository (University of East Anglia), 25, 4, pp. 429-445, 10.1017/bsl.2019.59.

Guillaume Geoffroy, 2018, Classical realizability as a classifier for nondeterminism, arXiv (Cornell University), pp. 462-471, 10.1145/3209108.3209140, http://arxiv.org/abs/1805.11392.

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, 2018, Formalizing Implicative Algebras in Coq, pp. 459-476, 10.1007/978-3-319-94821-8_27, https://inria.hal.science/hal-01703524.

JEAN-LOUIS KRIVINE, 2016, Realizability algebras III: some examples, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 28, 1, pp. 45-76, 10.1017/s0960129516000050, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.146.

MAURICIO GUILLERMO;ÉTIENNE MIQUEY, 2016, Classical realizability and arithmetical formulæ, 27, 6, pp. 1068-1107, 10.1017/s0960129515000559, https://inria.hal.science/hal-01247989.

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

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

Federico Aschieri, 2013, Strong Normalization for HA + EM1 by Non-Deterministic Choice, Electronic Proceedings in Theoretical Computer Science, 127, pp. 1-14, 10.4204/eptcs.127.1, https://doi.org/10.4204/eptcs.127.1.

Federico Aschieri;Margherita Zorzi, 2012, Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic, Electronic Proceedings in Theoretical Computer Science, 97, pp. 1-18, 10.4204/eptcs.97.1, https://doi.org/10.4204/eptcs.97.1.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3313 times.

This article's PDF has been downloaded 653 times.