Bounded arithmetic for NC, ALogTIME, L and NL

AbstractWe define theories of bounded arithmetic, whose definable functions and relations are exactly those in certain complexity classes. Based on a recursion-theoretic characterization of NC in Clote (1988, 1990), the first-order theory TNC, whose principal axiom scheme is a form of short induction on notation for nondeterministic polynomial-time computable relations, has the property that those functions having nondeterministic polynomial-time graph Θ(x, y) such that TNC ⊢∀x ∃y Θ(x, y) are exactly the functions in NC, computable on a parallel random-access machine in polylogarithmic parallel time with a polynomial number of processors.0 We then define three theories of weak second-order arithmetic which respectively characterize relations in the classes of alternating logarithmic time, logspace and nondeterministic logspace