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
Link To Document :
بازگشت