Abstract

In this article we define a new and transparent concept of total collapsing functions for an ordinal notation system which is characteristic for the theory (Δ 2 1 -CA)+(BI). We show that our construction allows the application of Pohler's method of local predicativity as presented in [2] which yields a perspicious proof-theoretic analysis of (Δ 2 1 -CA)+(BI) being not much more complicated than for ID1