[Proof Complexity] new paper

[Moritz Müller]

Dear all,

a new paper titled "Cobham recursive set functions and weak set 
theories" by A. Beckmann, S. Buss, S.-D. Friedman, N. Thapen and myself 
is available here:

http://www.logic.univie.ac.at/~muellem3/publications.html

Please find an (email friendly version of) the abstract below.

Of course, all comments are appreciated,

Moritz


Abstract:

The Cobham recursive set functions (CRSF) provide a notion of polynomial 
time computation over general sets. In this paper, we determine a 
subtheory of Kripke-Platek set theory whose Sigma_1-definable functions 
are precisely CRSF. This theory is based on the epsilon-induction scheme 
for Sigma_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 
whose Sigma_1-definable functions are CRSF relative to a global choice 
function. We further show that the addition of global choice is 
conservative over certain local choice principles.