Root finding in TC^0 and open induction
Seminar Room 1, Newton Institute
AbstractIt is known that elementary arithmetic operations are computable in uniform TC^0, and some (multiplication, division) are even complete for this complexity class. The corresponding theory of bounded arithmetic, VTC^0, duly defines addition, multiplication, and ordering, and proves that integers form a discretely ordered ring under these operations. It is a natural question what other first-order properties of elementary arithmetic operations are provable in VTC^0. In particular, we are interested whether VTC^0 (or a theory of similar strength) can prove open induction in the basic language of arithmetic (Shepherdson's theory IOpen). This turns out equivalent to the problem whether there are TC^0 root-finding algorithms for constant-degree polynomials whose soundness is provable in VTC^0. In this talk, we will establish that such root-finding algorithms exist in the real (or rather, complex) world, and we will discuss the prospects of their formalization in bounded arithmetic.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.