Proof-theoretic characterization of the primitive recursive functions?

464 Views Asked by At

The total recursive functions are exactly those number-theoretic functions that can be represented by a $\Sigma_1$ formula of first-order arithmetic.

Is there a similar characterization of the primitive recursive functions? I'm looking for something like for example

(wild conjecture) The primitive recursive functions are those that can be represented by a $\Sigma^0_1$ formula which can be proved total and single-valued by $\Delta^0_0$ induction.

1

There are 1 best solutions below

3
On BEST ANSWER

The provably total functions in $\mathrm I\Sigma_1$ are exactly the primitive recursive functions. This is a theorem of Parsons from the 1970s; see, for instance, Theorem 3 on page 34 of the book Proof Theory edited by Aczel, Simmons and Wainer for the standard proof.

The theory $\mathrm I\Delta_0$ in the usual language of arithmetic $\{0,1,{+},{\times},{<}\}$ is not sufficient to prove the totality of all primitive recursive functions. For example, it was shown by Parikh in his paper “Existence and feasibility in arithmetic” that the totality of exponentiation is not provable in $\mathrm I\Delta_0$.