Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6424796 | Annals of Pure and Applied Logic | 2014 | 10 Pages |
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
Michael Rathjen,