loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)
A Computational Interpretation of Open Induction
Turku, Finland
July 13-July 17
ISBN: 0-7695-2192-4
Ulrich Berger, University of Wales Swansea, UK
We study the proof-theoretic and computational properties of open induction, a principle which is classically equivalent to Nash-Williams' minimal-bad-sequence argument and also to (countable) dependent choice (and hence contains full classical analysis). We show that, intuitionistically, open induction and dependent choice are quite different: Unlike dependent choice, open induction is closed under negative- and -translation, and therefore proves the same II_2^0-formulas (over not necessarily decidable, basic predicates) with classical or intuitionistic arithmetic. Via modified realizability we obtain a new direct method for extracting programs from classical proofs of II_2^0-formulas using open induction. We also show that the computational interpretation of classical countable choice given by Berardi, Bezen and Coquand [On the computational content of the axiom of choice] can be derived from our results.
Citation:
Ulrich Berger, "A Computational Interpretation of Open Induction," lics, pp.326, 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.