Full operational set theory with unbounded existential quantification and power set (Q1024551)

From the introduction: ``This paper is a direct sequel of [\textit{G. Jäger}, Ann. Pure Appl. Logic 150, No. 1--3, 19--39 (2007; Zbl 1136.03038)] and answers the question about the exact consistency-theoretic strength of Feferman's operational set theory [\textit{S. Feferman}, ``Notes on operational set theory. I. Generalization of ``small'' large cardinals in classical and admissible set theory'' (2001), available at \url{http://math.stanford.edu/~feferman/papers/OperationalST-I.pdf}] extended by operational versions of unbounded existential quantification and power set. We show that this system, called \(\mathsf{OST}(\mathbf{E},\mathbb{P})\), is equiconsistent with a natural theory of sets and classes, \(\mathsf{NBG}_{<E_0}\), which is obtained from usual von Neumann-Bernays-Gödel theory \(\mathsf{NBG}\) by adding \({\in}\)-induction for arbitrary formulas and a specific form of iteration of elementary class comprehension.''