• DocumentCode
    3260580
  • Title

    An arithmetical hierarchy of the law of excluded middle and related principles

  • Author

    Akama, Yohji ; Berardi, Stefano ; Hayashi, Susumu ; Kohlenbach, U.

  • Author_Institution
    Math. Inst., Tohoku Univ., Sendai, Japan
  • fYear
    2004
  • fDate
    13-17 July 2004
  • Firstpage
    192
  • Lastpage
    201
  • Abstract
    The topic of this paper is relative constructivism. We are concerned with classifying nonconstructive principles from the constructive viewpoint. We compare, up to provability in intuitionistic arithmetic, subclassical principles like Markov´s principle, (a function-free version of) weak Konig´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.
  • Keywords
    Markov processes; formal logic; theorem proving; Markov principle; Post theorem; bound extraction; classical proofs; excluded middle law; extended program extraction; intuitionistic arithmetic provability; relative constructivism; simply existential statements; simply universal statements; weak Konig lemma; Computer science; Logic;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium on
  • ISSN
    1043-6871
  • Print_ISBN
    0-7695-2192-4
  • Type

    conf

  • DOI
    10.1109/LICS.2004.1319613
  • Filename
    1319613