On the computational content of the axiom of choice
From MaRDI portal
Publication:4212925
DOI10.2307/2586854zbMath0914.03059WikidataQ114004528 ScholiaQ114004528MaRDI QIDQ4212925
Thierry Coquand, Stefano Berardi, Marc Bezem
Publication date: 21 June 1999
Published in: The Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: http://doc.rero.ch/record/293640/files/S0022481200015127.pdf
axiom of choice; intuitionistic arithmetic; excluded middle; functional interpretation of classical analysis; higher-order functionals
03F50: Metamathematics of constructive systems
03F55: Intuitionistic mathematics
03E25: Axiom of choice and related propositions
Related Items
Realizability algebras III: some examples, Validating Brouwer's continuity principle for numbers using named exceptions, THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT, Unnamed Item, Unnamed Item, Constructive forcing, CPS translations and witness extraction in Interactive realizability, Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1, Realizability interpretation of PA by iterated limiting PCA, Stateful Realizers for Nonstandard Analysis, Realizability for Peano arithmetic with winning conditions in HON games, The equivalence of bar recursion and open recursion, The Peirce translation, Bar recursion over finite partial functions, Parameter-free polymorphic types, Operational domain theory and topology of sequential programming languages, Uniform Heyting arithmetic, Dependent choice, `quote' and the clock, Limiting partial combinatory algebras, Minimum classical extensions of constructive theories, The effects of effects on constructivism, Programs from proofs using classical dependent choice, A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory, A Coalgebraic View of Bar Recursion and Bar Induction, Exercising Nuprl’s Open-Endedness, A generalization of Nash's theorem with higher-order functionals, Sequential games and optimal strategies, Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs, Selection functions, bar recursion and backward induction
Cites Work
