Open induction in a bounded arithmetic for TC^0

Abstract

The elementary arithmetic operations $+,\cdot ,\le$ on integers are well-known to be computable in the weak complexity class ${\mathrm{TC}}^0$, and it is a basic question what properties of these operations can be proved using only ${\mathrm{TC}}^0$-computable objects, i.e., in a theory of bounded arithmetic corresponding to ${\mathrm{TC}}^0$. We will show that the theory ${VTC}^0$ extended with an axiom postulating the totality of iterated multiplication (which is computable in ${\mathrm{TC}}^0$) proves induction for quantifier-free formulas in the language $⟨+,\cdot ,\le ⟩$ (IOpen), and more generally, minimization for ${\Sigma }_0^b$ formulas in the language of Buss's $S_2$.

35 pages

Cited by in corpus (2)

• Elementary analytic functions in $VT{C}^0$
• Models of $VT{C}^0$ as exponential integer parts