This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories $\widehat{ID}_\alpha and \widehat{ID}_{ the exact proof-theoretic ordinals of these systems are presented.

This paper deals with the proof theory of first-order applicative theories with non-constructive μ operator and a form of the bar rule, yielding systems of ordinal strength Γ0 and 20, respectively. Relevant use is made of fixed-point theories with ordinals plus bar rule.

In this paper, we study a concept of universe for a truth predicate over applicative theories. A proof-theoretic analysis is given by use of transfinitely iterated fixed point theories . The lower bound is obtained by a syntactical interpretation of these theories. Thus, universes over Frege structures represent a syntactically expressive framework of metapredicative theories in the context of applicative theories.