slideshow 3

Logic seminar

usually takes place each Monday at 16:00 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, 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.

Globalisers
Fedor Pakhomov
Institute of Mathematics
Monday, 13. July 2020 - 13:30 to 15:00
A globaliser of a c.e. first-order theory T is a c.e. theory U such that U is locally interpretable in T and any c.e. theory V locally interpretable in T is globally interpretable in U. From standard results about reflexive theories (e.g. PA, ZF, ZFC) it follows that any reflexive theory is its own globaliser. In recent years Albert Visser proved that Robinson's arithmetic R is its own globaliser. And that there is a globaliser for any sequential c.e. theory T.  In the present talk I would give two proofs of a new result that for any c.e. theory T there is a globaliser. The talk is based on two papers in preparation. One is joint with Albert Visser and the other is joint with Yong Cheng.

Pages