The following is part of a series of papers on theories for (iterated) admissible sets (cf. [10], [11], [12], [14], [15]). Although these theories are weak subsystems of Zermelo-Fraenkel set theory, they allow one to formalize and prove a fair amount of definability theory and generalized recursion theory. Using this machinery it is in general not very hard to establish the connections between theories for admissible sets and (for example) systems of second order arithmetic. A proof-theoretic analysis of theories for admissible sets therefore provides quite a uniform and powerful framework for the proof-theoretic treatment of many systems of set theory, second order arithmetic and constructive mathematics (see [12] and [15]). The strongest result in this direction so far is the pair of proof-theoretic equivalenceswhere T0 is Feferman's system for explicit mathematics of [5] and [6], (-CA) + (BI) is the usual system of second order arithmetic with the axiom of -comprehension and bar induction and KPi is Kripke-Platek set theory with ∈-inductionfor arbitrary formulas and the additional axiom.The least standard model of KPi is L(i0) where i0 is the first recursively inaccessible ordinal.In this paper we are mainly interested in the theory KPi0 which results from KPi by severely restricting the principles of induction. Basically, complete induction on the natural numbersis allowed only for ∆0-formulas, and (IND∈) is omitted completely.
ω-models of second order arithmetic and admissible sets