Realizability algebras II : new models of ZF + DC

DOI10.2168/LMCS-8(1:10)2012zbMath1239.03009arXiv1007.0825MaRDI QIDQ2881077

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

set theoryaxiom of choicelambda-calculusCurry-Howard correspondencecombinatory logicrelative consistency

Mathematics Subject Classification ID

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

Related Items (10)

Realizability algebras III: some examples ⋮ Classical realizability and arithmetical formulæ ⋮ Delimited control operators prove double-negation shift ⋮ Implicative algebras: a new foundation for realizability and forcing ⋮ A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Verificationism and Classical Realizability ⋮ REALIZING REALIZABILITY RESULTS WITH CLASSICAL CONSTRUCTIONS ⋮ Preserving cardinals and weak forms of Zorn’s lemma in realizability models ⋮ Unnamed Item

This page was built for publication: Realizability algebras II : new models of ZF + DC