Journal of Symbolic Logic 63 (2):600-622 (1998)
|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)|
|Through your library||Configure|
Similar books and articles
G. Mints (1999). Cut-Elimination for Simple Type Theory with an Axiom of Choice. Journal of Symbolic Logic 64 (2):479-485.
Paul E. Howard, Arthur L. Rubin & Jean E. Rubin (1978). Independence Results for Class Forms of the Axiom of Choice. Journal of Symbolic Logic 43 (4):673-684.
Lorenz Halbeisen & Saharon Shelah (2001). Relations Between Some Cardinals in the Absence of the Axiom of Choice. Bulletin of Symbolic Logic 7 (2):237-261.
Paul E. Howard (1973). Limitations on the Fraenkel-Mostowski Method of Independence Proofs. Journal of Symbolic Logic 38 (3):416-422.
Vivian Charles Walsh (1967). On the Significance of Choice Sets with Incompatibilities. Philosophy of Science 34 (3):243-250.
Andrea Cantini (2003). The Axiom of Choice and Combinatory Logic. Journal of Symbolic Logic 68 (4):1091-1108.
Jeffry L. Hirst & Carl Mummert (2010). Reverse Mathematics and Uniformity in Proofs Without Excluded Middle. Notre Dame Journal of Formal Logic 52 (2):149-162.
Jeremy Avigad, The Computational Content of Classical Arithmetic to Appear in a Festschrift for Grigori Mints.
Paul Howard & Jean E. Rubin (1995). The Axiom of Choice for Well-Ordered Families and for Families of Well- Orderable Sets. Journal of Symbolic Logic 60 (4):1115-1117.
G. P. Monro (1983). On Generic Extensions Without the Axiom of Choice. Journal of Symbolic Logic 48 (1):39-52.
Added to index2009-01-28
Total downloads10 ( #114,297 of 722,745 )
Recent downloads (6 months)3 ( #25,873 of 722,745 )
How can I increase my downloads?