Аннотация
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.
Пользователи данного ресурса
Пожалуйста,
войдите в систему, чтобы принять участие в дискуссии (добавить собственные рецензию, или комментарий)