Research article:
Samuel R. Buss.
"The witness function method and provably recursive functions of
Peano arithmetic."
In Proceedings of Ninth International Congress on
Logic, Methodology and Philosophy of Science, D. Prawitz, B. Skyrms and D.
Westerstahl (eds), Elsevier Science North-Holland, 1994, pp. 29-68.
Download article: postscript or PDF.
Abstract: This paper presents a new proof of the
characterization of the provably recursive functions of the fragments $I\Sigma_n$ of Peano
arithmetic. The proof method also characterizes the $\Sigma_k$-definable functions
of~$I\Sigma_n$ and of theories axiomatized by transfinite induction on ordinals. The
proofs are completely proof-theoretic and use the method of witness functions and witness
oracles.
Similar methods also yield a new proof of Parson's theorem on the
conservativity of the $\Sigma_{n+1}$-induction rule over the $\Sigma_n$-induction axioms.
A new proof of the conservativity of $B\Sigma_{n+1}$ over $I\Sigma_n$ is given.
The proof methods provide new analogies between Peano arithmetic and
bounded arithmetic.