[Proof Complexity] new paper

[Emil Jerabek]

Dear colleagues,

A new preprint "Iterated multiplication in VTC^0" is available on my
web page https://math.cas.cz/~jerabek/ . Comments, corrections, and
suggestions are welcome.

Best regards,
Emil Jerabek

Abstract:
We show 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 Hesse, Allender, and Barrington.
As a consequence, VTC^0 can also prove the integer division axiom, and
(by results of Jerabek) the RSUV-translation of induction and
minimization for sharply bounded formulas. Similar consequences hold
for the related theories \Delta^b_1-CR and C^0_2.

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).