Realizability algebras II : new models of ZF + DC

Abstract

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.

28 p

References in corpus (2)

• Realizability algebras: a program to well order R
• Structures de réalisabilité, RAM et ultrafiltre sur N

Cited by in corpus (15)

• Delimited control operators prove Double-negation Shift
• Realizability algebras III: some examples
• Implicative algebras: a new foundation for realizability and forcing
• Classical realizability as a classifier for nondeterminism
• Strong Normalization for HA + EM1 by Non-Deterministic Choice
• On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic
• Realizing realizability results with classical constructions
• Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic
• A program for the full axiom of choice
• Quantitative classical realizability
• Realizability Toposes from Specifications
• A first-order completeness result about characteristic Boolean algebras in classical realizability
• Revisiting the duality of computation: an algebraic analysis of classical realizability models
• A constructive proof of dependent choice in classical arithmetic via memoization
• Implicative models of set theory