•  
    • Tin Lok Wong
    • (National University of Singapore)
    • Arithmetic under negated induction
    • Abstract:
    • 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).
    • 13.12.21   13:00
    • Jan Pich
    • (University of Oxford)
    • Learning algorithms versus automatability of Frege systems
    • Abstract:
    • 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 for P=WF, then Items 1 and 2 are equivalent for P=WF.

      If there is a function h in NE\cap coNE which is hard on average for circuits of size 2^{n/4}, for each sufficiently big n, then there is an explicit propositional proof system P satisfying properties I.-III., i.e. the equivalence of Items 1 and 2 holds for P.

      This is joint work with Rahul Santhanam.

    • 06.12.21   16:00
    • Fedor Part
    • (Institute of Mathematics)
    • On the Complexity of Algebraic Proofs of Membership in the Complement of an Affine Image of the Boolean Cube
    • Abstract:
    • 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.
    • 29.11.21   16:00
    • Susanna de Rezende
    • (Institute of Mathematics)
    • Average-case hardness of clique
    • Abstract:
    • 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.
    • 15.11.21   16:00
    • Damir Dzhafarov
    • (University of Connecticut and Charles University)
    • New developments in reverse mathematics
    • Abstract:
    • 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.
    • 08.11.21   16:00
    • Ilario Bonacina
    • (UPC Barcelona)
    • On the strength of the Sherali-Adams proof system
    • Abstract:
    • 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.

    • 25.10.21   16:00
    • Theodoros Papamakarios
    • (University of Chicago)
    • A super-polynomial separation between resolution and cut-free sequent calculus
    • Abstract:
    • We show a quadratic separation between resolution and cut-free sequent calculus width. We use this gap to get, first, a super-polynomial separation between resolution and cut-free sequent calculus for refuting CNF formulas, and secondly, a quadratic separation between resolution width and monomial space in polynomial calculus with resolution. Our super-polynomial separation between resolution and cut-free sequent calculus only applies when clauses are seen as disjunctions of unbounded arity; our examples have linear size cut-free sequent calculus proofs writing, in a particular way, their clauses using binary disjunctions. Interestingly, this shows that the complexity of sequent calculus depends on how disjunctions are represented.
    • 04.10.21   16:00
    • Marco Carmosino
    • (Boston University)
    • LEARN-Uniform Circuit Lower Bounds and Provability in Bounded Arithmetic
    • Abstract:
    • We investigate randomized LEARN-uniformity, which captures the power of randomness and equivalence queries (EQ) in the construction of Boolean circuits for an explicit problem. This is an intermediate notion between P-uniformity and non-uniformity motivated by connections to learning, complexity, and logic. Building on a number of techniques, we establish the first unconditional lower bounds against LEARN-uniform circuits. For example:

      For each k >= 1, there is a language L in NP such that circuits for L of size O(n^k) cannot be learned in deterministic polynomial time with access to n^o(1) EQs.

      We employ such results to investigate the (un)provability of non-uniform circuit upper bounds (e.g., Is NP contained in SIZE[n^3]?) in theories of bounded arithmetic. Some questions of this form have been addressed in recent papers of Krajicek-Oliveira (2017), Muller-Bydzovsky (2020), and Bydzovsky-Krajicek-Oliveira (2020) via a mixture of techniques from proof theory, complexity theory, and model theory. In contrast, by extracting computational information from proofs via a direct translation to LEARN-uniformity, we establish robust unprovability theorems that unify, simplify, and extend nearly all previous results. In addition, our lower bounds against randomized LEARN-uniformity yield unprovability results for theories augmented with the dual weak pigeonhole principle, such as APC^1 (Jerabek, 2007), which is known to formalize a large fragment of modern complexity theory.

      Finally, we make precise potential limitations of theories of bounded arithmetic such as PV (Cook, 1975) and Jerabek's theory APC^1, by showing unconditionally that these theories cannot prove statements like "NP is not contained in BPP, and NP is contained in ioP/poly", i.e., that NP is uniformly "hard" but non-uniformly "easy" on infinitely many input lengths. In other words, if we live in such a complexity world, then this cannot be established feasibly.

       

    • 14.06.21   15:45
    • Iddo Tzameret
    • (Imperial College London)
    • A Diagonalization-Based Approach to Proof Complexity
    • Abstract:
    • We propose a diagonalization-based approach to several important questions in proof complexity. We illustrate this approach in the context of the algebraic proof system IPS and in the context of propositional proof systems more generally.

      We use the approach to give an explicit sequence of CNF formulas phi_n such that VNP \neq VP iff there are no polynomial-size IPS proofs for the formulas phi_n. This provides the first natural equivalence between proof complexity lower bounds and standard algebraic complexity lower bounds. Our proof of this fact uses the implication from IPS lower bounds to algebraic complexity lower bounds due to Grochow and Pitassi together with a diagonalization argument: the formulas phi_n themselves assert the non-existence of short IPS proofs for formulas encoding VNP \neq VP at a different input length. Our result also has meta-mathematical implications: it gives evidence for the difficulty of proving strong lower bounds for IPS within IPS.

      For any strong enough propositional proof system R, we define the *iterated R-lower bound formulas*, which inductively assert the non-existence of short R proofs for formulas encoding the same statement at a different input length, and propose them as explicit hard candidates for the proof system R. We observe that this hypothesis holds for Resolution following recent results of Atserias and Muller and of Garlik, and give evidence in favour of it for other proof systems.

      Joint work with Rahul Santhanam

    • 07.06.21   15:45
    • Valery Isaev
    • (JetBrains research)
    • Introduction to homotopy type theory
    • Abstract:
    • Homotopy type theory (HoTT) is a new field of mathematics that blends logic, homotopy theory, and the theory of programming languages. In this talk, I will describe all the components of HoTT including necessary type theoretic construction. I will compare this theory with more traditional set theories like ZFC and show how homotopy theoretic constructions such as spheres and homotopy groups are defined in HoTT. I will also show how to work with such a theory in a proof assistant by providing examples of discussed concepts. Finally, I will discuss one of the open problems in the field.
    • 24.05.21   15:45
    • Mateusz Lelyk
    • (Department of Philosophy, University of Warsaw)
    • Proof theoretic properties of truth predicates II
    • Abstract:
    • During the talk we discuss the lengths of proofs of arithmetical sentences in canonical truth theories. We focus mainly on extensions of the canonical compositional truth theory CT^-, introduced in the first talk of Bartosz Wcis?o. In particular, we present a proof of the existence of a PTIME computable function f such that for every CT^- proof p of an arithmetical sentence A, f(p) is a PA-proof of A. Our proof relies on the arithmetization and uniformity of the Enayat-Visser model-theoretic construction of models with satisfaction classes. If time permits we shall comment on the speed-up phenomenon for various other truth theories, such as Kripke-Feferman (KF^-) and Friedman-Sheard (FS^-).
    • 17.05.21   15:30
    • Bartosz Wcislo
    • (Institute of Mathematics, Polish Academy of Sciences)
    • Proof theoretic properties of truth predicates I
    • Abstract:
    • Axiomatic theory of truth is an area of logic which studies this notion in the following way: To a fixed base theory B (which in this talk will be Peano Arithmetic, PA), we add a fresh predicate T(x) with the intended reading "x is (a Goedel code of) a true sentence" and axioms which guarantee that the predicate T has a truth-like behaviour. For instance, we can stipulate that T satisfies Tarskian compositional conditions for arithmetical sentences (obtaining a theory called CT^-) or that it satisfies various forms of induction.

      It is a classical result that the theory CT^- with the full induction scheme for the formulae containing the truth predicate, called CT, is not conservative over PA. In fact, it proves so called global reflection principle which says that an arbitrary arithmetical sentence provable in PA is true (in the sense of the truth predicate). On the other hand, a theorem by Kotlarski, Krajewski, and Lachlan shows that CT^- is conservative.

      In the presentation, we will discuss Tarski Boundary programme which tries to delineate the conservative and nonconservative extensions of the compositional truth theory CT^-. It turns out that many natural nonconservative truth axioms are exactly equivalent to Global Reflection which appears to be arguably the minimal "natural" truth theory which is not conservative over PA (though now we can systematically produce theories of truth whose strength is below Global Reflection).

      On the other hand, Enayat and Visser invented a remarkably effective method of demonstrating that certain extensions of CT^- are in fact conservative which relies on a neat model-theoretic argument. It turns out that the uniformmity of this method allows in fact to obtain much more fine-grained understanding of the proof-theoretic properties of CT^-. In particular, one can show that proofs of arithmetical statements from the compositional truth axioms can be reduced to proofs in Peano Arithmetic with a PTIME algorithm.

      This the first half of a two-part talk. It will be devoted mostly to the conservativeness of truth theories while the reducibility issues will be discussed mostly in the second part.

    • 10.05.21   15:30
    • Raheleh Jalali
    • (Utrecht University)
    • Feasible disjunction property for intuitionistic modal logics
    • Abstract:
    • In this talk, we present a uniform method to prove feasible disjunction property (DP) for various intuitionistic modal logics. More specifically, we prove that if the rules in a sequent calculus for a modal intuitionistic logic have a special form, then the sequent calculus enjoys feasible DP. Our method is essentially an adaptation of the method used by Hrubes in his lower bound proof for the intuitionistic Frege system. As a consequence, we uniformly prove that the sequent calculi for intuitionistic logic, the intuitionistic version of several modal logics such as K, T, K4, S4, S5, their Fisher-Servi versions, propositional lax logic, and many others have feasible DP. Our method also provides a way to prove negative results: we show that any intermediate modal logic without DP does not have a calculus of the given form. This talk is based on a joint work with Amir Tabatabi.
    • 26.04.21   15:30
    • Radek Honzik
    • (Charles University)
    • Compactness at small cardinals
    • Abstract:
    • We will survey some results related to compactness principles at small cardinals which extend the usual first-order compactness to more complex structures.

      More specifically, suppose kappa is an uncountable regular cardinal (typically kappa can be taken to be the size of the reals). We will review a variety of compactness principles, such as the tree property, stationary reflection, Rado's conjecture, etc., which claim that if all parts of size < kappa of a given structure of size kappa have some property, so does the whole structure.

      We will discuss basic models in which such principles hold, consistency strength of these principles, implications between the principles and other hypotheses (such as CH), and some consequences.

    • 12.04.21   15:30
    • Barnaby Martin
    • (Durham University)
    • Depth lower bounds in Stabbing Planes for combinatorial principles
    • Abstract:
    • We prove logarithmic depth lower bounds in Stabbing Planes for the classes of combinatorial principles known as the Pigeonhole principle and the Tseitin contradictions. The depth lower bounds are new, obtained by giving almost linear length lower bounds which do not depend on the bit-size of the inequalities and in the case of the Pigeonhole principle are tight.

      The technique known so far to prove depth lower bounds for Stabbing Planes is a generalization of that used for the Cutting Planes proof system. In this work we introduce two new approaches to prove length/depth lower bounds in Stabbing Planes: one relying on Sperner's Theorem which works for the Pigeonhole principle and Tseitin contradictions over the complete graph; a second proving the lower bound for Tseitin contradictions over a grid graph, which uses a result on essential coverings of the boolean cube by linear polynomials, which in turn relies on Alon's combinatorial Nullenstellensatz.

      (Joint work with Stefan Dantchev, Nicola Galesi and Abdul Ghani.)

    • 29.03.21   15:30
    • Dmitry Itsykson
    • (Steklov Institute of Mathematics at St.Petersburg)
    • Proof complexity of natural formulas via communication arguments
    • Abstract:
    • A canonical communication problem Search(F) is defined for every unsatisfiable CNF F: an assignment to the variables of F is distributed among the communicating parties, they are to find a clause of F falsified by this assignment. Lower bounds on the communication complexity of Search(F) imply tree-size lower bounds, rank lower bounds, and size-space tradeoffs for the formula F in a large class of proof systems. All known lower bounds on Search(F) are realized on ad-hoc formulas F (i.e. they were introduced specifically for these lower bounds). We introduce a new communication complexity approach that allows establishing proof complexity lower bounds for natural formulas.

       

      First, we demonstrate our approach for two-party communication and prove an exponential lower bound on the size of tree-like Res(+) refutations of the Perfect matching principle. Then we apply our approach to k-party communication complexity in the NOF model and obtain a lower bound on the randomized k-party communication complexity of Search(BPHP) w.r.t. to some natural partition of the variables, where BPHP is the bit pigeonhole principle. In particular, this lower bound implies that the bit pigeonhole requires exponential tree-like Th(k) proofs, where Th(k) is the semantic proof system operating with polynomial inequalities of degree at most k.

       

      The talk is based on the joint work with Artur Riazanov that is available as ECCC report https://eccc.weizmann.ac.il/report/2020/184/.
    • 15.03.21   15:30
    • Jan Krajíček
    • (Charles University)
    • Information in propositional proofs and algorithmic proof search
    • Abstract:
    • Motivated by the *informal* proof search problem:  "Is there an optimal way to search for propositional proofs?" I present a few proof complexity results, a new notion and some problems.
    • 01.03.21   15:45
    • Tuomas Hakoniemi
    • (Universitat Politčcnica de Catalunya)
    • Feasible interpolation and (semi-)algebraic proof systems
    • Abstract:
    • In this talk we discuss feasible interpolation for the algebraic and semialgebraic proof systems Polynomial Calculus, Sums-of-Squares and Sherali-Adams. We show that each system admits feasible interpolation in the following form: there is a poly-time algorithm that given two sets P(x,z) and Q(y,z) of polynomial constraints in distinct sequences x,y and z of variables; a refutation of the union of P(x,z) and Q(y,z) and an assignment a to the z variables, outputs either a refutation of P(x,a) or a refutation of Q(y,a). In each case the proof combines a semantic proof of the existence of a suitable resource-bounded refutation of either P(x,a) or Q(y,a) with an efficient proof search algorithm for the said refutations.
    • 15.02.21   15:30
    • Olaf Beyersdorff
    • (Friedrich Schiller University Jena)
    • Quantified Boolean formulas: proof systems, circuit complexity, and solving
    • Abstract:
    • This talk will start with an overview of the relatively young field of QBF proof complexity, explaining QBF proof systems (including QBF resolution) and an assessment of which lower bound techniques are available for QBF proof systems. In the main part of the talk, I will explain hardness characterisations for QBF proof systems in terms of circuit complexity, yielding very direct connections between circuit lower bounds and QBF proof system lower bounds. The talk will also cover the relations between QBF resolution and QCDCL solving algorithms. Modelling QCDCL as proof systems we show that QCDCL and Q-Resolution are incomparable.

      This talk is based on two recent papers, joint with Joshua Blinkhorn and Meena Mahajan (LICS'20) and with Benjamin Boehm (ITCS'21).

    • 11.01.21   15:30

    Pavel Pudlak, Neil Thapen, Jan Krajíček
    organizers

  •