2013/02/13 by Michael Rathjen, Rathjen, Michael
Computer Science · Mathematics · Psychology · #Computability, Logic, AI Algorithms #Logic, Reasoning, and Knowledge #Philosophy and Theoretical Science #math.LO #msc:03B15 #msc:03C70 #msc:03E55 #msc:03F25 #msc:03F50
paper · pdf · doi:10.48550/arxiv.1302.3037
11 pages
arxiv created 2013/02/13 · arxiv updated 2013/02/14
In recent years the question of whether adding the limited principle of omniscience, LPO, to constructive Zermelo-Fraenkel set theory, CZF, increases its strength has arisen several times. As the addition of excluded middle for atomic formulae to CZF results in a rather strong theory, i.e. much stronger than classical Zermelo set theory, it is not obvious that its augmentation by LPO would be proof-theoretically benign. The purpose of this paper is to show that CZF +RDC+ LPO has indeed the same strength as CZF, where RDC stands for relativized dependent choice. In particular, these theories prove the same Pi-?0-2 theorems of arithmetic.