We study the extension of Feferman’s operational set theory provided by adding operational versions of unbounded existential quantification and power set and determine its proof-theoretic strength in terms of a suitable theory of sets and classes.

Jäger, G., Fixed points in Peano arithmetic with ordinals, Annals of Pure and Applied Logic 60 119-132. This paper deals with some proof-theoretic aspects of fixed point theories over Peano arithmetic with ordinals. It studies three such theories which differ in the principles which are available for induction on the natural numbers and ordinals. The main result states that there is a natural theory in this framework which is a conservative extension of Peano arithmeti.

The aim of this article is to give the proof-theoretic analysis of various subsystems of Feferman's theory T1 for explicit mathematics which contain the non-constructive μ-operator and join. We make use of standard proof-theoretic techniques such as cut-elimination of appropriate semiformal systems and asymmetrical interpretations in standard structures for explicit mathematics.