Iterated multiplication in VTC0

0559081 - MÚ 2023 RIV DE eng J - Journal Article
Jeřábek, Emil
Iterated multiplication in VTC0.
Archive for Mathematical Logic. Roč. 61, 5-6 (2022), s. 705-767. ISSN 0933-5846. E-ISSN 1432-0665
R&D Projects: GA ČR(CZ) GA19-05497S
Institutional support: RVO:67985840
Keywords : bounded arithmetic * integer division * iterated multiplication * modular powering
OECD category: Pure mathematics
Impact factor: 0.3, year: 2022
Method of publishing: Limited access
https://doi.org/10.1007/s00153-021-00810-6

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 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 IDelta_0+WPHP(Delta_0).
Permanent Link: https://hdl.handle.net/11104/0332500