[Proof Complexity] new paper

Moritz Müller moritz.mueller at univie.ac.at
Mon Oct 17 15:30:54 CEST 2016

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:


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

Of course, all comments are appreciated,



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.

More information about the Proof-Complexity mailing list