Realizability algebras: a program to well order R

DOI10.2168/LMCS-7(3:2)2011MaRDI QIDQ3224668zbMATH OpenFDO

Authors Jean-Louis Krivine

Publication date 2 April 2012

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

Full work available at URL https://doi.org/10.2168/LMCS-7(3:2)2011

zbMATH Keywords

axiom of choicecombinatory logicCurry-Howard correspondencelambda-calculus

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)

Recommendations

• Realizability algebras III: some examples
• scientific article; zbMATH DE number 5851813
• Realizability algebras. II: New models of \(\mathrm{ZF} + \mathrm{DC}\)
• On the structure of classical realizability models of ZF
• Typed realizability for first-order classical analysis

Cited in

(16)

• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Realizability models for a linear dependent PCF
• Realizability algebras. II: New models of \(\mathrm{ZF} + \mathrm{DC}\)
• 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
• On the structure of classical realizability models of ZF
• Constructive forcing, CPS translations and witness extraction in interactive realizability
• Classical realizability and arithmetical formulæ
• Stateful Realizers for Nonstandard Analysis
• A first-order completeness result about characteristic Boolean algebras in classical realizability
• Implicative models of set theory
• Realizability with stateful computations for nonstandard analysis

This page was built for publication: Realizability algebras: a program to well order \(\mathbb R\)

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