Constructive Zermelo-Fraenkel set theory and the limited principle of
omniscience
M. Rathjen. (2013)cite arxiv:1302.3037Comment: 11 pages.
Zusammenfassung
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.
Beschreibung
Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
%0 Generic
%1 rathjen2013constructive
%A Rathjen, Michael
%D 2013
%K constructive fraenkel set theory zermelo
%T Constructive Zermelo-Fraenkel set theory and the limited principle of
omniscience
%U http://arxiv.org/abs/1302.3037
%X 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.
@misc{rathjen2013constructive,
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
Pi-?0-2 theorems of arithmetic.},
added-at = {2013-12-23T04:23:24.000+0100},
author = {Rathjen, Michael},
biburl = {https://www.bibsonomy.org/bibtex/25f23786a07284a436aad9a08225a4c4e/aeu_research},
description = {Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience},
interhash = {3ebf737bfce1d42679b1f798e4ce9a6e},
intrahash = {5f23786a07284a436aad9a08225a4c4e},
keywords = {constructive fraenkel set theory zermelo},
note = {cite arxiv:1302.3037Comment: 11 pages},
timestamp = {2013-12-23T04:39:53.000+0100},
title = {Constructive Zermelo-Fraenkel set theory and the limited principle of
omniscience},
url = {http://arxiv.org/abs/1302.3037},
year = 2013
}