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.

A Walk with Goodstein

David Fernández-Duque

Ghent University and Czech Academy of Sciences

Monday, 21. March 2022 - 16:00 to 17:30

The classical Goodstein process is based on writing numbers in "normal form" in terms of addition and exponentiation with some base k. By iteratively changing base and subtracting one, one obtains very long sequences of natural numbers which eventually terminate. The latter is proven by comparing base-k normal forms with Cantor normal forms for ordinals, and in fact this proof relies heavily on the notion of normal form. The question then naturally arises: what if we write natural numbers in an arbitrary fashion, not necessarily using normal forms? What if we allow not only addition and exponentiation, but also multiplication for writing numbers?

A "Goodstein walk" is any sequence obtained by following the standard Goodstein process but arbitrarily choosing how each element of the sequence is represented. As it turns out, any Goodstein walk is finite, and indeed the longest possible Goodstein walk is given by the standard normal forms. In this talk we sketch a proof of this fact... more

Nisan-Wigderson generators in Proof Complexity: New lower bounds

Erfan Khaniki

Institute of Mathematics

Monday, 14. March 2022 - 16:00 to 17:30

A map g:{0,1}^n --> {0,1}^m (m>n) is a hard proof complexity generator for a proof system P iff for every string b in {0,1}^m\Rng(g) the formula \tau_b(g), naturally expressing b \not \in Rng(g), requires superpolynomial size P-proofs. One of the well-studied maps in the theory of proof complexity generators is the Nisan-Wigderson generator. Razborov (Annals of Mathematics 2015) conjectured that if A is a suitable matrix and f is a NP \cap CoNP function hard-on-average for P/poly, then NW_{f, A} is a hard proof complexity generator for Extended Frege.

In this talk, we prove a form of Razborov's conjecture for AC0-Frege. We show that for any symmetric NP \cap CoNP function f that is exponentially hard for depth two AC0 circuits, NW_{f, A} is a hard proof complexity generator for AC0-Frege in a natural setting.

On Semi-Algebraic Proofs and Algorithms

Robert Robere

McGill University

Monday, 7. March 2022 - 16:00 to 17:30

We discuss a new characterization of the Sherali-Adams proof system, a standard propositional proof system considered in both proof complexity and combinatorial optimization, showing that there is a degree-d Sherali-Adams refutation of an unsatisfiable CNF formula F if and only if there is an ε > 0 and a degree-d conical junta J such that viol(x) − ε = J, where viol(x) counts the number of falsified clauses of F on an input x. This result implies that the linear separation complexity, a complexity measure recently studied by Hrubes (and independently by de Oliveira Oliveira and Pudlak under the name of weak monotone linear programming gates), monotone feasibly interpolates Sherali-Adams proofs, sharpening a feasible interpolation result of Hakoniemi. On the lower-bound side, we prove a separation between the conical junta degree of viol(x) - 1 and Resolution width; since Sherali-Adams can simulate Resolution this also separates the conical junta degree of viol(x) - 1 and viol(x) -... more

slides

Resolution, Heavy Width and Pseudorandom Generators

Dmitry Sokolov

St Petersburg State University and PDMI RAS

Monday, 21. February 2022 - 16:00 to 17:30

Following the paper of Alekhnovich, Ben-Sasson, Razborov, Wigderson we call a pseudorandom generator hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement that b is outside of the image for any string b \in {0, 1}^m.

In ABRW04 the authors suggested the "functional encoding" of the considered statement for Nisan--Wigderson generator that allows the introduction of "local" extension variables and gave a lower bound on the length of Resolution proofs if the number of extension variables is bounded by the n^2 (where n is the number of inputs of the PRG).

In this talk, we discuss a "heavy width" measure for Resolution that allows us to show a lower bound on the length of Resolution proofs of the considered statement for the Nisan--Wigderson generator with a superpolynomial number of local extension variables. It is a solution to one of the open problems from ABRW04.