Recently, various restrictions of the primitive recursive set functions have been proposed with the aim to capture feasible computation on sets. Amongst these are the "Safe Recursive Set Functions" (Beckmann, Buss, Friedman, accepted for publication in JSL) the "Predicatively Computable Set Functions" (Arai, Archive for Mathematical Logic, vol. 54 (2015), pp. 471–485) and the "Cobham Recursive Set Functions" (Beckmann, Buss, Friedman, Müller, Thapen, in progress).
In this talk, I will identify "bounded" versions of Kripke-Platek set theory inspired by Buss' Bounded Arithmetic, which have the potential to capture some of the above classes as their Sigma-1-definable set functions. I will comment on adding definable symbols to these theories, along the lines of the first chapter of Barwise's book "Admissible Sets and Structures". The main part of my talk will be to sketch a proof that the Sigma-1 definable functions of some bounded Kripke-Platek set theory are exactly the Safe Recursive Set Functions.
CZ
