On the computational content of the axiom of choice

DOI10.2307/2586854zbMath0914.03059OpenAlexW2107359728WikidataQ114004528 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

zbMATH Keywords

axiom of choiceintuitionistic arithmeticexcluded middlefunctional interpretation of classical analysishigher-order functionals

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55) Axiom of choice and related propositions (03E25)

Related Items

Dependent choice, `quote' and the clock ⋮ The effects of effects on constructivism ⋮ Limiting partial combinatory algebras ⋮ Realizability for Peano arithmetic with winning conditions in HON games ⋮ The equivalence of bar recursion and open recursion ⋮ The Peirce translation ⋮ A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory ⋮ Stateful Realizers for Nonstandard Analysis ⋮ Realizability algebras III: some examples ⋮ Constructive forcing, CPS translations and witness extraction in Interactive realizability ⋮ Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Selection functions, bar recursion and backward induction ⋮ Bar recursion over finite partial functions ⋮ Parameter-free polymorphic types ⋮ Programs from proofs using classical dependent choice ⋮ Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1 ⋮ Realizability interpretation of PA by iterated limiting PCA ⋮ Uniform Heyting arithmetic ⋮ A Coalgebraic View of Bar Recursion and Bar Induction ⋮ Operational domain theory and topology of sequential programming languages ⋮ Exercising Nuprl’s Open-Endedness ⋮ THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT ⋮ Unnamed Item ⋮ A generalization of Nash's theorem with higher-order functionals ⋮ Sequential games and optimal strategies ⋮ Unnamed Item ⋮ Minimum classical extensions of constructive theories

Cites Work

• Strong normalization of barrecursive terms without using infinite terms
• Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item