Iterated multiplication in \(VTC^0\) (Q2155497)

The paper is devoted to feasible reasoning. It is shown that \(VTC^{0}\), the basic theory of bounded arithmetic corresponding to the complexity class TC\(^{0}\), proves the IMUL axiom expressing the totality of iterated multiplication satisfying its recursive definition, by formalizing a suitable version of the TC\(^{0}\) iterated multiplication algorithm by \textit{W. Hesse} et al. [J. Comput. Syst. Sci. 65, No. 4, 695--716 (2002; Zbl 1059.68044)]. As a consequence, \(VTC^{0}\) can also prove the integer division axiom, and (by our previous results) the RSUV-translation of induction and minimization for sharply bounded formulas. It is shown that similar consequences hold for the related theories \(\Delta^{b}_{1}-CR\) and \(C^{0}_{2}\). As a side result, it is proved that there is a well-behaved \(\Delta_{0}\) definition of modular powering in \(I \Delta_{0} + WPHP(\Delta_{0})\).