Logic in Computer Science (LICS 2004)

Paper: An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles (at LICS 2004)

Authors: Yohji Akama Stefano Berardi Susumu Hayashi Ulrich Kohlenbach

Abstract

The topic of this paper is Relative Constructivism. We are concerned with classifying non-constructive principles from the constructive viewpoint. We compare, up to provability in Intuitionistic Arithmetic, sub-classical principles like Markov's Principle, (a function-free version of) Weak König's Lemma, Post's Theorem, Excluded Middle for simply Existential and simply Universal statements, and many others. Our motivations are rooted in the experience of one of the authors with an extended program extraction and of another author with bound extraction from classical proofs.

BibTeX

  @InProceedings{AkamaBerardiHayashi-AnArithmeticalHiera,
    author = 	 {Yohji Akama and Stefano Berardi and Susumu Hayashi and Ulrich Kohlenbach},
    title = 	 {An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {192--201},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }