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.

We formulate epsilon substitution method for a theory [Π0 1, Π0 1]-FIX for two steps non-monotonic Π0 1 inductive definitions. Then we give a termination proof of the H-processes based on Ackermann [1].

In Arai (An ordinal analysis of a single stable ordinal, submitted) it is shown that an ordinal \(\sup _{N is an upper bound for the proof-theoretic ordinal of a set theory \(\mathsf {KP}\ell ^{r}+(M\prec _{\Sigma _{1}}V)\). In this paper we show that a second order arithmetic \(\Sigma ^{1-}_{2}{\mathrm {-CA}}+\Pi ^{1}_{1}{\mathrm {-CA}}_{0}\) proves the wellfoundedness up to \(\psi _{\varOmega _{1}}(\varepsilon _{\varOmega _{{\mathbb {S}}+N+1}})\) for each _N_. It is easy to interpret \(\Sigma ^{1-}_{2}{\mathrm {-CA}}+\Pi ^{1}_{1}{\mathrm {-CA}}_{0}\) in \(\mathsf {KP}\ell ^{r}+(M\prec _{\Sigma _{1}}V)\).