Logic in Computer Science (LICS 2004)

Paper: A Computational Interpretation of Open Induction (at LICS 2004)

Authors: 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 -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.

BibTeX

  @InProceedings{Berger-AComputationalInter,
    author = 	 {Ulrich Berger},
    title = 	 {A Computational Interpretation of Open Induction},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {326--334},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }