Iterated multiplication in $VT{C}^0$

Abstract

We show that $VT{C}^0$, the basic theory of bounded arithmetic corresponding to the complexity class ${\mathrm{TC}}^0$, proves the $IMUL$ axiom expressing the totality of iterated multiplication satisfying its recursive definition, by formalizing a suitable version of the ${\mathrm{TC}}^0$ iterated multiplication algorithm by Hesse, Allender, and Barrington. As a consequence, $VT{C}^0$ can also prove the integer division axiom, and (by our previous results) the RSUV-translation of induction and minimization for sharply bounded formulas. Similar consequences hold for the related theories ${\Delta }_1^b$-$CR$ and $C_2^0$. As a side result, we also prove that there is a well-behaved ${\Delta }_0$ definition of modular powering in $I{\Delta }_0+WPHP({\Delta }_0)$.

59 pages