We study constructive set theories, which deal with 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 impredicative . (...) © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim. (shrink)

The purpose of this article is to present a new theory for fixed points over arithmetic which allows the building up of fixed points in a very nested and entangled way. But in spite of its great expressive power we can show that the proof-theoretic strength of our theory—which is intensional in a meaning to be described below—is characterized by the Feferman–Schütte ordinal Γ0. Our approach is similar to the building up of fixed points over state spaces in the propositional (...) modal μ-calculus. (shrink)