slideshow 3

Logic seminar

usually takes place each Monday at 13:30 temporarily on Zoom, normally in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.

Iterated multiplication in VTC^0

Emil Jeřábek
Monday, 26. October 2020 - 15:30 to 17:00

Zoom meeting 472 648 284 -
(contact for password)

Basic arithmetic operations +, -, *, / belong to the complexity class TC^0, and it is a natural question what can be proved about them in the corresponding theory of arithmetic VTC^0. It has been known that the theory VTC^0 + IMUL including an axiom expressing the totality of iterated multiplication \prod_{i=0}^n X_i proves quite a lot: it can formalize root finding for constant-degree polynomials, and as a consequence, it proves the RSUV-translation of IOpen, and more generally, of induction and minimization for sharply bounded formulas in Buss's language.

This left open the problem whether IMUL is itself provable in VTC^0, which effectively calls for the formalization of the TC^0 iterated multiplication algorithm due to Hesse, Allender, and Barrington.

Even though the analysis of the HAB algorithm is in principle fairly elementary, it has some peculiar features that make its formalization quite challenging: in particular, it suffers from serious "chicken or... more