The paper relativizes the method of ordinal analysis developed for Kripke–Platek set theory to theories which have the power set axiom. We show that it is possible to use this technique to extract information about Power Kripke–Platek set theory, KP.As an application it is shown that whenever KP+AC proves a ΠP2 statement then it holds true in the segment Vτ of the von Neumann hierarchy, where τ stands for the Bachmann–Howard ordinal.

In this paper we introduce a notation system for the infinitary derivations occurring in the ordinal analysis of KP + Π₃-Reflection due to Michael Rathjen. This allows a finitary ordinal analysis of KP + Π₃-Reflection. The method used is an extension of techniques developed by Wilfried Buchholz, namely operator controlled notation systems for RS∞-derivations. Similarly to Buchholz we obtain a characterisation of the provably recursive functions of KP + Π₃-Reflection as <-recursive functions where < is the ordering on Rathjen's ordinal (...) notation system J(K). Further we show a conservation result for $\Pi _{2}^{0}$-sentences. (shrink)

In this paper we formulate epsilon substitution method for a theory $\Pi _{2}^{0}$-FIX for non-monotonic $\Pi _{2}^{0}$ inductive definitions. Then we give a termination proof of the H-processes based on Ackermann [1].

We show that the existence of a weakly compact cardinal over the Zermelo–Fraenkel's set theory ZF is proof-theoretically reducible to iterations of Mostowski collapsings and Mahlo operations.

The technique of using infinitary rules in an ordinal analysis has been one of the most productive developments in ordinal analysis. Unfortunately, one of the most advanced variants, the Buchholz Ωμ rule, does not apply to systems much stronger than -comprehension. In this paper, we propose a new extension of the Ω rule using game-theoretic quantifiers. We apply this to a system of inductive definitions with at least the strength of a recursively inaccessible ordinal.

The \-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory \ using a variant of the cut-elimination formalism introduced by Mints.