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.

Proof-theoretic analysis of some impredicative theories

Fedor Pakhomov
Institute of Mathematics
Monday, 9. March 2020 - 13:30 to 15:00
In the field of ordinal analysis there is an important boundary between theories of predicative strength and essentially stronger impredicative theories. Calculation of proof-theoretic ordinals of impredicative theories requires considerably more advanced technique. This talk will be about relatively weak impredicative theories: theories of positive inductive definitions, Kripke-Platek set theory, and system of second-order arithmetic Pi^1_1-CA_0.  The key feature exhibiting by ordinal notation systems for this theories (in contrast with ordinal notations for predicative theories) is that they use larger ordinals to denote smaller ordinals. In the present talk I will discuss this ordinal notation systems and outline the method of proof-theoretic analysis of this systems based on operator-controlled derivation.

Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs, Part 2

Susanna F. de Rezende
Institute of Mathematics
Monday, 2. March 2020 - 13:30 to 15:00
In this talk, we will present Razborov's pseudo-width method and explain how it can be extended to obtain exponential resolution lower bounds for the weak pigeonhole principle (PHP) and perfect matching formulas over highly unbalanced, sparse expander graphs. Our result establishes strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov '03, '04]. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking other longstanding open problems for resolution and other proof systems. This is... more

Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs

Susanna F. de Rezende
Institute of Mathematics
Monday, 24. February 2020 - 13:30 to 15:00
In this talk, we will present Razborov's pseudo-width method and explain how it can be extended to obtain exponential resolution lower bounds for the weak pigeonhole principle (PHP) and perfect matching formulas over highly unbalanced, sparse expander graphs. Our result establishes strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov '03, '04]. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking other longstanding open problems for resolution and other proof systems. This is joint work with Jakob Nordström, Kilian Risse and Dmitry Sokolov.

Proof complexity of logics of bounded branching, Part 2

Emil Jeřábek
Institute of Mathematics
Monday, 3. February 2020 - 13:30 to 15:00
We revisit the problem of Frege and extended Frege (EF) lower bounds for transitive modal logics. Hrubes proved an exponential lower bound on the number of lines in Frege proofs, or equivalently, on the size of EF proofs, for some basic modal logics such as K, K4, S4, and GL. This was extended by Jerabek to an exponential separation between EF and substitution Frege (SF) systems for all transitive logics of unbounded branching.

On the other hand, for typical logics of bounded width, the EF and SF systems are p-equivalent, and they are in a certain sense p-equivalent to the classical EF system, for which we do not know any lower bounds, and even candidate hard tautologies are scarce.

The main ingredients in all the lower bounds above (as well as similar bounds for superintuitionistic logics) were variants of the feasible disjunction property (DP), playing a role similar to feasible interpolation in classical proof systems.

This raises the question what happens for... more

Pages