slideshow 3

Logic seminar

usually takes place each Monday at 13:30 temporarily on Zoom starting at 15:30, 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.

A lower bound for Polynomial Calculus with extension rule

Yaroslav Alekseev
Chebyshev Laboratory, St Petersburg State University
Monday, 16. November 2020 - 15:30 to 17:00
In this talk we consider an extension of the Polynomial Calculus proof system where we can introduce new variables and take a square root. We prove that an instance of the subset-sum principle, the binary value principle, requires refutations of exponential bit size over rationals in this system. Part and Tzameret proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations) refutations of the binary value principle. We show that our system p-simulates Res-Lin and thus we get an alternative exponential lower bound for the size of Res-Lin refutations of the binary value principle.

Iterated multiplication in VTC^0, Part 2

Emil Jeřábek
IM CAS
Monday, 2. November 2020 - 15:30 to 17:00
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

Iterated multiplication in VTC^0

Emil Jeřábek
IM CAS
Monday, 26. October 2020 - 15:30 to 17:00
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

Not all Kripke models of HA are locally PA

Erfan Khaniki
IM CAS
Monday, 12. October 2020 - 16:00 to 17:30
Let K be an arbitrary Kripke model of Heyting Arithmetic, HA. For every node k in K, we can view the classical structure of k, m_k, as a model of some classical theory of arithmetic. Let T be a classical theory in the language of arithmetic. We say K is locally T, iff for every k in K, m_k models T. A well-studied question in the model theory of HA is the following question: Is every Kripke model of HA locally PA? We answer this question negatively by constructing a Kripke model of HA which is not locally B\Sigma_1.

Pages