Article ID Journal Published Year Pages File Type
6424796 Annals of Pure and Applied Logic 2014 10 Pages PDF
Abstract

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 Π20 theorems of arithmetic.

Related Topics
Physical Sciences and Engineering Mathematics Logic
Authors
,