Preprint:
Arnold Beckmann, Sam Buss, Sy-David Friedman,
Moritz Müller, and Neil Thapen
"Cobham Recursive Set Functions and Weak Set Theories"
In Sets and Computations,
Lecture Notes Series 33,
Institute for Mathematical Sciences,
National University of Singapore,
Edited by S.D. Friedman, D. Raghavan, Y. Yang,
World Scientific, 2018, pages 55-116.
Download
preprint.
Abstract: The Cobham recursive set functions (CRSF) provide a notion of polynomial time computation over general sets. In this paper, we determine a subtheory KPU1 of Kripke-Platek set theory whose Σ1-definable functions are precisely CRSF. The theory KPU1 is based on the ∈-induction scheme for Σ1-formulas whose leading existential quantifier satisfies certain boundedness and uniqueness conditions. Dropping the uniqueness condition and adding the axiom of global choice results in a theory KPC≤1 whose Σ1-definable functions are CRSFC, that is, CRSF relative to a global choice function C. We further show that the addition of global choice is conservative over certain local choice principles.