Open induction in a bounded arithmetic for TC^0

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