Iterating Σ Operations in Admissible Set Theory without Foundation: A Further Aspect of Metapredicative Mahlo
Gerhard Jäger, Dieter Probst · 2004
In this article we study the theory KPi 0 + (Σ-TR) which (i) describes a recursively inaccessible universe, (ii) permits the iteration of Σ operations along the ordinals, (iii) does not comprise ∈ induction, and (iv) restricts complete induction on the natural numbers to sets. It is shown that the proof-theoretic ordinal of KPi 0 + (Σ-TR) is the metapredicative Mahlo ordinal ϕω00. Our system KPi 0 + (Σ-TR) is closely related to the system of second order arithmetic for Σ 1 1 transfinite dependent choice introduced in Rüede [8].