On the computational content of the axiom of choice

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

Authors
Stefano Berardi
Università degli Studi di Torino
Abstract
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
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2586854
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 40,736
Through your library

References found in this work BETA

Foundations of Constructive Analysis.Errett Bishop, A. Kino, J. Myhill & R. E. Vesley - 1972 - Journal of Symbolic Logic 37 (4):744-747.
From Frege to Gödel.[author unknown] - 1968 - Philosophical Books 9 (1):31-32.
Mathematical Logic.Joseph R. Shoenfield - 1975 - Journal of Symbolic Logic 40 (2):234-236.

Add more references

Citations of this work BETA

The Equivalence of Bar Recursion and Open Recursion.Thomas Powell - 2014 - Annals of Pure and Applied Logic 165 (11):1727-1754.
Realizability for Peano Arithmetic with Winning Conditions in HON Games.Valentin Blot - 2017 - Annals of Pure and Applied Logic 168 (2):254-277.
The Peirce Translation.Martín Escardó & Paulo Oliva - 2012 - Annals of Pure and Applied Logic 163 (6):681-692.
Uniform Heyting Arithmetic.Ulrich Berger - 2005 - Annals of Pure and Applied Logic 133 (1):125-148.
Programs From Proofs Using Classical Dependent Choice.Monika Seisenberger - 2008 - Annals of Pure and Applied Logic 153 (1-3):97-110.

View all 8 citations / Add more citations

Similar books and articles

Analytics

Added to PP index
2009-01-28

Total views
44 ( #179,248 of 2,243,784 )

Recent downloads (6 months)
12 ( #87,176 of 2,243,784 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature