Extending constructive operational set theory by impredicative principles

We study constructive set theories, which deal with (partial) operations applying both to sets and operations themselves. Our starting point is a fully explicit, finitely axiomatized system ESTE of constructive sets and operations, which was shown in [10] to be as strong as PA. In this paper we consider extensions with operations, which internally represent description operators, unbounded set quantifiers and local fixed point operators. We investigate the proof theoretic strength of the resulting systems, which turn out to be (except for the description operator) impredicative (being comparable with full second-order arithmetic and the second-order mu-calculus over arithmetic). (C) 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim