A classification of the set-theoretic total recursive functions of KPl

Abstract

The set theory KPl, which stands for Kripke-Platek-limit, roughly stipulates that there are unboundedly many admissible sets. Admissible sets are models of the Kripke-Platek set-theory KP which is a very weak fragment of ZFC. In [1], J. Cook and M. Rathjen classify the provably total set functions in KP using a proof system based on an ordinal notation system for the Bachmann-Howard ordinal relativized to a fixed set. In this paper, we adapt this result to the KPl set theory. We consider set functions which are provably total in KPl and Σ-definable by the same formula in any admissible set. We prove that, if f is such a function then, for any set x in the universe, the value f(x) always belongs to an initial segment of L(x), the constructible hierarchy relativized to the transitive closure of x, at a level below the relativized Takeuti-Feferman-Buchholz ordinal (the TFB ordinal is the prooftheoretic ordinal of KPl). To prove this result, we first construct an ordinal notation system based on [2] for KPl relativized to a fixed set that we will use in order to build a logic dependent on this fixed set where we will embed KPl. Thanks to this relativized system, we will be able to bound the value of the function at this fixed set.