On the computational content of the axiom of choice

Journal of Symbolic Logic 63 (2):600-622 (1998)
  Copy   BIBTEX


We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Godel's Dialectica interpretation



    Upload a copy of this work     Papers currently archived: 91,349

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

104 (#164,656)

6 months
25 (#111,330)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Stefano Berardi
Università degli Studi di Torino

Citations of this work

Uniform heyting arithmetic.Ulrich Berger - 2005 - Annals of Pure and Applied Logic 133 (1):125-148.
The equivalence of bar recursion and open recursion.Thomas Powell - 2014 - Annals of Pure and Applied Logic 165 (11):1727-1754.
The Peirce Translation.Martín Escardó & Paulo Oliva - 2012 - Annals of Pure and Applied Logic 163 (6):681-692.
Realizability for Peano arithmetic with winning conditions in HON games.Valentin Blot - 2017 - Annals of Pure and Applied Logic 168 (2):254-277.
Programs from proofs using classical dependent choice.Monika Seisenberger - 2008 - Annals of Pure and Applied Logic 153 (1-3):97-110.

View all 9 citations / Add more citations

References found in this work

Foundations of Constructive Analysis.John Myhill - 1972 - Journal of Symbolic Logic 37 (4):744-747.
Passion and Value in Hume's Treatise.D. G. C. Macnabb - 1968 - Philosophical Books 9 (1):2-4.
Mathematical Logic.Georg Kreisel - 1965 - In Lectures on Modern Mathematics. New York: Wiley. pp. 95-195.
Mathematical Logic.Donald Monk - 1975 - Journal of Symbolic Logic 40 (2):234-236.

Add more references