This article provides an ordinal analysis of Σ11 transfinite dependent choice.

In this paper it is shown that the intuitionistic .xed point theory equation image for α times iterated fixed points of strictly positive operator forms is conservative for negative arithmetic and equation image sentences over the theory equation image for α times iterated arithmetic comprehension without set parameters.This generalizes results previously due to Buchholz [5] and Arai [2].

In this paper we introduce theories of universes in analysis. We discuss a non-uniform, a uniform and a minimal variant. An analysis of the proof-theoretic bounds of these systems is given, using only methods of predicative proof-theory. It turns out that all introduced theories are of proof-theoretic strength between Γ0 and ϕ1ɛ00.

In this paper we present some metapredicative subsystems of analysis. We deal with reflection principles, $\omega-model$ existence axioms (limit axioms) and axioms asserting the existence of hierarchies. We show several equivalences among the introduced subsystems. In particular we prove the equivalence of $\sum_1^1$ transfinite dependent choice and $\prod_2^1$ reflection on $\omega-models$ of $\sum_1^1-DC$.