A computational interpretation of open induction
Ulrich Berger

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

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}

Draft copy