First Order Bounded Arithmetic and Small Boolean Circuit Complexity Classes
Peter Clote, Gaisi Takeuti · Birkhäuser Boston eBooks · 1995
A well known result of proof theory is the characterization of primitive recursive functions ƒ as those provably recursive in the first order theory of Peano arithmetic with the induction axiom restricted to Σ 1 formulas. In this paper, we study a variety of weak theories of first order arithmetic, whose provably total functions (with graphs of a certain form) are exactly those computable within some resource bound on a particular computation model (boolean circuits, with possible parity or MOD 6 gates, or threshold circuits, or alternating Turing machines, or ordinary Turing machines). To establish these kinds of results for small complexity classes, we provide a recursion-theoretic characterization of the complexity class, prove how one can encode sequences in very weak theories, and use the witnessing technique of [7].