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.

Back to Sam Buss's publications page.