**
A computational interpretation of open induction
**

*
Ulrich Berger
*

**Abstract**

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 A-translation, and therefore proves the same
Pi02-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 Pi02-formulas using open
induction. We also show that the computational interpretation of
classical countable choice given by Berardi, Bezem and
Coquand can be derived from our results.

**Bibtex entry**

@Inproceedings{Berger04, Author = "Ulrich Berger", Title = "A computational interpretation of open induction", Booktitle = "Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science", Editor = "F. Titsworth", Pages = "326--334, Publisher = "IEEE Computer Society", Year = 2004}