This work is joint with Marta Fiori-Carones (Novosibirsk), Leszek Aleksander Kolodziejczyk (Warsaw) and Keita Yokoyama (Sendai).

Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček

More information on the old seminar web page. The programme is announced via the mailing list.

National University of Singapore

Monday, 13. December 2021 - 13:00 to 14:30

https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz before the meeting to join

Arithmetic generally does not admit any non-trivial quantifier elimination. I will talk about one exception, where the negation of an induction axiom is included in the theory. Here the Weak Koenig Lemma from reverse mathematics arises as a model completion.

This work is joint with Marta Fiori-Carones (Novosibirsk), Leszek Aleksander Kolodziejczyk (Warsaw) and Keita Yokoyama (Sendai).

This work is joint with Marta Fiori-Carones (Novosibirsk), Leszek Aleksander Kolodziejczyk (Warsaw) and Keita Yokoyama (Sendai).

University of Oxford

Monday, 6. December 2021 - 16:00 to 17:30

Zitna, rear building, ground floor and zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join

We connect learning algorithms and algorithms automating proof search in propositional proof systems: for every sufficiently strong, well-behaved propositional proof system P, we prove that the following statements are equivalent,

1. Provable learning: P proves efficiently that p-size circuits are learnable by subexponential-size circuits over the uniform distribution with membership queries.

2. Provable automatability: P proves efficiently that P is automatable by non-uniform circuits on propositional formulas expressing p-size circuit lower bounds.

Here, P is sufficiently strong and well-behaved if I.-III. holds: I. P p-simulates Jeřábek's system WF (which strengthens the Extended Frege system EF by a surjective weak pigeonhole principle); II. P satisfies some basic properties of standard proof systems which p-simulate WF; III. P proves efficiently for some Boolean function h that h is hard on average for circuits of subexponential size. For example, if III. holds... more

Institute of Mathematics

Monday, 29. November 2021 - 16:00 to 17:30

*NOT BROADCAST* in IM, rear building, ground floor

For a field F, char(F) > 3, and an affine map A : F^n -> F^m we form a contradiction by picking some b not in A({0,1}^n) and saying Ax = b. This can be written as a system of 0-1 unsatisfiable linear equations over F expressible in the language of algebraic proof systems like Res(lin), NS, PC over F. One may think of these instances as the Subset Sum principle in positive characteristic. I'll suggest some hardness criterions for such instances and prove lower bounds for linear decision trees, tree-like Res(lin) and some restricted dag-like Res(lin) refutations. I'll also discuss work in progress on lower bounds for general dag-like Res(lin) refutations and PC refutations of these instances.

Institute of Mathematics

Monday, 15. November 2021 - 16:00 to 17:30

*NOT BROADCAST* - IM large seminar room, rear building, ground floor

We will start by recalling what is currently known about the hardness of refuting the clique formula on random graphs. We will then sketch some ideas on how to generalize these results to stronger proof systems.

University of Connecticut and Charles University

Monday, 8. November 2021 - 16:00 to 17:30

Zitna, back building, first floor (by offices) and zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join

I will give a brief introduction to reverse mathematics, focusing on computable combinatorics, and survey some recent trends and results in the subject. No prior background beyond basic logic is necessary.

UPC Barcelona

Monday, 25. October 2021 - 16:00 to 17:30

IM rear building, first floor *NOT BROADCAST*

This talk is about Sherali-Adams when considered as a propositional proof system. We will present some propositional proof systems equivalent to it and we will prove two results upper-bounding the strength of Sherali-Adams. More precisely, we will prove that (1) depth-2 Frege + PHP p-simulates Sherali-Adams with unary coefficients, and (2) depth-2 Frege +"wtPHP" p-simulates Sherali-Adams (with coefficients in binary). The "wtPHP" is a new combinatorial principle, some sort of "weighted" version of the pigeonhole principle.

This talk is based on a joint work with Maria Luisa Bonet.