caa a22 4500 388039469 CHVBK 20180307125017.0 cr unu---uuuuu 161130e199806 xx s 000 0 eng 10.2307/2586854 doi S0022481200015127 pii (NATIONALLICENCE)cambridge-10.2307/2586854 On the computational content of the axiom of choice [Elektronische Daten] 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 Gödel's Dialectica interpretation. Copyright © Association for Symbolic Logic 1998 Berardi Stefano Torino University, Dip. Informatica, C. So Svizzera 185, 10149 Torino, Italy, E-mail: stefano@di.unito.it Bezem Marc Utrecht University, Department of Philosophy, P.O. Box 80126, 3508 TC Utrecht, The Netherlands, E-mail: bezem@phil.ruu.nl Coquand Thierry Chalmers University of Gothenburg, Department of Computer Sciences, S-41296, Gothenburg, Sweden, E-mail: coquand@cs.chalmers.se The Journal of Symbolic Logic Cambridge University Press 63/2(1998-06), 600-622 0022-4812 63:2<600 1998 63 JSL https://doi.org/10.2307/2586854 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.2307/2586854 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Berardi Stefano Torino University, Dip. Informatica, C. So Svizzera 185, 10149 Torino, Italy, E-mail: stefano@di.unito.it NATIONALLICENCE 700 1- Bezem Marc Utrecht University, Department of Philosophy, P.O. Box 80126, 3508 TC Utrecht, The Netherlands, E-mail: bezem@phil.ruu.nl NATIONALLICENCE 700 1- Coquand Thierry Chalmers University of Gothenburg, Department of Computer Sciences, S-41296, Gothenburg, Sweden, E-mail: coquand@cs.chalmers.se NATIONALLICENCE 773 0- The Journal of Symbolic Logic Cambridge University Press 63/2(1998-06), 600-622 0022-4812 63:2<600 1998 63 JSL CC0 http://creativecommons.org/publicdomain/zero/1.0 nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-cambridge