Realizability algebras. II: New models of ZF + DC

DOI10.2168/LMCS-8(1:10)2012MaRDI QIDQ2881077zbMATH OpenFDO

Authors Jean-Louis Krivine

Publication date 3 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.0825

zbMATH Keywords

axiom of choicecombinatory logicCurry-Howard correspondencelambda-calculusrelative consistencyset theory

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Axiom of choice and related propositions (03E25) Consistency and independence results (03E35)

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.

Recommendations

• Realizability algebras III: some examples
• On the structure of classical realizability models of ZF
• Realizability algebras: a program to well order \(\mathbb R\)
• Theory and Applications of Models of Computation
• Lifschitz realizability as a topological construction

Cited in

(15)

• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Realizability algebras: a program to well order \(\mathbb R\)
• Verificationism and Classical Realizability
• Delimited control operators prove double-negation shift
• Realizability algebras III: some examples
• A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
• Preserving cardinals and weak forms of Zorn’s lemma in realizability models
• Implicative algebras: a new foundation for realizability and forcing
• A program for the full axiom of choice
• REALIZING REALIZABILITY RESULTS WITH CLASSICAL CONSTRUCTIONS
• On the structure of classical realizability models of ZF
• Classical realizability and arithmetical formulæ
• A first-order completeness result about characteristic Boolean algebras in classical realizability
• Implicative models of set theory
• Realizability models for large cardinals

This page was built for publication: Realizability algebras. II: New models of \(\mathrm{ZF} + \mathrm{DC}\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2881077)