Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience

TL;DR

This paper demonstrates that adding the limited principle of omniscience (LPO) to constructive Zermelo-Fraenkel set theory with relativized dependent choice (CZF + RDC) does not increase its proof-theoretic strength, maintaining equivalence with CZF.

Contribution

It proves that CZF + RDC + LPO has the same strength as CZF, showing LPO's addition is proof-theoretically benign.

Findings

CZF + RDC + LPO and CZF prove the same Pi-?0-2 theorems of arithmetic.

Adding LPO does not increase the proof-theoretic strength of CZF.

Theories with LPO remain proof-theoretically equivalent to CZF.

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.