{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:50:38Z","timestamp":1773096638088,"version":"3.50.1"},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":5763,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1998,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 <jats:italic>not<\/jats:italic> interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of \u2203-statements and how to extract algorithms from proofs of \u2200\u2203-statements. Our interpretation seems computationally more direct than the one based on G\u00f6del's Dialectica interpretation.<\/jats:p>","DOI":"10.2307\/2586854","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:01:17Z","timestamp":1146938477000},"page":"600-622","source":"Crossref","is-referenced-by-count":57,"title":["On the computational content of the axiom of choice"],"prefix":"10.1017","volume":"63","author":[{"given":"Stefano","family":"Berardi","sequence":"first","affiliation":[]},{"given":"Marc","family":"Bezem","sequence":"additional","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200015127_ref015","first-page":"95","volume-title":"Lectures on modern mathematics","volume":"III","author":"Kreisel","year":"1965"},{"key":"S0022481200015127_ref011","first-page":"325","volume":"31","author":"Howard","year":"1966","journal-title":"Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis"},{"key":"S0022481200015127_ref024","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70853-X"},{"key":"S0022481200015127_ref014","first-page":"139","volume":"27","author":"Kreisel","year":"1962","journal-title":"On weak completeness of intuitionistic predicate logic"},{"key":"S0022481200015127_ref013","first-page":"465","volume-title":"From Frege to G\u00f6del","author":"Kolmogorov","year":"1971"},{"key":"S0022481200015127_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-9478-5"},{"key":"S0022481200015127_ref007","unstructured":"Goodman, N. , Intuitionistic arithmetic as a theory of constructions, Ph.D. thesis , Stanford University, 1968."},{"key":"S0022481200015127_ref019","volume-title":"Systems that learn: An introduction to learning theory for cognitive and computer scientists","author":"Osherbon","year":"1986"},{"key":"S0022481200015127_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/BF01448445"},{"key":"S0022481200015127_ref025","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80021-9"},{"key":"S0022481200015127_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BF02007566"},{"key":"S0022481200015127_ref006","volume-title":"Collected work","volume":"II","author":"G\u00f6del","year":"1986"},{"key":"S0022481200015127_ref012","first-page":"109","volume":"10","author":"Kleene","year":"1945","journal-title":"On the interpretation of intuitionistic number theory"},{"key":"S0022481200015127_ref017","unstructured":"Murthy, C. , Extracting constructive content from classical proofs, Ph.D. thesis , Cornell University, 1990."},{"key":"S0022481200015127_ref027","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(77)90060-9"},{"key":"S0022481200015127_ref018","first-page":"230","article-title":"On the consistency of certain logical calculi","volume":"12","author":"Novikoff","year":"1943","journal-title":"Matematiceskij sbornik (Recueil Math\u00e9matique)"},{"key":"S0022481200015127_ref003","volume-title":"Foundations of constructive analysis","author":"Bishop","year":"1967"},{"key":"S0022481200015127_ref022","first-page":"1","volume-title":"Recursive function theory","author":"Spector","year":"1961"},{"key":"S0022481200015127_ref026","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S0022481200015127_ref021","volume-title":"Mathematical logic","author":"Shoenfield","year":"1967"},{"key":"S0022481200015127_ref004","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.014"},{"key":"S0022481200015127_ref020","doi-asserted-by":"publisher","DOI":"10.4064\/cm-6-1-165-170"},{"key":"S0022481200015127_ref009","first-page":"465","volume-title":"From Frege to G\u00f6del","author":"Hilbert","year":"1971"},{"key":"S0022481200015127_ref023","first-page":"204","volume-title":"Lecture notes in mathematics","author":"Tait","year":"1968"},{"key":"S0022481200015127_ref005","first-page":"325","volume":"60","author":"Coquand","year":"1995","journal-title":"A semantics of evidence for classical arithmetic"},{"key":"S0022481200015127_ref010","first-page":"107","article-title":"Functional interpretation of bar induction by bar recursion","volume":"20","author":"Howard","year":"1968","journal-title":"Compositio Mathematica"},{"key":"S0022481200015127_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/BF01449946"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200015127","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,10]],"date-time":"2021-08-10T12:15:59Z","timestamp":1628597759000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200015127\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,6]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,6]]}},"alternative-id":["S0022481200015127"],"URL":"https:\/\/doi.org\/10.2307\/2586854","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,6]]}}}