Iterated multiplication in VTC0

0559081 - MÚ 2023 RIV DE eng J - Článek v odborném periodiku
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
Grant CEP: GA ČR(CZ) GA19-05497S
Institucionální podpora: RVO:67985840
Klíčová slova: bounded arithmetic * integer division * iterated multiplication * modular powering
Obor OECD: Pure mathematics
Impakt faktor: 0.3, rok: 2022
Způsob publikování: Omezený přístup
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).
Trvalý link: https://hdl.handle.net/11104/0332500