•  
    • Dmitry Sokolov
    • (EPFL)
    • Top-down depth-4 circuit lower bounds
    • Abstract:
    • In this talk, we present a top-down lower-bound method for depth-4 boolean circuits. In particular, we give a new proof of the well-known result that the parity function requires depth-4 circuits of size exponential in n^{1/3}. Our proof is an application of robust sunflowers and block unpredictability. Joint work with Mika Göös, Artur Riazanov and Anastasia Sofronova
    • 05.06.23   16:00
    • Leonardo Coregliano
    • (IAS Princeton)
    • Continuous combinatorics
    • Abstract:
    • The field of continuous combinatorics is the study of (large, dense) combinatorial structures using tools typically associated with continuous objects, such as tools from analysis, topology or measure theory. The field started under the name of "graph limits" since the main object of study were graphons, i.e., limits of graphs. Since then, several other limits have been constructed for all sorts of combinatorial objects (e.g., digraphs, hypergraphs, permutations, etc.) and even general limits were provided through the unifying theory of flag algebras.

      However, the limits constructed in the theory of flag algebras are of an algebraic/syntactic nature, due to the minimalist nature of the theory (as opposed to the more semantic/geometric nature of the previous ad hoc limits of the literature). In this talk, I will present the semantic/geometric counterpart to flag algebras: the theory of theons. I will also give a couple of examples of proofs both within continuous combinatorics and of applications that use its tools.

      This talk is based on joint work with Alexander A. Razborov.

    • 22.05.23   16:00
    • Emil Jeřábek
    • (IM CAS)
    • A simplified lower bound on intuitionistic implicational proofs
    • Abstract:
    • Unlike classical Frege systems, we know exponential lower bounds for some non-classical logics (modal, superintuitionistic, substructural), starting with seminal work of Hrubes (2007); they are all based on variants of the feasible disjunction property that play a similar role as monotone feasible interpolation for classical proof systems. This might suggest that disjunction is essential for these lower bounds, but Jerabek (2017) adapted them to the implicational fragment of intuitionistic logic. This results in a complex argument employing an implicational translation of intuitionistic logic on top of the proof of the lower bound proper, which in turn relies on monotone circuit lower bounds (Razborov, Alon-Boppana).

      I will show how to prove the exponential lower bound directly for intuitionistic implicational logic without any translations, using a simple argument based on an efficient version of Kleene's slash. Apart from Frege, it applies directly to sequent calculus and (dag-like) natural deduction, obviating also the need for translation of these proof systems to Frege.

      I will also mention a tangentially related problem about classical Frege systems.

      One motivation for this work comes from presistent claims by Gordeev and Haeusler, who purport to show that all intuitionistic implicational tautologies have polynomial-size dag-like natural deduction proofs, implying NP = PSPACE. Their claims are false as they contradict the above-mentioned exponential lower bounds (and, in fact, also exponential lower bounds on constant-depth Frege), but for a non-specialist, understanding this requires tracking down multiple papers and some reading between the lines. Our argument consolidates all proof-theoretic components of the lower bound into one simple proof, depending only on the Alon-Boppana circuit lower bound.

       

    • 15.05.23   16:00
    • Amirhossein Akbar Tabatabai
    • (University of Groningen)
    • Unearthing the Feasible World: A Proposal
    • Abstract:
    • The decades-long practice of complexity theory and bounded arithmetic provided some strong clues for the existence of an alternative yet rich feasible world, where for instance all the functions are feasible and the polynomially and exponentially bounded sets are the new finite and infinite, respectively. The situation is similar to the so-called computable and continuous worlds whose traces first unearthed in constructive mathematics and later realized by the forcing-style model constructions that elevated to a general and conceptual theory called the topos theory. In this talk, imitating the main ideas of topos theory, we propose a program to provide a general machinery for the feasible forcing in order to prove some independence results for weak arithmetic, on the one hand and find a conceptual understanding of the low complexity computation, on the other. As we will see, any fulfillment of that proposal needs a certain (geometric) form of structural theory and one canonical base model. We will report some of our partial results to find these two ingredients. For the first, we will present our structural theory for the low complexity versions of the inductive objects like the natural numbers, binary strings, ordinals and sets. For the latter, we will explain our imitation of Hyland's construction of the computable world (effective topos) for the feasible functions and the problematic role of the intuitionistic implication there that leads to our general theory of implication and its inherent non-geometricity. Despite what it appears at the first glance, we will not assume any familiarity with category theory and topos theory and the talk will be rather informal in this respect.
    • 10.05.23   16:00
    • Pavel Pudlák
    • (IM CAS)
    • Some remarks on Herbrand's Theorem
    • Abstract:
    • In [3] I proved Proposition 4.3 about the impossibility of certain forms of the formulas in Herbrand's Theorem. This is seemingly in contradiction with Theorem 6 of Buss, Kolodzieczyk and Thapen [1], and a more recent Theorem 3.2 of Li and Oliveira of [2]. Nevertheless, all theorems hold true. In the lecture I will explain the differences and prove my Proposition with an explicit formula, which is not in [3].

      [1] Buss, Kolodzieczyk and Thapen: Fragments of approximate counting, JSL 79. [2] Li, Igor Carboni Oliveira: Unprovability of strong complexity lower bounds in bounded arithmetic. ECCC~TR23-022. [3] P. Pudlak: Consistency and games - in search of new combinatorial principles. Proc. Logic Colloquium'03.

    • 24.04.23   16:00
    • Ilario Bonacina
    • (Universitat Politčcnica de Catalunya )
    • Polynomial Calculus for MaxSAT
    • Abstract:
    • MaxSAT is the problem of finding an assignment satisfying the maximum number of clauses in a CNF formula. We consider a natural generalization of this problem to generic sets of polynomials and propose a weighted version of Polynomial Calculus to address this problem.

      Weighted Polynomial Calculus is a natural generalization of MaxSAT-Resolution and weighted Resolution that manipulates polynomials with coefficients in a finite field and either weights in N or Z. We show the soundness and completeness of these systems via an algorithmic procedure.

      Weighted Polynomial Calculus, with weights in N and coefficients in F_2, is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in Z, it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable.

       

    • 17.04.23   16:00
    • Ján Pich
    • (University of Oxford)
    • Towards P != NP from Extended Frege lower bounds
    • Abstract:
    • We prove that if conditions I-II (below) hold and there is a sequence of Boolean functions $f_n$ hard to approximate by p-size circuits such that p-size circuit lower bounds for $f_n$ do not have p-size proofs in Extended Frege system EF, then $P \ne NP$.

      I. $S^1_2$ proves that there is a function $g\in E$ hard to approximate by subexponential-size circuits.

      II. (Learning from the non-existence of OWFs.) $S^1_2$ proves that a p-time reduction transforms circuits breaking one-way functions to p-size circuits learning p-size circuits over the uniform distribution, with membership queries.

      Here, $S^1_2$ is Buss's theory of bounded arithmetic formalizing p-time reasoning.

      Further, we show that any of the following assumptions implies that $P \ne NP$, if EF is not p-bounded:

      1. (Feasible anticheckers.) $S^1_2$ proves that a p-time function generates anticheckers for SAT.

      2. (Witnessing $NP\not\subseteq P/poly$.) $S^1_2$ proves that a p-time function witnesses an error of each p-size circuit which fails to solve SAT.

      3. (OWFs from $NP\not\subseteq P/poly$ & hardness of E.) Condition I holds and $S^1_2$ proves that a p-time reduction transforms circuits breaking one-way functions to p-size circuits computing SAT.

      The results generalize to stronger theories and proof systems.

      This is joint work with Rahul Santhanam.

       

    • 12.12.22   16:00
    • Moritz Müller
    • (University of Passau)
    • On the parameterized complexity of Delta-0 truth
    • Abstract:
    • We consider the problem, given a ?0 formula ?(x) and a natural number n in unary, whether ?(n) is true. We are interested in instances of the problem where n is much bigger than ?. More precisely, we consider the parameterized problem with parameter |?|. We show unconditionally that this problem does not belong to the parameterized version of AC0. We also show that certain natural upper bounds on the parameterized complexity of the problem imply separations of classical complexity classes. These results are obtained by an analysis of a parameterized halting problem. A related problem concerns the provability of the MRDP theorem in bounded arithmetic.
    • 21.11.22   16:00
    • Martin Suda
    • (CVUT)
    • Integrating Machine Learning into Saturation-based ATPs
    • Abstract:
    • Applying the techniques of machine learning (ML) promises to dramatically improve the performance of modern automatic theorem provers (ATPs) and thus to positively impact their applications. The most successful avenue in this direction explored so far is machine-learned clause selection guidance, where we learn to recognize and prefer for selection clauses that look like those that contributed to a proof in past successful runs. In this talk I present Deepire, an extension of the ATP Vampire where clause selection is guided by a recursive neural network (RvNN) for classifying clauses based solely on their derivation history.
    • 14.11.22   16:00
    • Emil Jeřábek
    • (IM CAS)
    • Elementary analytic functions in VTC^0, Part 2
    • Abstract:
    • It is known that rational approximations of elementary analytic functions (exp, log, trigonometric and hyperbolic functions, and their inverse functions) are computable in the complexity class TC^0. In this talk, we will show how to formalize their construction and basic properties in the correspoding arithmetical theory VTC^0, working with completions of fraction fields of models of VTC^0. As a consequence, we will show that every countable model of VTC^0 is an exponential integer part of a real-closed exponential field, using a recursive saturation argument.
    • 24.10.22   16:00
    • Emil Jeřábek
    • (IM CAS)
    • Elementary analytic functions in VTC^0
    • Abstract:
    • It is known that rational approximations of elementary analytic functions (exp, log, trigonometric and hyperbolic functions, and their inverse functions) are computable in the complexity class TC^0. In this talk, we will show how to formalize their construction and basic properties in the correspoding arithmetical theory VTC^0, working with completions of fraction fields of models of VTC^0. As a consequence, we will show that every countable model of VTC^0 is an exponential integer part of a real-closed exponential field, using a recursive saturation argument.
    • 17.10.22   16:00
    • Chris Lambie-Hanson
    • (IM CAS)
    • Compactness and incompactness in set theory, with applications to uncountable graphs
    • Abstract:
    • (Joint seminar with set theory group) The study of compactness phenomena at uncountable cardinals has been a central line of research in combinatorial set theory since the mid-twentieth century. In the first part of this talk, we will give a broad overview of this area of research and survey some of its most prominent results. We will then look at a few recent results concerning compactness phenomena for uncountable graphs. We first look at possible generalizations of the de Bruijn-Erdos compactness theorem for chromatic numbers to uncountable cardinalities, in particular showing that consistently there are large uncountable graphs witnessing extreme failures of compactness for, e.g., the property of having a countable chromatic number. We then turn to the study of the structure of the collections of finite subgraphs of uncountably chromatic graphs, answering a question of Erdos, Hajnal, and Szemeredi about the growth rates of chromatic numbers in such collections of finite subgraphs.
    • 26.09.22   16:00
    • Rahul Santhanam
    • (University of Oxford)
    • On the Conjectures of Razborov and Rudich
    • Abstract:
    • We say that Rudich's Conjecture holds for a propositional proof system Q if there are no efficient Q-proofs of random truth table tautologies. We say that Razborov's Conjecture holds for a propositional proof system Q if there are no efficient Q-proofs of any truth table tautologies. A fundamental task in proof complexity and the meta-mathematics of circuit lower bounds is to understand for which Q these conjectures hold. We show various results about these conjectures, including evidence for their difficulty.

      Based on joint work with Jan Pich.

    • 23.05.22   16:00
    • Leszek Kołodziejczyk
    • (University of Warsaw)
    • In search of the first-order part of Ramsey's theorem for pairs
    • Abstract:
    • Reverse mathematics studies the logical strength of mathematical theorems formalized as statements in the language of second-order arithmetic (which is a two-sorted language with one sort of variables for natural numbers and another for sets of natural numbers). The strength is usually measured in terms of implications between the theorems and some set existence axioms, but it also makes sense to ask about the first-order consequences of a theorem, that is, what statements about natural numbers it implies.

      In recent decades, a particularly interesting case study has been provided by RT^2_2: Ramsey's theorem for pairs and two colours. RT^2_2 and its variants are anomalous in the sense of not being equivalent to any of the typical set existence axioms considered in reverse mathematics, or to each other. Characterizing the first-order part of RT^2_2 is a long-standing and highly interesting open problem. Methods used to make progress on this problem have typically been based on some combination of recursion theory and nonstandard models of arithmetic, with the latter playing an increasingly important role.

      I will briefly discuss some major results on the first-order part of RT^2_2 obtained over the years and then talk about some more recent work related to the problem that I have been involved in (jointly with Marta Fiori Carones, Kasia Kowalik, Keita Yokoyama and Tin Lok Wong).

    • 16.05.22   16:00
    • Yoriyuki Yamagata
    • (AIST)
    • On proving consistency of equational theories in Bounded Arithmetic
    • Abstract:
    • We consider pure equational theories that allow substitution but disallow induction, which we denote as PETS, based on recursive definition of their function symbols. We show that the Bounded Arithmetic theory S12 proves the consistency of PETS. Our approach employs models for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest.
    • 09.05.22   11:00
    • Pavel Pudlák
    • (IM CAS)
    • From Peano Arithmetic to propositional calculus and back
    • Abstract:
    • In the first half of my talk I will mention the history of our logic group in our institute and how we gradually moved from studying metamathematics of Peano Arithmetic to weak fragments, and eventually to proof complexity of propositional logic. In the second part I will talk about my project to define a hierarchy of propositional proof systems indexed by ordinals up to epsilon_0 with the aim to prove that they characterize the proof system associated with Peano Arithmetic.
    • 02.05.22   16:00
    • Leroy Chew
    • (TU Wien)
    • Simulations in QBF Proof Complexity
    • Abstract:
    • Quantified Boolean Formulas (QBF) extend propositional formulas with Boolean quantifiers. Solving a QBF is PSPACE complete, and QBFSAT is seen as a natural extension of the SAT problem. Just as propositional proof complexity underlies the theory behind SAT solving, QBF proof complexity underlies the theory behind QBF solving. Here we will focus on the relative strengths of QBF proof systems via p-simulation.

      On the surface QBF proof systems seem harder to compare to one another since they vary considerably in how they deal with quantification. In particular there's a vast difference between theory systems that generalise from propositional logic, the proof systems that capture the process of CDCL solving and the proof systems that capture the expansion and CEGAR based solvers. And many results do formally show an incomparability in the proof complexity between different systems as we suspect. However, there are a few non-obvious cases where a simulation is possible. In this talk we will examine the landscape of simulation in QBF, looking at the results over the last decade, as well as our own recent work with simulations based on strategy extraction and propositionalisation. We will interpret the theoretical and practical importance of these results.

    • 25.04.22   16:00
    • Azza Gaysin
    • (Charles University)
    • Proof complexity of CSP on algebras with linear congruence, Part 2
    • Abstract:
    • CSP (constraint satisfaction problems) is a class of problems deciding whether there exists a homomorphism from an instance relational structure to a target one. The CSP dichotomy is a profound result recently proved by Zhuk (2020, J. ACM, 67) and Bulatov (2017, FOCS, 58). It says that for each fixed target structure, CSP is either NP-complete or p-time. Zhuk's algorithm for the p-time case of the problem eventually leads to algebras with linear congruence.

      We show that Zhuk's algorithm for algebras with linear congruence can be formalized in the theory V^1. Thus, using known methods of proof complexity, Zhuk's algorithm for negative instances of the problem can be augmented by extra information: it not only rejects X that cannot be homomorphically mapped into A but produces a certificate - a short extended Frege (EF) propositional proof - that this rejection is correct.

    • 11.04.22   16:00
    • Azza Gaysin
    • (Charles University)
    • Proof complexity of CSP on algebras with linear congruence
    • Abstract:
    • CSP (constraint satisfaction problems) is a class of problems deciding whether there exists a homomorphism from an instance relational structure to a target one. The CSP dichotomy is a profound result recently proved by Zhuk (2020, J. ACM, 67) and Bulatov (2017, FOCS, 58). It says that for each fixed target structure, CSP is either NP-complete or p-time. Zhuk's algorithm for the p-time case of the problem eventually leads to algebras with linear congruence.

      We show that Zhuk's algorithm for algebras with linear congruence can be formalized in the theory V^1. Thus, using known methods of proof complexity, Zhuk's algorithm for negative instances of the problem can be augmented by extra information: it not only rejects X that cannot be homomorphically mapped into A but produces a certificate - a short extended Frege (EF) propositional proof - that this rejection is correct.

    • 04.04.22   16:00
    • David Fernández-Duque
    • (Ghent University and Czech Academy of Sciences)
    • A Walk with Goodstein
    • Abstract:
    • 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 and discuss how a similar idea can be applied to other variants of the Goodstein process, including those based on the Ackermann function.

      Joint work with A. Weiermann

    • 21.03.22   16:00
    • Erfan Khaniki
    • (Institute of Mathematics)
    • Nisan-Wigderson generators in Proof Complexity: New lower bounds
    • Abstract:
    • 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.
    • 14.03.22   16:00
    • Robert Robere
    • (McGill University)
    • On Semi-Algebraic Proofs and Algorithms
    • Abstract:
    • 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) - ? for arbitrarily small ? > 0. Finally, by applying known lifting theorems, we can translate this separation into separations between extension complexity and monotone circuit complexity.

      This talk is based on joint work with Noah Fleming, Mika Goos, and Stefan Grosser.

    • 07.03.22   16:00
    • Dmitry Sokolov
    • (St Petersburg State University and PDMI RAS)
    • Resolution, Heavy Width and Pseudorandom Generators
    • Abstract:
    • 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.

    • 21.02.22   16:00
    • Michal Garlik
    • (St. Petersburg Department of Steklov Institute of Mathematics and Euler International Mathematical Institute)
    • A revision of the width method
    • Abstract:
    • We consider a framework for proving lower bounds on the length of proofs in logical calculi that can be seen as a generalization of the game framework in which Pudlák presented Haken's lower bound for resolution. Our framework, while still requiring some notion of width, can be applied in a way that avoids the use of the random restriction technique. As an example, we demonstrate this for resolution, obtaining a proof in which the calculations are very simple.
    • 10.01.22   16:00
    • 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
    • Sam Buss
    • (University of California, San Diego)
    • Propositional branching program proofs and logics for L and NL
    • Abstract:
    • We introduce systems of propositional logic for reasoning directly with decision trees, non-deterministic decision trees, branching programs and non-deterministic branching programs. These propositional systems allow reasoning about properties in non-uniform logarithmic space and non-deterministic logarithmic space. We also report on work-in-progress to use these propositional proof systems for the bounded arithmetic theories VL and VNL with proof theoretic strength corresponding to logarithmic space and non-deterministic logarithmic space. The talk will start with an overview of the propositional proof systems which are already known to have close correspondences with bounded arithmetic. The new results are joint work with Anupam Das and Alexander Knop.
    • 14.12.20   15:30
    • Jeremy Avigad
    • (Carnegie Mellon University)
    • Interactive theorem proving for the working logician
    • Abstract:
    • Over the last few decades, computational proof assistants have made it possible to construct formal axiomatic derivations of increasing complexity. They are now used to verify that hardware and software designs meet their specifications, as well as to verify the correctness of mathematical proofs. The practice has taken root and promises to play an important role in mathematics and computer science.

      In this talk, I will survey the technology, with an emphasis on formal mathematics. I will then discuss aspects of interactive theorem proving that may be of interest to the working logician, and places where a better theoretical understanding can lead to progress. Specifically, I'll discuss the need for practical foundations, search procedures, decision procedures, and proof systems.

    • 07.12.20   15:30
    • Susanna F. de Rezende
    • (IM CAS)
    • Automating tree-like resolution in time n^o(log n/ log log n) is ETH-hard
    • Abstract:
    • It is known that tree-like resolution is automatable in time n^O(log n). In this talk we will show that under ETH tree-like resolution is not automatable in time n^o(log n/ log log n). We will also provide an alternative, arguably simpler proof of the result of Alekhnovich and Razborov (SIAM J. Comput. 2008) that unless the fixed parameter hierarchy collapses, tree-like resolution is not automatable in polynomial time. The proof builds on a joint work with Mika Göös, Jakob Nordström, Toni Pitassi, Robert Robere and Dmitry Sokolov (ECCC 2020), which presents a simplification of the breakthrough result of Atserias and Müller (JACM 2020).
    • 30.11.20   15:30
    • Mikolas Janota
    • (CIIRC)
    • QBF Solving and Calculi, Overview
    • Abstract:
    • Quantified Boolean Formulas (QBFs) enrich the SAT problem with quantifiers taking the problem from NP to PSPACE. Recent years have seen a number of novel approaches to QBF solving. At the same time, QBF calculi were developed to match the solvers. However, there are calculi with no solving counterparts. In this talk I will overview the two prominent paradigms in QBF solving: conflict-driven and expansion-based. I will also discuss the connection between solving and the existing proof systems as well as challenges for future research.
    • 23.11.20   15:30
    • Yaroslav Alekseev
    • (Chebyshev Laboratory, St Petersburg State University)
    • A lower bound for Polynomial Calculus with extension rule
    • Abstract:
    • In this talk we consider an extension of the Polynomial Calculus proof system where we can introduce new variables and take a square root. We prove that an instance of the subset-sum principle, the binary value principle, requires refutations of exponential bit size over rationals in this system. Part and Tzameret proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations) refutations of the binary value principle. We show that our system p-simulates Res-Lin and thus we get an alternative exponential lower bound for the size of Res-Lin refutations of the binary value principle.
    • 16.11.20   15:30
    • Emil Jeřábek
    • (IM CAS)
    • Iterated multiplication in VTC^0, Part 2
    • Abstract:
    • 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 egg"-type problems (the analysis heavily uses various iterated products and divisions, whose existence in VTC^0 a priori requires the very IMUL axiom we'd like to prove). In this talk, we will show that IMUL is, after all, provable in VTC^0. We will outline the main challenges and ways how to get around them. As a byproduct, we will obtain a well-behaved \Delta_0 definition of modular exponentiation in the theory I\Delta_0 + WPHP(\Delta_0).
    • 02.11.20   15:30
    • Emil Jeřábek
    • (IM CAS)
    • Iterated multiplication in VTC^0
    • Abstract:
    • 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 egg"-type problems (the analysis heavily uses various iterated products and divisions, whose existence in VTC^0 a priori requires the very IMUL axiom we'd like to prove). In this talk, we will show that IMUL is, after all, provable in VTC^0. We will outline the main challenges and ways how to get around them. As a byproduct, we will obtain a well-behaved \Delta_0 definition of modular exponentiation in the theory I\Delta_0 + WPHP(\Delta_0).
    • 26.10.20   15:30
    • Erfan Khaniki
    • (IM CAS)
    • Not all Kripke models of HA are locally PA
    • Abstract:
    • 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.
    • 12.10.20   16:00
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Globalisers
    • Abstract:
    • 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.
    • 13.07.20   13:30
    • Michal Garlík
    • (Polytechnic University of Catalonia)
    • Feasible disjunction property and k-DNF resolution
    • Abstract:
    • We discuss feasible disjunction property and reflection principles for propositional proof systems. For every integer $k \geq 2$, we show that $k$-DNF resolution does not have the feasible disjunction property. This contrasts with the case $k = 1$ (the usual resolution). Time permitting, we look at some consequences.
    • 29.06.20   15:15
    • Ján Pich
    • (University of Oxford)
    • Consistency of Nondeterministic Circuit Upper Bounds
    • Abstract:
    • We show unconditionally that Jeřábek's theory of approximate counting APC_1 formalizing probabilistic poly-time reasoning cannot prove, for any non-deterministic poly-time machine M, that M is inapproximable by co-nondeterministic circuits of sub-exponential size. We also show several related results concerning worst-case and zero-error average case lower bounds for various versions of the Minimum Circuit Size Problem against co-nondeterministic circuits.   This is joint work with Rahul Santhanam.
    • 15.06.20   13:30
    • Leszek Kolodziejczyk
    • (University of Warsaw)
    • The logical strength of Büchi's decidability theorem
    • Abstract:
    • I will talk about a result obtained a few years ago jointly with Henryk Michalewski, Pierre Pradic and Micha? Skrzypczak. Our aim was to describe the strength of axioms needed to prove Büchi's theorem, which says that the monadic second order theory of the natural number order is decidable. The axiomatic requirements of theorems involving second-order quantification over the naturals, like Büchi's theorem, are commonly studied within a research programme known as reverse mathematics, and often characterized in terms of an equivalence between the theorem and some fragment of so-called second order arithmetic. I plan to give a (brief) introduction to second order arithmetic and to monadic second order logic. Then I will discuss our main result, which says that Büchi's theorem (suitably formulated) is, over the usual base theory considered in reverse mathematics, equivalent to the induction scheme for Sigma^0_2 formulas. Various automata-theoretic statements related to Büchi's theorem also turn out to be either equivalent to, or provable from, Sigma^0_2 induction.
    • 25.05.20   13:30
    • Susana F. de Rezende
    • (IM CAS)
    • Automating Algebraic Proof Systems is NP-Hard
    • Abstract:
    • Recently, Atserias and Müller (FOCS 2019) established that it is NP-hard to find a resolution refutation of an unsatisfiable formula in time polynomial in the size of the shortest such refutation. In this talk, I will present a simplified proof of this result and explain how it can be extended to hold also for Nullstellensatz, Polynomial Calculus, and Sherali–Adams. This is based on joint work with Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere and Dmitry Sokolov.
    • 11.05.20   13:30
    • Iddo Tzameret
    • (Royal Holloway, University of London)
    • Semi-Algebraic Proofs, IPS lower bounds and the tau-Conjecture
    • Abstract:
    • We introduce the binary value principle which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a well-known hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi (2014). Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semi-algebraic proof systems. Our results extend to full-fledged IPS the paradigm introduced in Forbes, Shpilka, Tzameret and Wigderson (2016), whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semi-algebraic over algebraic reasoning, for sufficiently strong systems.

      Joint work with Yaroslav Alekseev, Dima Grigoriev and Edward A. Hirsch. See full version here: https://eccc.weizmann.ac.il/report/2019/142/download

    • 04.05.20   13:30
    • Pavel Pudlák
    • (IM CAS)
    • Reflection principles in the propositional calculus, Part 2
    • Abstract:
    • I will survey some results on the reflection principles for propositional proof systems, show a connection to the recent result on non-automatibility of Resolution and ask several problems.
    • 27.04.20   13:30
    • Azza Gaysin
    • (Charles University)
    • H-Coloring Dichotomy in Proof Complexity
    • Abstract:
    • The H-Coloring problem can be considered as an example of the computational problem from a huge class of constraint satisfaction problems (CSP): an H-Coloring of a graph G is just a homomorphism from G to H. The dichotomy theorem for H-Coloring was proved by Hell and Nešetřil (an analogous theorem for all CSPs was recently proved by Zhuk and Bulatov) and it says that for each H the problem is either p-time decidable or NP-complete. Since negations of unsatisfiable instances of CSP can be expressed as propositional tautologies, it seems to be natural to investigate the proof complexity of CSP. We show that the decision algorithm in the p-time case of the H-Coloring can be formalized in a relatively weak theory and that the tautologies expressing the negative instances for such H have short proofs in propositional proof system R^*(log). We complement this upper bound result by a lower bound result for the special example of NP-complete case of the H-Coloring, using the known results about proof complexity of the Pigeonhole Principle
    • 20.04.20   13:30
    • Pavel Pudlák
    • (IM CAS)
    • Reflection principles in the propositional calculus.
    • Abstract:
    • I will survey some results on the reflection principles for propositional proof systems, show a connection to the recent result on non-automatibility of Resolution and ask several problems. ** Location: https://us02web.zoom.us/j/472648284 **
    • 14.04.20   13:30
    • Erfan Khaniki
    • (Institute of Mathematics)
    • On the proof complexity of Resolution over Polynomial Calculus
    • Abstract:
    • The refutation system Res_R(PC_d) is a natural extension of the Resolution refutation system such that it operates with disjunctions of degree d polynomials over ring R with boolean variables. For d=1, this system is called Res_R(lin). One of the important open problems in Proof Complexity is proving lower bounds for Res_R(lin) when R is a finite field such as F_2. Interestingly, Res_{F_2}(lin) is fairly strong, and there is no known nontrivial lower bound for it, but for Res^*_R(lin) (tree-like Res_R(lin)) we know exponential lower bounds for every finite field. For the stronger systems Res_R(PC_d) and Res_R^*(PC_d) for d>1 on finite ring R, there is no known lower bounds. In this talk, we prove a size-width relation for Res_R(PC_d) and Res^*_R(PC_d) for every finite ring R. This relation is proved by a new idea to reduce the problem to the original Ben-Sasson and Wigderson size-width relation for Res and Res^* using extension variables. As a by product, we get the following new lower bounds for every finite field F: 1. We prove a nontrivial lower bound for Res_F(PC_d) for fixed d: a nearly quadratic lower bound for mod q Tseitin formulas (char(F) is not equal to q). 2. We also prove superpolynomial and exponential lower bounds for Res^*_F(PC_d) where d is not too large with respect to n for the following principles: a. mod q Tseitin formulas (char(F) is not equal to q), b. Random k-CNFs.
    • 30.03.20   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Proof-theoretic analysis of some impredicative theories, Part 2
    • Abstract:
    • 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.
    • 23.03.20   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Proof-theoretic analysis of some impredicative theories
    • Abstract:
    • 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.
    • 09.03.20   13:30
    • Susanna F. de Rezende
    • (Institute of Mathematics)
    • Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs, Part 2
    • Abstract:
    • 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.
    • 02.03.20   13:30
    • Susanna F. de Rezende
    • (Institute of Mathematics)
    • Exponential resolution lower bounds for weak pigeonhole principle and perfect matching formulas over sparse graphs
    • Abstract:
    • 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.
    • 24.02.20   13:30
    • Emil Jeřábek
    • (Institute of Mathematics)
    • Proof complexity of logics of bounded branching, Part 2
    • Abstract:
    • 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 logics with bounded branching but unbounded width, such as K4BB_k, S4BB_k, and GLBB_k. In this talk, I will show that while these logics apparently do not have feasible DP as such, they have DP (and more general extension rules) decidable in ZPP^{NP}, and for k=2, even in promise-S_2^P. Moreover, one can also adapt Hrubes's form of "monotone interpolation" to this setting.

      As a consequence, we prove superpolynomial speedup of SF over EF assuming PSPACE \ne NP (possibly exponential under a stronger hypothesis) for all modal logics included in GLBB_2 or S4GrzBB_2, and more generally, for all logics L that, in a certain sense, admit all finite binary trees (with reflexive or irreflexive points as convenient) to appear inside L-frames.

       

    • 03.02.20   13:30
    • Emil Jeřábek
    • (Institute of Mathematics)
    • Proof complexity of logics of bounded branching
    • Abstract:
    • 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 logics with bounded branching but unbounded width, such as K4BB_k, S4BB_k, and GLBB_k. In this talk, I will show that while these logics apparently do not have feasible DP as such, they have DP (and more general extension rules) decidable in ZPP^{NP}, and for k=2, even in promise-S_2^P. Moreover, one can also adapt Hrubes's form of "monotone interpolation" to this setting.

      As a consequence, we prove superpolynomial speedup of SF over EF assuming PSPACE \ne NP (possibly exponential under a stronger hypothesis) for all modal logics included in GLBB_2 or S4GrzBB_2, and more generally, for all logics L that, in a certain sense, admit all finite binary trees (with reflexive or irreflexive points as convenient) to appear inside L-frames.

       

    • 27.01.20   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Systems of second order arithmetic and well-ordering principles, Part 4
    • Abstract:
    • I'll give a brief introduction to systems of second-order arithmetic and the study of their proof-theoretic ordinals. Further the focus will be on well-ordering principles and the approach to ordinal analysis based on functorial ordinal notation systems.
    • 16.12.19   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Systems of second order arithmetic and well-ordering principles, Part 3
    • Abstract:
    • I'll give a brief introduction to systems of second-order arithmetic and the study of their proof-theoretic ordinals. Further the focus will be on well-ordering principles and the approach to ordinal analysis based on functorial ordinal notation systems.
    • 09.12.19   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Systems of second order arithmetic and well-ordering principles, Part 2
    • Abstract:
    • I'll give a brief introduction to systems of second-order arithmetic and the study of their proof-theoretic ordinals. Further the focus will be on well-ordering principles and the approach to ordinal analysis based on functorial ordinal notation systems.
    • 02.12.19   13:30
    • Albert Atserias
    • (Universitat Politčcnica de Catalunya)
    • Automating Resolution Is NP-Hard
    • Abstract:
    • We show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NP-hard. In the parlance of proof complexity, Resolution is not automatizable unless P = NP. Indeed, we show that it is NP-hard to distinguish between formulas that have Resolution refutations of polynomial length and those that do not have subexponential length refutations. This also implies that Resolution is not automatizable in subexponential time or quasi-polynomial time unless NP is included in SUBEXP or QP, respectively. This is joint work with Moritz Müller
    • 25.11.19   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Systems of second order arithmetic and well-ordering principles
    • Abstract:
    • In the present talk I'll give a brief introduction to systems of second-order arithmetic and the study of their proof-theoretic ordinals. Further the focus will be on well-ordering principles and the approach to ordinal analysis based on functorial ordinal notation systems.
    • 18.11.19   13:30
    • Moritz Müller
    • (Universitat Politčcnica de Catalunya)
    • Forcing with partial structures
    • Abstract:
    • Define a finitary combinatorial principle to be a first-order sentence which is valid in the finite but falsifiable in the infinite. We aim to compare the strength of such principles over bounded arithmetics. We distinguish “weak” and “strong” principles based on their behaviour with respect to finite structures that are only partially defined. We show that over relativized T^1_2 “weak” principles do not imply “strong” ones. The proof applies a general forcing method to produce models of relativized T^1_2.
    • 13.11.19   14:00
    • Pavel Pudlák
    • (Institute of Mathematics)
    • The symmetric calculus and monotone interpolation, Part 2
    • Abstract:
    • In this talk I will say a little bit more about the topic that I presented this spring. First I will ask and explain the problem whether the symmetric calculus simulates Frege systems. Then I show how one can strengthen the characterization of the canonical and interpolation pairs. The result can be viewed as monotone interpolation by certain generalizations of monotone Boolean circuits, called bounded depth game schemas. I will also show simulations of point-line game schemas by depth-2 games and vice versa.
    • 11.11.19   13:30
    • Pavel Pudlák
    • (Institute of Mathematics)
    • The symmetric calculus and monotone interpolation
    • Abstract:
    • In this talk I will say a little bit more about the topic that I presented this spring. First I will ask and explain the problem whether the symmetric calculus simulates Frege systems. Then I show how one can strengthen the characterization of the canonical and interpolation pairs. The result can be viewed as monotone interpolation by certain generalizations of monotone Boolean circuits, called bounded depth game schemas. I will also show simulations of point-line game schemas by depth-2 games and vice versa.
    • 04.11.19   13:30
    • Ján Pich
    • (Institute of Mathematics)
    • Why are Proof Complexity Lower Bounds Hard?
    • Abstract:
    • We formalize and study the question of whether there are inherent difficulties to showing lower bounds on propositional proof complexity. We establish the following unconditional result: Propositional proof systems cannot efficiently show that truth tables of random Boolean functions lack polynomial size non-uniform proofs of hardness. Assuming a conjecture of Rudich, propositional proof systems also cannot efficiently show that random k-CNFs of linear density lack polynomial size non-uniform proofs of unsatisfiability. Since the statements in question assert the average-case hardness of standard NP problems (MCSP and 3-SAT respectively) against co-nondeterministic circuits for natural distributions, one interpretation of our result is that propositional proof systems are inherently incapable of efficiently proving strong complexity lower bounds in our formalization. Another interpretation is that an analogue of the Razborov-Rudich 'natural proofs' barrier holds in proof complexity: under reasonable hardness assumptions, there are natural distributions on hard tautologies for which it is infeasible to show proof complexity lower bounds for strong enough proof systems. For the specific case of the Extended Frege (EF) propositional proof system, we show that at least one of the following cases holds: (1) EF has no efficient proofs of superpolynomial circuit lower bound tautologies for any Boolean function or (2) There is an explicit family of tautologies of each length such that under reasonable hardness assumptions, most tautologies are hard but no propositional proof system can efficiently establish hardness for most tautologies in the family. Thus, under reasonable hardness assumptions, either the Circuit Lower Bounds program toward complexity separations cannot be implemented in EF, or there are inherent obstacles to implementing the Cook-Reckhow program for EF. This is a joint work with Rahul Santhanam.
    • 21.10.19   13:30
    • Fedor Pakhomov
    • (Institute of Mathematics)
    • Lengths of proofs for Presburger arithmetic
    • Abstract:
    • Speedups (i.e., differences in the lengths of shortest proofs of the same sentences) between various theories in the language of first-order arithmetic and richer languages is a relatively well-studied phenomenon. There are three typical orders of speedup that occur in natural examples: non-recursive speedups, at most polynomial speedups, and speedups of the order of the super-exponentiation function exp*(0)=1, exp*(x+1)=exp(exp*(x)). In the present talk I will compare this situation to what happens over the language of Presburger arithmetic. We consider theories that are complete in the language of Presburger arithmetic and for them the usual quantifier elimination algorithm guarantees that any formula of the length n has a proof of the length ?exp(exp(exp(P(n)))). This shows that speedups in this setting are at most triple-exponential. An important tool for proving non-polynomial speedups for first-order theories is Friedman-Pudlak finite version of Gödel's second-incompleteness theorem. In this talk I'll show how to adopt it to the case of theories in the language of Presburger arithmetic. This yields the result that if T is a system in the language of PA and T?Con(U), then T has at least exponential speedup over U in the language of Presburger arithmetic. Also I'll show that even very weak theories in the language of Peano arithmetic, for example I??, have at least exponential speedups over the standard axiomatization of Presburger arithmetic.
    • 07.10.19   13:30
    • Jannik Vierling
    • (TU Wien)
    • Clause Set Cycles and Induction
    • Abstract:
    • The subject of automated inductive theorem (AITP) proving focuses on the development of procedures that find proofs by induction and their efficient implementation. AITP is of particular relevance to the formal verification of hardware and software. This subject is characterized by a great variety of approaches that are often only empirically studied and their theoretical properties are therefore often unclear. We aim at studying existing approaches to automated inductive theorem proving by applying results from mathematical logic in order to gain a better understanding of the various methods and to explore the relations between them. In this talk I will present the notion of clause set cycles — an abstraction of the n-clause calculus introduced by Kersani and Peltier in 2013. I will explain this formalism in terms of theories of induction and discuss how the study of this formalism is related to subtheories of Presburger arithmetic.
    • 30.09.19   13:30
    • Raheleh Jalali Keshavarz
    • (Institute of Mathematics)
    • An exponential lower bound for lengths of proofs in substructural logics
    • Abstract:
    • In this talk, we will investigate the lengths of proofs in the usual Gentzen calculus for the substructural logic FL_e. We will present a sequence of tautologies of the system and show any short proof for them implies a short proof for Hrubes' formulas for intuitionistic logic, hence the exponential lower bound follows. We will then conclude that this lower bound also applies to any proof system for a logic between FL_e and IPC.
    • 23.09.19   13:30
    • Nicola Galesi
    • (University of Rome Sapienza)
    • Bounded-depth Frege complexity of Tseitin formulas for all graphs
    • Abstract:

    • We prove that Tseitin formulas Ts(G), for an undirected graph G, require proofs of size 2^{tw(G)^{\Omega(1/d)}} in depth d-Frege systems for d<{K \log n}/{\log \log n}, where tw(G) is the treewidth of G and K a constant. If time will allow, we prove tightness of the lower bound. Namely, that for large enough d, there are depth d-Frege proofs for Ts(G) of size 2^{\tw(G)^{\O(1/d)}} \poly(|Ts(G)|).This is a joint work with Dmitry Itsykson, Artur Riazanov and Anastasia Sofronova

    • 16.09.19   13:30
    • Emil Jeřábek
    • (Institute of Mathematics)
    • Complexity of admissible rules with parameters
    • Abstract:
    • A rule \phi_1, ..., \phi_k / \psi is admissible in a (nonclassical) propositional logic L if the set of L-tautologies is closed under substitution instances of the rule. We are particularly interested in the set-up with parameters (constants), which are required to be preserved by substitutions. In this talk, we shall study basic properties of admissibility with parameters in a class of well-behaved transitive modal logics (i.e., extensions of K4). The main goal is a classification of the computational complexity of admissibility (and the closely related problem of unifiability) with parameters based on semantic properties of logics.
    • 27.05.19   13:00
    • Pavel Pudlák
    • (Mathematical Institute)
    • Propositional proofs and monotone computations
    • Abstract:
    • One of the major discoveries of Stephen Cook is that lower bounds on the lengths of proofs in the propositional calculus can be used to prove independence results. This stimulated research into proving lower bounds for various propositional proof systems. Later it was shown that one can use lower bounds on the size of monotone circuits to prove lower bounds on propositional proofs. New models of monotone computations have been proposed recently that potentially may give us lower bounds for more propositional proof systems that we have so far. In this talk we will survey some results that connect lower bounds on monotone computations in various models with lower bounds on the lengths of proofs in proof systems.
    • 20.05.19   13:00
    • Martin Maxa
    • (Charles University)
    • Feasible incompleteness
    • Abstract:
    • We will present finite counterparts to the well-known theorems that are connected to the foundations of mathematics such as Godel's incompleteness theorems or Lob's theorem. Their finite versions go already beyond famous open problems in computational theory, for example P != NP. Beside the finite version of Godel's second incompleteness theorem, we will present also the finite version of Godel's first incompleteness theorem and we will prove that they are equivalent. We will also state a conjecture that could be called a finite version of Lob's theorem.
    • 13.05.19   13:00
    • Jan Bydžovský
    • (Vienna Technical University)
    • Consistency of circuit lower bounds
    • Abstract:
    • Let T be a strong enough universal theory in language L (containing the symbol '<') and let A(x) be a Sigma^b_2 L-formula. What are the sufficient and possibly useful conditions to derive that 1) T+"A(x) fails for some x" is consistent, 2) T+"A(x) fails for infinitely many x" is consistent, 3) T+"A(x) fails for all but finitely many x" is consistent? I will prove a theorem giving such conditions and use the conditions for 1) and 2) respectively to prove that two formalization of the statement    "for every natural number k, there is a polynomial-time computable Boolean-function which is not computable by circuits of size O(n^k)"   one given by Krajicek and Oliveira in [1] and another one given by Bydzovsky and Muller in [2] are both consistent with the theory PV. Time permitting, I will comment on the possible consistency of the scheme    "for every natural number k, there is a polynomial-time computable Boolean-function which is not computable by circuits of size O(n^k) on all but finitely many lengths"   and on obstacles that appears when one wants to replace PV with S^1_2 or some other non-universal theory. Some preliminary knowledge of the definition of an ultrapower and the statement of the Herbrand theorem are welcome but I will briefly remind those at the beginning.   [1] https://www.karlin.mff.cuni.cz/~krajicek/unprov.pdf [2] https://www.cs.upc.edu/~moritz/ultra_M_30_5.pdf
    • 29.04.19   13:00
    • Fedor Part
    • (JetBrains)
    • A first order theory for constant degree Sum of Squares , Part 2
    • Abstract:
    • The Unique Games Conjecture (UGC) predicts that a certain universal algorithm achieves an optimal approximation for a large class of NP optimization problems. This algorithm can be seen as a proof searching procedure for the constant degree Sum-of-Squares (SoS) proof system, which is automatizable via semidefinite programming. The actual strength of this algorithm and, possibly, the fate of UGC depend on what is derivable in constant degree SoS. In some cases one can argue that the SoS algorithm achieves a bound on an instance by taking some known "ZFC" proof that the optimum meets the bound and trying to redo the proof in constant degree SoS. For example, for the integrality gap instance for LP and SDP hierarchies, that is based on Frankl-Rodl graphs, one can show that the SoS algorithm meets the bound on the size of a maximal independent set, guaranteed by the the Frankl-Rodl theorem, by proving the theorem in constant degree SoS. In this talk, we will present work in progress on the conceptual analysis of the reasoning constant degree SoS is capable of. In particular, we will sketch the definition of a first-order theory, which under propositional translation corresponds to constant degree SoS. This is joint work with Neil Thapen and Iddo Tzameret.
    • 15.04.19   13:00
    • Fedor Part
    • (JetBrains)
    • A first order theory for constant degree Sum of Squares
    • Abstract:
    • The Unique Games Conjecture (UGC) predicts that a certain universal algorithm achieves an optimal approximation for a large class of NP optimization problems. This algorithm can be seen as a proof searching procedure for the constant degree Sum-of-Squares (SoS) proof system, which is automatizable via semidefinite programming. The actual strength of this algorithm and, possibly, the fate of UGC depend on what is derivable in constant degree SoS. In some cases one can argue that the SoS algorithm achieves a bound on an instance by taking some known "ZFC" proof that the optimum meets the bound and trying to redo the proof in constant degree SoS. For example, for the integrality gap instance for LP and SDP hierarchies, that is based on Frankl-Rodl graphs, one can show that the SoS algorithm meets the bound on the size of a maximal independent set, guaranteed by the the Frankl-Rodl theorem, by proving the theorem in constant degree SoS. In this talk, we will present work in progress on the conceptual analysis of the reasoning constant degree SoS is capable of. In particular, we will sketch the definition of a first-order theory, which under propositional translation corresponds to constant degree SoS. This is joint work with Neil Thapen and Iddo Tzameret.
    • 08.04.19   13:00
    • Raheleh Jalali Keshavarz
    • (Institute of Mathematics)
    • An Exponential Lower Bound for Proofs in Focused Calculi
    • Abstract:
    • In her recent paper, Iemhoff introduced a special form of sequent-style rules and axioms, which she called focused, and studied the relationship between the focused proof systems, the systems only consisting of this kind of rules and axioms, and the uniform interpolation of the logic that the system captures. Subsequently, as a negative consequence of this relationship, she excludes almost all super-intuitionistic logics from having these focused proof systems. In this talk, we will strengthen this negative result to show that even in the cases that these systems exist, their proof-length would computationally explode. More precisely, we will first introduce two natural subclasses of focused rules, called PPF and MPF rules. Then, we will introduce some CPC-valid (IPC-valid) sequents with polynomially short tree-like proofs in the usual Hilbert- style proof system, or equivalently LK + Cut, that have exponentially long proofs in the systems only consisting of PPF (MPF) rules.
    • 27.03.19   14:00
    • Neil Thapen
    • (Institute of Mathematics)
    • Polynomial calculus space and resolution width, part II
    • Abstract:
    • Let w(F) be the width needed to refute a CNF F in resolution. It is well known that the space needed to refute F in resolution is lower bounded by w(F), and it has been open whether something similar holds for polynomial calculus (PCR).  We show, by a novel 'forcing' argument, that the space needed to refute F in PCR is lower bounded by the square root of w(F). Joint work with Nicola Galesi and Leszek Kolodziejczyk. ** Please notice the earlier starting time - 13:00 **  
    • 04.03.19   13:00
    • Neil Thapen
    • (Institute of Mathematics)
    • Polynomial calculus space and resolution width
    • Abstract:
    • Let w(F) be the width needed to refute a CNF F in resolution. It is well known that the space needed to refute F in resolution is lower bounded by w(F), and it has been open whether something similar holds for polynomial calculus (PCR).  We show, by a novel 'forcing' argument, that the space needed to refute F in PCR is lower bounded by the square root of w(F). Joint work with Nicola Galesi and Leszek Kolodziejczyk.
    • 25.02.19   14:00
    • Fedor Part
    • (Royal Holloway, University of London)
    • Lower Bounds for Resolution with Linear Equations over a Ring
    • Abstract:
    • The proof system Res(lin_R) is an extension of Resolution in which proof lines are disjunctions of linear equations over a ring R. If R is a finite field GF(p), Res(lin_R) can be viewed as a "minimal" fragment of bounded depth Frege system with counting gates AC^0[p]-Frege (and similarly, for R the integers and the TC^0-Frege), for which no nontrivial lower bound is known. Recent suggested approaches for obtaining lower bounds against Res(lin_GF(2)) refutations include feasible interpolation and combinatorial techniques. In this talk we explore and develop further the combinatorial approach for various rings R. In particular, we prove an exponential-size dag-like Res(lin_F) lower bound for the Subset Sum principle with large coefficients, as well as establish a host of new tree-like lower bounds and separations over different fields. Based on a joint work with Iddo Tzameret.
    • 17.12.18   14:00
    • Neil Thapen
    • (Institute of Mathematics)
    • DRAT proofs without new variables
    • Abstract:
    • The DRAT proof system is used by modern SAT solvers to witness that a CNF is unsatisfiable. The full system allows you to freely introduce new variables, and is as strong as extended resolution. I will discuss some upper and lower bounds on a restricted system, in which you cannot introduce new variables. This is ongoing work with Sam Buss.
    • 10.12.18   14:00
    • Raheleh Jalali Keshavarz
    • (Institute of Mathematics)
    • Semi-analytic rules and uniform interpolation
    • Abstract:
    • In her recent works, Iemhoff introduced a connection between the existence of a terminating sequent calculus of a certain kind and the uniform interpolation property of the super-intuitionistic logic that the calculus captures. In this talk, we will generalize this relationship to also cover the substructural setting on the one hand and a much more powerful class of rules on the other. The resulted relationship then provides a uniform method to establish uniform interpolation property for the logics FL_e, FL_{ew}, CFL_e, CFL_{ew}, IPC, CPC and their K and KD-type modal extensions. More interestingly though, on the negative side, we will show that no extension of FL_e can enjoy a certain natural type of terminating sequent calculus unless it has the uniform interpolation property. It excludes almost all super-intutionistic logics and the logics K4 and S4 from having such a reasonable calculus.
    • 19.11.18   14:00
    • Raheleh Jalali Keshavarz
    • (Institute of Mathematics)
    • Semi-analytic Rules and Craig Interpolation
    • Abstract:
    • In one of her recent works, Iemhoff introduced the notion of a centered axiom and a centered rule as the building blocks for a certain form of sequent calculus which she calls a centered proof system. She then showed how the existence of a terminating centered system implies the uniform interpolation property for the logic that the calculus captures. In this paper we first generalize her centered rules to semi-analytic rules, a dramatically powerful generalization, and then we will show how the semi-analytic calculi consisting of these rules together with our generalization of her centered axioms, lead to the feasible Craig interpolation property. Using this relationship, we first present a uniform method to prove interpolation for different logics from sub-structural logics FL_e, FL_{ec}, FL_{ew} and IPC to their appropriate classical and modal extensions, including the intuitionistic and classical linear logics. Then we will use our theorem negatively, first to show that so many sub-structural logics including $\L_n$, $G_n$, $BL$, $R$ and $RM^e$ and almost all super-intutionistic logics (except at most seven of them) do not have a semi-analytic calculus. To investigate the case that the logic actually has the Craig interpolation property, we will first define a certain specific type of semi-analytic calculus which we call PPC systems and we will then present a sound and complete PPC calculus for classical logic. However, we will show that all such PPC calculi are exponentially slower than the classical Hilbert-style proof system (or equivalently LK+Cut). We will then present a similar exponential lower bound for a certain form of complete PPC calculi, this time for any super-intuitionistic logic.
    • 12.11.18   14:00
    • Ilario Bonacina
    • (Universitat Politčcnica de Catalunya)
    • Clique is Hard on Average for Regular Resolution
    • Abstract:
    • Deciding whether a graph G with n vertices has a k-clique is one of the most basic computational problems on graphs. In this talk we show that certifying k-clique-freeness of Erdos-Renyi random graphs is hard for regular resolution. More precisely we show that, for k
    • 22.10.18   14:00
    • Navid Talebanfard
    • (Institute of Mathematics)
    • Structure in Proof Complexity: The Case of Tseitin and Tree Decompositions
    • Abstract:
    • One of the main difficulties of proving lower bounds in proof complexity is that we cannot (seemingly) make structural assumptions about the proof and thus our argument should work against any conceivable proof (which may not even exist). I will survey a few old results showing that in some cases it is possible to prove structural properties of proofs of specific formulas or minimal proofs of arbitrary formulas. Then I will give a more direct proof of our result with Nicola Galesi and Jacobo Toran showing that the minimum width of Tseitin formulas is the same in general and regular resolution.
    • 24.09.18   14:00
    • Nicola Galesi
    • (Sapienza University of Rome)
    • Resolution and the binary encoding of combinatorial principles
    • Abstract:
    • We investigate the size complexity of proofs in RES(s) -- an extension of Resolution working on s-DNFs instead of clauses -- for families of contradictions given in the unusual binary encoding. A motivation of our work is to approach size lower bounds of refutations in Resolution for families of contradictions in the usual unary encoding. Our main interest is the k-Clique principle, whose Resolution complexity is still unknown. The approach is justified by the observation that for a large class of combinatorial principles short RES(log n) refutations for the binary encoding are obtained from short Resolution refutations of the unary encoding, in particular for the k-Clique principle. In the talk we show a n^{Omega(k)} lower bound for the size of refutations of the binary k-Clique Principle in RES(log log n). This improves a result of Lauria, Pudlák, Rödl and Thapen, who proved the lower bound for Resolution, that is RES(1). Resolution lower bounds for the (unary) k-Clique principle are known only when refutations are either treelike or read-once. The result is part of a larger work investigating the complexity of proofs in RES(s) for binary encodings of combinatorial principles, written jointly with Stefan Dantchev and Barnaby Martin and available at https://arxiv.org/abs/1809.02843
    • 17.09.18   14:00
    • Pavel Hrubes
    • (Institute of Mathematics)
    • An interesting (?) problem equivalent to Continuum Hypothesis
    • Abstract:
    • I will discuss a problem which came up in the context of machine learning, and which ended up being undecidable in ZFC. The flavor is similar to the so-called Axioms of Symmetry of Freiling. Based on a work with B. Shai-David, S. Moran, A. Shpilka, A. Yehudayoff.
    • 04.06.18   14:00
    • Emil Jerabek
    • (Institute of Mathematics)
    • Rigid models of Presburger arithmetic
    • Abstract:
    • While all first-order theories have plenty of models with many automorphisms (e.g., saturated), models with few automorphisms are harder to come by, and their existence varies with the theory. In the extreme case of rigid models (= with no nontrivial automorphism), some theories have no rigid models at all (such as divisible ordered abelian groups), while e.g. Peano arithmetic has many: every model of PA has a rigid elementary end-extension of the same cardinality. In this talk, we will give a complete description of rigid models of Presburger arithmetic Th(Z,+,
    • 28.05.18   14:00
    • Arnold Beckmann
    • (Swansea University)
    • Hyper Natural Deduction
    • Abstract:
    • We introduce Hyper Natural Deduction as an extension of Gentzen's Natural Deduction system by communication like rules. The motivation is to obtain a natural deduction like system which is equivalent to Avron's Hypersequent Calculus for Goedel-Dummett Logic, and which permits natural conversion rules for normalisation as an extension of the well-known conversion rules for Natural Deduction. The ultimate goal of this project is to establish a Curry-Howard correspondence to some (yet to be found) model of parallel computation. An additional aim is to shed further light on Avron's suggestion [in A. Avron: Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artificial Intelligence, 4(1991), 225-248] that a hypersequent can be thought of as a multiprocess. This is joint work with Norbert Preining, supported by a Royal Society Daiwa Anglo-Japanese Foundation International Exchanges Award #IE130639.
    • 21.05.18   14:00
    • Jan Krajíček
    • (Charles University)
    • Proof Complexity Catch 22
    • Abstract:
    • I will present some views on the structure of proof complexity and possible research directions, illustrating them by some theorems and problems.
    • 23.04.18   14:00
    • Pavel Pudlák
    • (IM CAS)
    • A proof system polynomially equivalent to bounded depth Frege, part 3
    • Abstract:
    • In the 3rd part we will show how to reduce the disjoint NP pairs of the games we introduced in the 2nd part to the canonical pairs of bounded depth Frege systems. To this end we will use the proof system equivalent to bounded depth Frege introduced in the 1st part. Given a refutation of A(x) & B(y) in this system, we will define a game and show that a satisfying assignment for A(x) (resp. B(y)) can be transformed into a positional winning strategy for Player I (resp. II).
    • 16.04.18   14:00
    • Lorenzo Carlucci
    • (Sapienza University of Rome)
    • On the strength of some natural restrictions of Hindman's Theorem
    • Abstract:
    • Hindman's Finite Sums Theorem states that any finite coloring of the positive integers admits an infinite sequence such that any sum of finitely many distinct elements from that sequence has the same color. Some interesting open problems exist related to this theorem both in Combinatorics and in Computable or Reverse Mathematics. The best lower and upper bound known locate the strength of the theorem between the Halting Set and Arithmetical Truth, leaving a huge gap in-between. These bounds, due to Blass, Hirst and Simpson, have not been improved since the Eighties. Hindman, Leader and Strauss asked in 2003 whether there exists a proof of the restriction of Hindman's Theorem to sums of one or two elements that does not prove the full theorem. The question is still open and can be made precise in the context of Computable or Reverse Mathematics. We report on recent results on the strength of restrictions of Hindman's Theorem. For example we show that the known lower bound for the full theorem already holds for its restrictions to sums of one or two elements. We furthermore discuss some "weak yet strong" variants admitting both a significant lower bound and a much lower upper bound than the upper bound known on the full theorem. We also discuss connections with the Increasing Polarized Ramsey's Theorem and highlight the role of a sparsity condition on the solution set, which we call partness. Part of the work presented is joint with Kolodziejczyk, Lepore and Zdanowski.
    • 09.04.18   14:00
    • Albert Atserias
    • (Universitat Politčcnica de Catalunya)
    • Locally consistent equations, the structure of solution spaces, and quantum information games
    • Abstract:
    • I will start with a (partial) survey of some recent results on the proof complexity of the graph isomorphism problem with a surprising outcome: for certifying that two graphs are non isomorphic, Polynomial Calculus over the reals, Sherali-Adams, and Sums-of-Squares proofs are equally powerful (or weak). I will try to convey why I think this outcome is surprising. Then I will link this topic to the area of perfect strategies in quantum information games. We show that there are graphs that are quantum isomorphic but not classically isomorphic, and a complete characterization of the Boolean constraint languages that admit instances that are quantum but not classically realizable.
    • 26.03.18   14:00
    • Pavel Pudlák
    • (IM CAS)
    • A proof system polynomially equivalent to bounded depth Frege, part 2
    • Abstract:
    • Our proof system is based on deep inferences rules. The only nonstructural rules of the system are resolution and the rule dual to resolution. The system is inspired by the proof system of Skelley and Thapen that they used to characterize provably total functions in Bounded Arithmetic. Our aim is to use the system to find a combinatorial characterization of canonical pairs of Bounded depth Frege systems.
    • 19.03.18   14:00
    • Pavel Pudlák
    • (IM CAS)
    • A proof system polynomially equivalent to bounded depth Frege
    • Abstract:
    • Our proof system is based on deep inferences rules. The only nonstructural rules of the system are resolution and the rule dual to resolution. The system is inspired by the proof system of Skelley and Thapen that they used to characterize provably total functions in Bounded Arithmetic. Our aim is to use the system to find a combinatorial characterization of canonical pairs of Bounded depth Frege systems.
    • 12.03.18   14:00
    • Amir Tabatabai
    • (AVCR and Charles University)
    • Proof mining in bounded arithmetic, part 3
    • Abstract:
    • A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this talk we will explain the basics of the theory of computational flows and how they make a sound and complete interpretation for bounded theories of arithmetic. This property helps us to decompose a first order arithmetical proof into a sequence of computational reductions by which we can extract the computational content of the low complexity statements in some bounded theories of arithmetic such as I Delta_0, T^k_n, I Delta_0+EXP and PRA.
    • 05.03.18   14:00
    • Amir Tabatabai
    • (AVCR and Charles University)
    • Proof mining in bounded arithmetic, part 2
    • Abstract:
    • A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this talk we will explain the basics of the theory of computational flows and how they make a sound and complete interpretation for bounded theories of arithmetic. This property helps us to decompose a first order arithmetical proof into a sequence of computational reductions by which we can extract the computational content of the low complexity statements in some bounded theories of arithmetic such as I Delta_0, T^k_n, I Delta_0+EXP and PRA.
    • 19.02.18   14:00
    • Amir Tabatabai
    • (AVCR and Charles University)
    • Proof mining in bounded arithmetic
    • Abstract:
    • A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this talk we will explain the basics of the theory of computational flows and how they make a sound and complete interpretation for bounded theories of arithmetic. This property helps us to decompose a first order arithmetical proof into a sequence of computational reductions by which we can extract the computational content of the low complexity statements in some bounded theories of arithmetic such as I Delta_0, T^k_n, I Delta_0+EXP and PRA.
    • 05.02.18   14:00
    • Neil Thapen
    • (Institute of Mathematics)
    • Semantic cutting planes with small coefficients
    • Abstract:
    • Cutting planes (CP) is a proof system whose lines are linear integral inequalities. It was shown recently by Filmus, Hrubes and Lauria that a semantic version of CP (that is, allowing any sound rule) is exponentially stronger than usual CP. I will discuss some upper bounds on the refutational and implicational completeness of CP, and show from these that semantic CP can be simulated by CP, if we only consider semantic refutations with very small coefficients. Joint work with Massimo Lauria.
    • 15.01.18   14:00
    • Michael Benedikt
    • (University of Oxford)
    • Interpolation for Query Reformulation
    • Abstract:
    • In this talk I will explain query reformulation problems - given a formula Q and a background theory T, the goal is to translate Q, either into another formula or a direct procedural implementation, such that the translation is equivalent to Q according to T, and such that the translation satisfies additional "interface restrictions" - e.g. restrictions on the vocabulary. I will review the approach to solving these problems via interpolation which has been investigated over the last few years, presenting the properties of a proof system and interpolation algorithm we might desire for the application to reformulation. I will then look at some proof methods and associated interpolation algorithms that have been proposed in the past -- via tableaux, resolution, and tree-automata, with some tentative remarks about how these stack up against the requirements.
    • 04.12.17   14:00
    • Wieslaw Kubis
    • (Institute of Mathematics)
    • Weak Fraisse categories and their limits
    • Abstract:
    • I will survey recent developments in the theory of limits of weak amalgamation classes, in the language of category theory, with examples in model theory.
    • 27.11.17   14:00
    • Neil Thapen
    • (Institute of Mathematics)
    • Bounded arithmetic does not collapse to approximate counting
    • Abstract:
    • We adapt the "fixing lemma", a simple switching lemma used recently to show lower bounds for random resolution, to show that Jerabek's theory of approximate counting does not prove the CPLS principle. This settles an open problem by showing that bounded arithmetic is strictly stronger than approximate counting, if we compare the strength of theories by looking at their \forall \Sigma^b_1 consequences.
    • 20.11.17   14:00
    • Jonathan Verner
    • (Charles University)
    • A Ramsey theorem for Metric spaces
    • Abstract:
    • We use the following variation of the standard Hungarian arrow notation which takes into account additional structure: Let K be a class of structures and kappa,lambda,nu be cardinals. The arrow kappa ->_K (lambda)^1_mu, is shorthand for the statement that for every X in K of size lambda there is a Y in K of size kappa such that for any partition of Y into mu-many pieces one of the pieces contains an isomorphic copy of X. In the talk we will investigate this arrow in the case where K is the class of bounded metric spaces with isomorphic copies being scaled copies. We extend previous work on these questions (e.g. Komjath (1987), Nesetril(2006), Komjath (1987b), Weiss (1990)).
    • 13.11.17   14:00
    • Pavel Pudlák
    • (Institute of Mathematics)
    • Incompleteness in the finite domain, Part 2
    • Abstract:
    • The title is just a new name for what I used to call "feasible incompleteness". In this lecture I will recall some basic old results and mention some new developments in this field.
    • 16.10.17   14:00
    • Pavel Pudlák
    • (Institute of Mathematics)
    • Incompleteness in the finite domain
    • Abstract:
    • The title is just a new name for what I used to call "feasible incompleteness". In this lecture I will recall some basic old results and mention some new developments in this field.
    • 09.10.17   14:00
    • Igor Oliveira
    • (Charles University)
    • Unprovability of circuit upper bounds in Cook's theory PV
    • Abstract:
    • We establish unconditionally that for every integer k>=1 there is a language L in P such that it is consistent with Cook's theory PV that L is not in Size(n^k). Our argument is non-constructive and does not provide an explicit description of this language.
    • 19.04.17   13:30
    • Kateřina Trlifajová
    • (Faculty of Information Technology, Czech Technical University, Prague)
    • Is Bolzano's theory of infinity consistent?
    • Abstract:
    • Bolzano's theory of infinity which is mostly contained in his Paradoxes of Infinity from 1848 is usually considered as a step in a wrong direction. Both Bolzano and Cantor defended actual infinity in mathematics. But while Cantor based his measuring of infinite sets on the one-to-one correspodence Bolzano based it on the part-whole principles: the whole is greater than its part. We'll demonstrate there are several interpretations of Bolzano's theory. Some of them are based on the framework of non-standard analysis. An open question remains: is there a meaningful interpretation without ultrafilters? Consequently, was Cantor's theory of infinite numbers inevitable?
    • 10.04.17   13:30
    • Petr Glivicky
    • (University of Economics & Charles University)
    • Nonstandard methods in Ramsey-type combinatorics, part II
    • Abstract:
    • Recently, nonstandard methods have been successfully applied in many areas of combinatorics. The nonstandard methodology provides an extension of the universe of mathematics by new ideal (nonstandard) objects such as "an infinitely large natural number", "an infinitely small neighborhood of a point", and many more. The rich structure of relations between the original (standard) and the new (nonstandard) objects enables the standard objects and their standard properties to be described and studied by means of nonstandard concepts. It turns out that this nonstandard description is in many cases more elegant and the nonstandard proofs clearer and shorter than their standard alternatives. In this series of two talks, I outline a nonstandard approach to Ramsey-type combinatorics. I prove two nonstandard Ramsey-type principles of the following common form (vaguely): "If, in a coloring of finite subsets of natural numbers, certain nonstandard object (a witness) has a color C, then there is an infinite subset of natural numbers homogeneously having the color C." As applications of these principles I give very short and simple nonstandard proofs of several well-known Ramsey-type combinatorial theorems, including Ramsey's, Hilbert's and Hindmann's theorems. This is joint work with Josef Mlček. In this second talk, I will build up a theory of the infinitely iterated nonstandard extension of the set of natural numbers and I will use it to prove the combinatorial results mentioned above.
    • 31.03.17   13:30
    • Petr Glivicky
    • (University of Economics & Charles University)
    • Nonstandard methods in Ramsey-type combinatorics, part I
    • Abstract:
    • Recently, nonstandard methods have been successfully applied in many areas of combinatorics. The nonstandard methodology provides an extension of the universe of mathematics by new ideal (nonstandard) objects such as "an infinitely large natural number", "an infinitely small neighborhood of a point", and many more. The rich structure of relations between the original (standard) and the new (nonstandard) objects enables the standard objects and their standard properties to be described and studied by means of nonstandard concepts. It turns out that this nonstandard description is in many cases more elegant and the nonstandard proofs clearer and shorter than their standard alternatives. In this series of two talks, I outline a nonstandard approach to Ramsey-type combinatorics. I prove two nonstandard Ramsey-type principles of the following common form (vaguely): "If, in a coloring of finite subsets of natural numbers, certain nonstandard object (a witness) has a color C, then there is an infinite subset of natural numbers homogeneously having the color C." As applications of these principles I give very short and simple nonstandard proofs of several well-known Ramsey-type combinatorial theorems, including Ramsey's, Hilbert's and Hindmann's theorems. This is joint work with Josef Mlček. In this first talk, I will give an "Introduction to nonstandard methods for standard mathematicians". I will build up all the necessary nonstandard concepts and methods from scratch and show some simple yet rather impressive applications and examples. Only the knowledge of very elementary set theory and logic will be assumed.
    • 13.03.17   13:30
    • Nicola Galesi
    • (Sapienza University Rome)
    • Refuting random 3-CNFs using polynomials requires large proof space
    • Abstract:
    • A main tool in proving (space) lower bounds? for refuting random k-CNF formulas is the well-known expansion property of incidence graph of the formula. Nevertheless, for k=3 the expansion is no longer sufficient to prove proof space lower bounds for Polynomial Calculus (PCR), a proof system working with polynomials. In the talk we first give an overview of a general technique for proving prove space lower bounds for random CNFs. Then we present a variant of Hall's theorem stating that in bipartite graphs G=(L, R) with left-degree at most 3, L can be covered by certain families of disjoint paths, provided that L expands in R by a factor of (2 ? ?), for ?
    • 06.03.17   13:30
    • Pavel Hrubeš
    • (Institute of Mathematics)
    • Monotone interpolation and Cutting Planes
    • Abstract:
    • We prove new lower bounds on the sizes of proofs in the Cutting Plane proof system, using a concept we call an unsatisfiability certificate. This approach is, essentially, equivalent to the well-known feasible interpolation method, but is applicable to CNF formulas that do not seem suitable for interpolation. Specifically, we prove exponential lower bounds for random (log n)-CNFs, and for the Weak Bit Pigeon Hole Principle.
    • 27.02.17   13:30
    • Dmitry Sokolov
    • (PDMI, Russian Academy of Sciences)
    • On OBDD based proof systems that dynamically change order of variables
    • Abstract:
    • In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deducing of identically false OBDD from OBDDs representing clauses of the initial formula. All OBDDs in such proofs have the same order of variables. In this talk we consider OBDD based proof systems that additionally contain a rule that allows to change the order in OBDDs. At first we consider a proof system OBDD(\land, reordering) that uses the conjunction (join) rule and the rule that allows to change the order. We exponentially separates this proof system from OBDD(\land)-proof system that uses only conjunction rule. We prove two exponential lower bounds on the size of OBDD(\land, reordering)-refutation of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for OBDD(\land)-proofs and the second one extends the result of Tveretina et. al from OBDD(\land) to OBDD(\land, reordering). Joint work with Dmitry Itsykson, Alexander Knop and Andrey Romashchenko.
    • 30.01.17   13:30
    • Dmitry Sokolov
    • (Russian Academy of Sciences)
    • Dag-like communication
    • Abstract:
    • In this talk we consider a model of dag-like communication complexity (instead of classical one where protocols correspond to trees). We prove an analogue of Karchmer-Wigderson Theorem for this model and boolean circuits. We also consider a relation between this model and communication PLS games proposed by Razborov in 1995 and simplify the proof of Razborov's analogue of Karchmer-Wigderson Theorem for PLS games. We also consider a dag-like analogue of real-valued communication protocols and adapt a lower bound technique for monotone real circuits to prove a lower bound for these protocols. We use real-valued dag-like communication protocols to generalize the ideas of "feasible interpolation" technique, which helps us to prove a lower bound on the Cutting Plane proof system (CP) and adopt it to "random CP" by using recent result of Krajicek. Our notion of dag-like communication games allows us to use a Raz-McKenzie transformation from Goos and Pitassi paper, which yields a lower bound on the real monotone circuit size for the CSPSAT problem.
    • 16.01.17   13:30
    • Massimo Lauria
    • (Universitat Politčcnica de Catalunya)
    • Circular (Yet Sound) Proofs
    • Abstract:
    • We introduce a new way of representing proofs in rule-based proof systems that generalizes tree-like and dag-like proofs. In the new definition proofs are represented in the form of directed graphs of derived formulas, in which cycles are allowed as long as every formula is derived at least as many times as it is used as a hypothesis of a rule. We call such proofs circular. We show that for all rule-based proofs systems, circular proofs are sound and, obviously, complete. For Frege systems, in which arbitrary propositional formulas are allowed in the proofs, we show that circular proofs can be converted into tree-like ones with at most polynomial overhead. The proof goes by a translation into an arithmetic statement and is thus indirect. For resolution, where the only allowed formulas are clauses, the arithmetic statement becomes a proof in the Sherali-Adams proof system that preserves both length/number-of-monomials and width/degree, up to small factors. Surprisingly, a reverse translation also holds: every Sherali-Adams refutation of a CNF formula translates into a circular resolution refutation of comparable length/number-of-monomials and width/degree. As corollaries we get: 1) polynomial-time algorithms that find circular resolution refutations of constant width, 2) examples showing that circular resolution proofs are sometimes exponentially more succinct than dag-like resolution proofs, and 3) exponentially hard examples for circular resolution.
    • 09.01.17   13:30
    • Wieslaw Kubis
    • (Institute of Mathematics)
    • The weak amalgamation property and infinite games, part 2
    • Abstract:
    • I will present a generalization of the Fraisse theory of universal homogeneous structures, where the crucial amalgamation property is replaced by a much weaker condition. I will characterize the new Fraisse limits by the existence of a winning strategy in a very natural game in which two players alternately choose finitely generated structures, building an infinite chain. One of the players wins if the union of this chain is isomorphic to a specific, chosen in advance, structure. This is joint work with A. Krawczyk (University of Warsaw).
    • 05.12.16   13:30
    • Wieslaw Kubis
    • (Institute of Mathematics)
    • The weak amalgamation property and infinite games
    • Abstract:
    • I will present a generalization of the Fraisse theory of universal homogeneous structures, where the crucial amalgamation property is replaced by a much weaker condition. I will characterize the new Fraisse limits by the existence of a winning strategy in a very natural game in which two players alternately choose finitely generated structures, building an infinite chain. One of the players wins if the union of this chain is isomorphic to a specific, chosen in advance, structure. This is joint work with A. Krawczyk (University of Warsaw).
    • 28.11.16   13:30
    • Stefan Dantchev
    • (Durham University)
    • Tseitin contradictions on weak expanders
    • Abstract:
    • Tseitin contradictions, which are certain inconsistent linear systems modulo two, have the distinction of being the earliest formulae shown to be provably hard for a propositional proof system, regular resolution, back in 1986. Since then, stronger results have been proven, culminating in two incomparable lower bounds for bounded-depth Frege proofs of the Tseitin contradictions based on expander graphs. We generalise both lower bounds to the case of “weak expanders”, i.e. (families of) graphs that are not expanders but are of unbounded tree-width. We first look at Tseitin formulae on square grids and reduce them to both bijective pigeon-hole principle and Tseitin formulae on expanders. This implies, via a standard result from (effective) graph theory, that both lower bounds above, known in case of expanders, also hold for weak expanders. Since our reductions do not apply to resolution (and it is unlikely that there is a reduction that does), we provide a different proof of a tight lower bound in this case. The argument is a randomised adversary argument against a resolution refutation. Finally, we discuss how one might prove similar lower bounds for matching formulae based on weak expanders.
    • 21.11.16   13:30
    • Michal Garlík
    • (Institute of Mathematics)
    • Some subsystems of constant depth Frege with parity, part 2
    • Abstract:
    • I shall discuss three families of subsystems of AC^0[2]-Frege for which exponential lower bounds on proof size are known. The strongest of these families of subsystems is a version of systems introduced by Krajíček which we call PK^{c}_{d}(\oplus). Lines in a PK^{c}_{d}(\oplus)-proof are cedents in which all formulas have depth at most d, parity connectives can only appear as the outermost connectives in formulas, and all but c formulas contain no parity connective at all. Comparing our systems with respect to formulas in De Morgan language, we show e.g. that treelike PK^{c}_{d}(\oplus) is quasipolynomially simulated by constant-depth Frege with parity axioms and that PK^{c}_{d}(\oplus) does not polynomially simulate AC^0[2]-Frege. Joint work with Leszek Ko?odziejczyk.
    • 14.11.16   13:30
    • Michal Garlík
    • (Institute of Mathematics)
    • Some subsystems of constant depth Frege with parity
    • Abstract:
    • I shall discuss three families of subsystems of AC^0[2]-Frege for which exponential lower bounds on proof size are known. The strongest of these families of subsystems is a version of systems introduced by Krajíček which we call PK^{c}_{d}(\oplus). Lines in a PK^{c}_{d}(\oplus)-proof are cedents in which all formulas have depth at most d, parity connectives can only appear as the outermost connectives in formulas, and all but c formulas contain no parity connective at all. Comparing our systems with respect to formulas in De Morgan language, we show e.g. that treelike PK^{c}_{d}(\oplus) is quasipolynomially simulated by constant-depth Frege with parity axioms and that PK^{c}_{d}(\oplus) does not polynomially simulate AC^0[2]-Frege. Joint work with Leszek Ko?odziejczyk.
    • 07.11.16   13:30
    • Pavel Pudlák
    • (Institute of Mathematics)
    • Random resolution refutations, part 2
    • Abstract:
    • The definition of random resolution attempts to capture the notion of a resolution refutation that may make mistakes but is correct most of the time. I will prove some upper and lower bounds, and discuss a separation between polylogarithmic width random resolution and quasipolynomial size resolution, which is connected to a question in bounded arithmetic. This is a continuation of Neil Thapen's talk on October 10th.
    • 31.10.16   13:30
    • Neil Thapen
    • (Institute of Mathematics)
    • Random resolution refutations
    • Abstract:
    • The definition of random resolution attempts to capture the notion of a resolution refutation that may make mistakes but is correct most of the time. I will prove some upper and lower bounds, and discuss a separation between polylogarithmic width random resolution and quasipolynomial size resolution, which is connected to a question in bounded arithmetic. Joint work with Pavel Pudlák.
    • 10.10.16   13:30
    • Joost Joosten
    • (Universitat de Barcelona)
    • Turing Taylor Expansions of Arithmetical Theories
    • Abstract:
    • Analytic functions can be endowed with a Taylor expansion around any given point in its domain. In a sense, one can project an analytical function f on a basis of orthogonal monomials x^n and f can be written as some sum of such monomials. We shall see that for a large class of arithmetical theories T something similar holds. The monomials are replaced by Turing progressions over Elementary Arithmetic and natural theories T can be expressed as the union of these monomials. However, we only have orthogonality of the monomials on certain intervals. This is not a problem since we can show that any union of monomials is provably equivalent to one in such an interval. These intervals are seen to live in a well-known structure: Ignatiev's universal modal model of the closed fragment of Japaridze's polymodal provability logic GLP. This is very nice and thus, points in Ignatiev's model can be interpreted in various ways: Turing Taylor expansions of natural arithmetical theories, ordinals, natural sequences of iterating end-logarithms on ordinals, and of course, modal formulae. This cross-interpretability powers applicability of these polymodal provability logics which we shall discuss as well.
    • 13.06.16   13:30
    • Kristina Hostáková
    • (Charles University)
    • The BSS model and hard to invert real functions
    • Abstract:
    • Real numbers are usually represented by various discrete objects such as floating points or partial decimal expansions. This is mainly because the classical computability theory relates to computers which work with discrete data. Nevertheless, for theoretical purposes it is interesting to look at models of computation that deal with real numbers as with objects of unit size. A very natural such model was suggested by Blum, Shub and Smale in 1989. In this talk, I will describe BSS machines over real numbers and their relationship with classical Turing machines. In addition, I will discuss the question whether there are real functions of one real variable that are easier to compute than to invert by a BSS machine.
    • 30.05.16   13:30
    • Šárka Stejskalová
    • (Faculty of Arts, Charles University)
    • Woodin solution(s) of CH
    • Abstract:
    • The continuum hypothesis says that any subset of the real numbers is at most countable or has the same size as the set of all real numbers. By the results of Godel and Cohen this hypothesis is independent over ZFC if ZFC is consistent. In the talk we focus on the atempt of Woodin to solve CH in the sense of finding a natural theory extending ZFC which decides CH. 
    • 09.05.16   13:30
    • Jan Pich
    • (University of Leeds)
    • Gentzen and Frege systems for QBF
    • Abstract:
    • Recently Beyersdorff, Bonacina, and Chew [1] introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. We provide a comprehensive analysis of the new extended Frege systems from [1], denoted EF+$\forall$-red, which is a natural extension of classical extended Frege EF. Our main results are the following: Firstly, we prove that the standard Gentzen-style system $G_1^*$ p-simulates EF+$\forall$-red and that $G_1^*$ is strictly stronger under standard complexity-theoretic hardness assumptions. Secondly, we show a correspondence of EF+$\forall$-red to bounded arithmetic: EF+$\forall$-red can be seen as a nonuniform propositional version of intuitionistic $S^1_2$. Specifically, intuitionistic $S^1_2$ proofs of arbitrary statements in prenex form translate to polynomial-size EF+$\forall$-red proofs, and EF+$\forall$-red is in a sense the weakest system with this property. Finally, we show that superpolynomial lower bounds for EF+$\forall$-red would imply either $PSPACE \notin P/poly$ or superpolynomial lower bounds for classical EF, and in fact the converse implication holds as well. Therefore, the system EF+$\forall$-red naturally unites the central problems from circuit and proof complexity. Technically, our results rest on a formalized strategy extraction theorem for EF+$\forall$-red akin to witnessing in intuitionistic $S^1_2$ and a normal form for EF+$\forall$-red proofs.
    • 25.04.16   13:30
    • Martin Escardo
    • (University of Birmingham)
    • Univalent Type Theory
    • Abstract:
    • I will try to explain Voevodsky's univalence axiom as rigorously as I can in the given amount of time. This requires an explanation of Martin-L?f type theory. In particular, Martin-L?f's identity types and universes. Voevodsky's univalence axiom postulates a property of the identity types of universes in Martin-L?f type theory, with a model in homotopy theory.
    • 18.04.16   13:30
    • Arnold Beckmann
    • (Swansea University)
    • Provably total NP search problems in strong theories
    • Abstract:
    • The class of total NP search problems has been identified by Megiddo and Papadimitriou in the beginning of the 1990ies, who denoted this class TFNP. Total NP search problems whose totality can be proven within a mathematical theory, denoted provably total NP search problems, play an important role in the study of Bounded Arithmetic theories and related questions. In this talk, I will present characterisations of the provably total NP search problems of strong theories like Peano Arithmetic, and a general research programme related to this.
    • 11.04.16   13:30
    • Amir Tabatabai
    • (Institute of Mathematics)
    • Provability Interpretation of Propositional and Modal Logics, Part 2
    • Abstract:
    • In 1933, Godel introduced a proof interpretation for propositional intuitionistic logic (IPC). The idea was translating IPC into another calculus (S4) which is a formalization of the concept of intuitive provability. Unfortunately, this approach does not introduce any kind of concrete proof interpretations. In fact, Godel himself showed that any naive interpretation would contradict with his second incompleteness theorem. After Godel, finding a concrete proof interpretation for S4 has been an open problem for years and leads to different fields like provability logics and logic of proofs. In this talk, we intend to introduce a framework for concrete interpretations which leads to a generalization of Solovay's arithmetical interpretation and we will show that these natural interpretations capture different modal logics like K4, KD4, GL and S4. Moreover, we will show that there is not any provability interpretation for S5 as we expected from our informal interpretation of the provability predicate. In addition, we will use these results to propose a class of provability interpretations for propositional logics like Basic and Intuitionistic logics and also to show that classical logic does not admit any provability interpretation.
    • 08.04.16   13:30
    • Amir Tabatabai
    • (Institute of Mathematics)
    • Provability Interpretation of Propositional and Modal Logics
    • Abstract:
    • In 1933, Godel introduced a proof interpretation for propositional intuitionistic logic (IPC). The idea was translating IPC into another calculus (S4) which is a formalization of the concept of intuitive provability. Unfortunately, this approach does not introduce any kind of concrete proof interpretations. In fact, Godel himself showed that any naive interpretation would contradict with his second incompleteness theorem. After Godel, finding a concrete proof interpretation for S4 has been an open problem for years and leads to different fields like provability logics and logic of proofs. In this talk, we intend to introduce a framework for concrete interpretations which leads to a generalization of Solovay's arithmetical interpretation and we will show that these natural interpretations capture different modal logics like K4, KD4, GL and S4. Moreover, we will show that there is not any provability interpretation for S5 as we expected from our informal interpretation of the provability predicate. In addition, we will use these results to propose a class of provability interpretations for propositional logics like Basic and Intuitionistic logics and also to show that classical logic does not admit any provability interpretation.
    • 04.04.16   13:30
    • Yiannis N. Moschovakis
    • (UCLA and University of Athens)
    • Intrinsic complexities
    • Abstract:
    • Sample result (without the precise definitions): Proposition. For every first order structure M = (U_M,c_1,...,R_1,..., f_1,...) and every n-ary relation R(x) on the universe U_M of M, there is a function C_R : U_M^n --> {0,1,..., infty} with the following properties: (1) If C_R(x) = 0 for some tuple x of distinct elements, then R is constant on U_M^n. (2) If \alpha is any (deterministic or non-deterministic) algorithm which decides R from the primitives of M, then for every x, C_R(x)
    • 08.02.16   13:30
    • Anna Horská
    • (Institute of Mathematics)
    • Gentzen's cut elimination strategy and Tait's cut elimination strategy in propositional sequent calculus
    • Abstract:
    • Nowadays, we usually eliminate cuts by decreasing the cut-rank of the derivation (Tait's strategy). That is, a cut with the greatest complexity is chosen such that there are only smaller cuts above it and this one is then decomposed into smaller cuts. Gentzen applies another strategy in his article of 1935. He eliminates the highest cuts, i.e., cuts that there are no other cuts above them. Hence, this procedure does not pay attention to the complexity of the chosen cut. The main property of cut elimination that we are interested in is the growth of the height of the derivation during the elimination, especially we want to know the height of the cut-free derivation. I want to show that both strategies mentioned above give us the same cut-free derivation in propositional logic. Not only is the height of the cut-free derivations the same, but they also have the same structure. I will define a procedure for eliminating a single cut (according to Buss) which makes global changes to a derivation. Then, I use Church-Rosser property to obtain that cut-free derivations are unique, when the only difference during the elimination is the way we choose the next cut to eliminate.
    • 11.01.16   13:30
    • Raheleh Jalali
    • (Mathematical Institute)
    • No Feasible Interpolation for TC^0-Frege Proofs
    • Abstract:
    • This is a paper by M.L.Bonet, T.Pitassi and R.Raz from 1997. The interpolation method has been one of the main tools for proving lower bounds for propositional proof systems. Loosely speaking, if one can prove that a particular proof system has the feasible interpolation property, then a generic reduction can (usually) be applied to prove lower bounds for the proof system, sometimes assuming a (usually modest) complexity-theoretic assumption. In this paper, we show that this method cannot be used to obtain lower bounds for Frege systems, or even for TC^0-Frege systems. More specifically, we show that unless factoring is feasible, neither Frege nor TC^0-Frege has the feasible interpolation property. In order to carry out our argument, we show how to carry out proofs of many elementary axioms/theorems of arithmetic in polynomial-size TC^0-Frege. In particular, we show how to carry out the proof for the Chinese Remainder Theorem, which may be of independent interest. As a corollary, we obtain that TC^0-Frege as well as any proof system that polynomially simulates it, is not automatizable (under a hardness assumption).
    • 04.01.16   13:30
    • Neil Thapen
    • (Institute of Mathematics)
    • Feasible set theory, part 2
    • Abstract:
    • The Cobham recursive set functions (CRSF) generalize the polynomial time functions to arbitrary sets. We define a weak fragment of Kripke-Platek set theory analogous to Buss's S^1_2 and prove, with some caveats, that the CRSF functions are exactly the provably recursive functions of this theory. Joint work with Arnold Beckmann, Sam Buss, Sy Friedman and Moritz Mueller.
    • 14.12.15   13:30
    • Neil Thapen
    • (Institute of Mathematics)
    • Feasible set theory
    • Abstract:
    • The Cobham recursive set functions (CRSF) generalize the polynomial time functions to arbitrary sets. We define a weak fragment of Kripke-Platek set theory analogous to Buss's S^1_2 and prove, with some caveats, that the CRSF functions are exactly the provably recursive functions of this theory. Joint work with Arnold Beckmann, Sam Buss, Sy Friedman and Moritz Mueller.
    • 07.12.15   13:30
    • Emil Jeřábek
    • (Institute of Mathematics)
    • Proof complexity of intuitionistic implicational formulas, Part 2
    • Abstract:
    • We study implicational formulas in the context of proof complexity of intuitionistic logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions. In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrubes [1], generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jerabek [2], can be realized by implicational tautologies. [1] P. Hrubes, A lower bound for intuitionistic logic, Annals of Pure and Applied Logic 146 (2007), 72--90. [2] E. Jerabek, Substitution Frege and extended Frege proof systems in non-classical logics, Annals of Pure and Applied Logic 159 (2009), 1--48.
    • 30.11.15   13:30
    • Emil Jeřábek
    • (Institute of Mathematics)
    • Proof complexity of intuitionistic implicational formulas
    • Abstract:
    • We study implicational formulas in the context of proof complexity of intuitionistic logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions. In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrubes [1], generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jerabek [2], can be realized by implicational tautologies. [1] P. Hrubes, A lower bound for intuitionistic logic, Annals of Pure and Applied Logic 146 (2007), 72--90. [2] E. Jerabek, Substitution Frege and extended Frege proof systems in non-classical logics, Annals of Pure and Applied Logic 159 (2009), 1--48.
    • 23.11.15   13:30
    • Raheleh Jalali
    • (Institute of Mathematics)
    • Some consequences of cryptographical conjectures for S^1_2 and EF
    • Abstract:
    • We present a paper by J. Krajicek and P. Pudlak from 1995. We show that if the RSA cryptosystem is secure, then \Delta^b_1 interpolation does not hold for S^1_2. Furthermore, we show that if factoring and discrete logarithm are in P/poly, then a certain \Pi^b_1 extension of S^1_2 does not admit \Delta^b_1 interpolation. At last, as a corollary we obtain that the feasible interpolation theorem fails for Extended Frege proof systems, if RSA is secure.
    • 02.11.15   13:30
    • Jan Krajíček
    • (MFF UK)
    • Consistency of circuit evaluation, extended resolution and total NP search problems
    • Abstract:
    • We consider sets ?(n,s,k) of narrow clauses expressing that no definition of a size s circuit with n inputs is refutable in resolution R in k steps. We show that every CNF shortly refutable in Extended R, ER, can be easily reduced to an instance of ?(0,s,k) (with s,k depending on the size of the ER-refutation) and, in particular, that ?(0,s,k) when interpreted as a relativized NP search problem is complete among all such problems provably total in the bounded arithmetic theory V^1_1. We use the ideas of implicit proofs to define from ?(0,s,k) a non-relativized NP search problem i? and we show that it is complete among all such problems provably total in bounded arithmetic theory V^1_2. The reductions are definable in S12. We indicate how similar results can be proved for some other propositional proof systems and bounded arithmetic theories and how the construction can be used to define specific random unsatisfiable formulas, and we formulate two open problems about them.
    • 26.10.15   13:30
    • Pavel Hrubeš
    • (Institute of Mathematics, ASCR)
    • Lower bounds on semantic cutting planes
    • Abstract:
    • Cutting Planes is a refutation system which certifies unsatisfiability of a set of linear inequalities. Typically, it is defined as using the addition rule and rounding rule. We consider the semantic version of the system, where every sound inference with a constant number of premises is allowed. We observe that the semantic system has feasible interpolation via monotone real circuits - a fact previously established for syntactic cutting planes by P. Pudlak. Nevertheless, we show that the semantic system is strictly stronger than the syntactic. Joint work with Y. Filmus and M. Lauria.
    • 19.10.15   13:30
    • Samuel R. Buss
    • (University of California, San Diego)
    • Bounded Arithmetic and Propositional Inconsistency Search Functions
    • Abstract:
    • We discuss the strength of fragments of second order bounded arithmetic in defining total NP search (TFNP) problems based on consistency of Frege and extended Frege proofs. This gives new examples of problems that are many-one complete for the second order theories U-1-2 and V-1-2 with proof theoretic strength characterized by polynomial space computation and exponential time computation. (Joint work with Arnold Beckmann.) The talk will begin with a review of the relevant theories of bounded arithmetic, and of the Frege and extended Frege proof systems. It might also cover recent results on propositional proofs of the pigeonhole principle and the Kneser-Lovasz theorem.
    • 27.07.15   13:30
    • Stanislav O. Speranski
    • (Sobolev Institute of Mathematics)
    • On two interesting properties in monadic second-order arithmetic
    • Abstract:
    • Let $A$ be a structure with domain the natural numbers. Consider the following properties: — for each positive integer $n$, the set of $Pi^1_n$-sentences true in $A$ is $Pi^1_n$-complete; — for each positive integer $n$, if a set of natural numbers is $Pi^1_n$-definable in the standard model of Peano arithmetic and closed under automorphisms of $A$, then it is $Pi^1_n$-definable in $A$. Intuitively, they mimic two well-known descriptions of the analytical hierarchy, one in terms of many-one reducibility and one in terms of second-order definability. I develop an approach to proving that certain structures (which are much weaker than the standard model of Peano arithmetic from the viewpoint of first-order logic) have one or both of these properties. E.g. any $A$ in which the divisibility relation is first-order definable has both properties. The same holds for some other interesting structures, including the standard model of Presburger arithmetic, the natural numbers with the coprimeness relation, and every Pascal's triangle modulo a prime.
    • 13.07.15   13:30
    • Amir Tabatabai
    • (Charles University)
    • Disjoint NP pairs and propositional proof systems
    • Abstract:
    • We continue presenting some results relevant to feasible completeness. This week, the 2003 paper "Disjoint NP-Pairs" by Glasser, Selman, Sengupta and Zhang. In this talk, we will concentrate on the problem of the existence of an optimal proof system. The goal is to show that in a relativized version we could find an oracle relative to which optimal proof systems do not exist. To achieve this goal, we need two major steps. First, we will define the canonical NP pair of a propositional proof system and show that any disjoint NP pair is equivalent to one of them. Moreover, if a propositional proof system is complete then its canonical disjoint NP pair should be complete, as well. Secondly, by constructing an oracle we will show that there is not any complete disjoint NP pair relative to that oracle and this is the relativized version which we need.
    • 15.06.15   13:30
    • Arnold Beckmann
    • (Swansea University)
    • Bounded Kripke Platek Set Theory
    • Abstract:
    • Recently, various restrictions of the primitive recursive set functions have been proposed with the aim to capture feasible computation on sets. Amongst these are the "Safe Recursive Set Functions" (Beckmann, Buss, Friedman, accepted for publication in JSL) the "Predicatively Computable Set Functions" (Arai, Archive for Mathematical Logic, vol. 54 (2015), pp. 471–485) and the "Cobham Recursive Set Functions" (Beckmann, Buss, Friedman, Müller, Thapen, in progress). In this talk, I will identify "bounded" versions of Kripke-Platek set theory inspired by Buss' Bounded Arithmetic, which have the potential to capture some of the above classes as their Sigma-1-definable set functions. I will comment on adding definable symbols to these theories, along the lines of the first chapter of Barwise's book "Admissible Sets and Structures". The main part of my talk will be to sketch a proof that the Sigma-1 definable functions of some bounded Kripke-Platek set theory are exactly the Safe Recursive Set Functions.
    • 08.06.15   13:30
    • Raheleh Jalali
    • (Charles University)
    • Propositional proof systems, the consistency of first order theories and the complexity of computations
    • Abstract:
    • The seminar next week will be on *Friday* (replacing the complexity seminar). We plan to use the seminar to go through some old papers relevant to the research project on feasible incompleteness. To start off, Raheleh Jalali will present this paper by Jan Krajicek and Pavel Pudlak, with abstract: We consider the problem about the length of proofs of the sentences Con_S(n) saying that there is no proof of contradiction in S whose length is
    • 05.06.15   13:30
    • Ilario Bonacina
    • (Sapienza University of Rome)
    • Space proof complexity of random 3CNFs
    • Abstract:
    • We prove that Resolution refutations of random 3CNFs in n variables and O(n) clauses require, with high probability, Ω(n) clauses each of width Ω(n) to be kept at the same time in memory. In Polynomial Calculus with Resolution refutations of a random 3-CNF in n variables and O(n) clauses require, with high probability, Ω(n) distinct monomials to be kept simultaneously in memory. For k > 3 such results were proven in joint works with N. Galesi and N. Thapen. The case k = 3 requires some additional work but essentially rely on a purely graph theoretic result: a variant of Hall’s Lemma. We show that in bipartite graphs G with bipartition (L,R) and left-degree at most 3, L can be covered by certain families of disjoint paths, called VW-matchings, provided that L expands in R by a factor of (2 − ε), for small enough ε. Talk based on a joint work with P. Bennet, N. Galesi, T. Huynh, M. Molloy, P. Wollan.
    • 25.05.15   13:30
    • Pavel Pudlak
    • Feasible incompleteness - conjectures and open problems
    • Abstract:
    • In this lecture I will briefly survey main feasible incompleteness conjectures and then focus on open problems.
    • 18.05.15   13:30
    • Ali Enayat
    • (University of Gothenburg)
    • The Power of Satisfaction Predicates
    • Abstract:
    • Suppose we start with a sequential 'base theory' B formulated in a language L (such as B = Peano arithmetic, or B = Zermelo-Fraenkel theory), and we extend B to a new theory B+ consisting of B plus T, where T stipulates that S "resembles" a Tarskian satisfaction predicate. Here T is formulated in the language L+ consisting of L plus an extra binary relation symbol S. For example, T might only express "S is a full satisfaction class" (note that in this case B+ does not include the scheme of induction for formulae of the extended language L+). I will give an overview of the status of our current knowledge of the relationship between B and B+ in connection with the following four questions (for various canonical choices of B and T): 1. Is B+ semantically conservative over B? In other words, does every model of B expand to a model of B+? 2. Is B+ syntactically conservative over B? In other words, if some L-sentence is provable from B+, then is it also provable from B? 3. Is B+ interpretable in B? 4. What type of speed-up (if any) does B+ have over B? This talk reports on joint work with Albert Visser.
    • 04.05.15   13:30
    • Neil Thapen
    • (Institute of Mathematics)
    • Cobham recursive set functions, part 3
    • Abstract:
    • I will define a class CRSF of "polynomial time functions" on arbitrary sets. The definition is in the spirit of Cobham's definition of polynomial time function on strings, in that we can only define a function by recursion if we already know a bound on the complexity of its output. I will show that on binary strings this gives the usual polynomial time functions, and that, for a suitable definition of circuit complexity for sets, every function in CRSF has small circuits. A general theme is that CRSF can be understood as a model of parallel computation over directed acyclic graphs, where the graph of the computation can only be polynomially more complex than the graph given as input. Joint work with Arnold Beckmann, Sam Buss, Sy Friedman and Moritz Mueller.
    • 13.04.15   13:30
    • Neil Thapen
    • (Institute of Mathematics)
    • Cobham recursive set functions, part 2
    • Abstract:
    • I will define a class CRSF of "polynomial time functions" on arbitrary sets. The definition is in the spirit of Cobham's definition of polynomial time function on strings, in that we can only define a function by recursion if we already know a bound on the complexity of its output. I will show that on binary strings this gives the usual polynomial time functions, and that, for a suitable definition of circuit complexity for sets, every function in CRSF has small circuits. A general theme is that CRSF can be understood as a model of parallel computation over directed acyclic graphs, where the graph of the computation can only be polynomially more complex than the graph given as input. Joint work with Arnold Beckmann, Sam Buss, Sy Friedman and Moritz Mueller.
    • 30.03.15   13:30
    • Neil Thapen
    • (Institute of Mathematics)
    • Cobham recursive set functions
    • Abstract:
    • I will define a class CRSF of "polynomial time functions" on arbitrary sets. The definition is in the spirit of Cobham's definition of polynomial time function on strings, in that we can only define a function by recursion if we already know a bound on the complexity of its output. I will show that on binary strings this gives the usual polynomial time functions, and that, for a suitable definition of circuit complexity for sets, every function in CRSF has small circuits. A general theme is that CRSF can be understood as a model of parallel computation over directed acyclic graphs, where the graph of the computation can only be polynomially more complex than the graph given as input. Joint work with Arnold Beckmann, Sam Buss, Sy Friedman and Moritz Mueller.
    • 23.03.15   13:30
    • Michal Garlík
    • (Charles University)
    • A restricted reduced power construction of models of bounded arithmetic, part 2
    • Abstract:
    • We will present a construction of models of bounded arithmetic in the framework of a generalization of the ultrapower construction called restricted reduced power. As an application of the construction we show, assuming the existence of a one-way permutation g hard against polynomial-size circuits, that strictR^1_2(g) is weaker than R^1_2(g).
    • 16.03.15   13:30
    • Michal Garlík
    • (Charles University)
    • A restricted reduced power construction of models of bounded arithmetic
    • Abstract:
    • We will present a construction of models of bounded arithmetic in the framework of a generalization of the ultrapower construction called restricted reduced power. As an application of the construction we show, assuming the existence of a one-way permutation g hard against polynomial-size circuits, that strictR^1_2(g) is weaker than R^1_2(g).
    • 09.03.15   13:30
    • Tin Lok Wong
    • (University of Vienna)
    • Variations of the Arithmetized Completeness Theorem
    • Abstract:
    • The Arithmetized Completeness Theorem is a formalization of Goedel's Completeness Theorem within arithmetic. It is one of the most powerful tools in constructing end extensions of models of arithmetic. In this talk, I will present some non-standard applications about expansions and omega-submodels that satisfy the Weak Koenig Lemma. I will discuss, in particular, the problems one has to face when, instead of Sigma1-induction, we only have Sigma1-collection with exponentiation. This research is joint with Ali Enayat in Gothenburg.
    • 16.02.15   13:30
    • Matthias Baaz
    • (Vienna University of Technology)
    • Elementary cut-elimination for prenex cuts in disjunction free LJ
    • Abstract:
    • The elimination of cuts (lemmas) from given sequent calculus proofs has remained in the focus of proof theory ever since Gentzen's seminal paper from 1934/35. It is well known that the worst case complexity of cut-elimination is non-elementary for first-order intuitionistic as well as classical logic. No elementary upper bound for cut-elimination seems to be known for non-trivial genuine first-order fragments of intuitionistic logics. The purpose of this paper is to show that one can in fact eliminate cuts involving only prenex cut-formulas from disjunction-free intuitionistic sequent proofs without non-elementary increase in the size of proofs. The result is sharp in several respects. As we will show, in all of the following cases there exist non-elementary lower bounds for cut-elimination: (1) classical disjunction-free proofs with quantified atomic cuts (2) intuitionistic disjunction-free proofs with infix cuts, (3) intuitionistic proofs with prenex cuts in the presence of disjunction. (joint work with Chris Fermüller, Vienna University of Technology)
    • 11.02.15   13:30
    • Marcello Stanisci
    • (Sapienza University of Rome)
    • On the complexity of Friedman's Free-set Theorem and Thin-set Theorem
    • Abstract:
    • Free-set Theorem (FST) and Thin-set Theorem (TST), both belonging to the second-order family, have been introduced by H. Friedman in a work called Boolean Relation Theory, that is aimed to find independence results under strong systems of Set Theory. This talk exposes two principles, called LTST and FFST, that are first-order adaptions of FST and TST. In particular, we will see some independence results of LTST and a linear lower bound for FFST. Before presenting the main results, there will be an overview of some known facts that motivated such a research of unprovability, as well as a comparison between FST, TST and the classical Ramsey's Theorem.
    • 12.01.15   13:30
    • Emil Jerabek
    • (ASCR)
    • Recursive functions meet existentially closed structures, Part 2
    • Abstract:
    • Robinson's theory R, which axiomatizes the true Sigma_1 sentences, is one of the weakest known essentially undecidable theories. It also has an interesting structural characterization due to Visser, being the strongest locally finite r.e. theory with respect to interpretation. The essential undecidability of R is a consequence of the fact that it can represent all recursive functions, and it is a natural question whether the converse also holds: i.e., does every r.e. theory that represents all (partial) recursive functions interpret R? The answer is negative, and more generally, R is not interpretable in any consistent theory axiomatized by existential sentences. The explanation comes from model theory. Generalizing the theory of random relational structures (graphs), we will show that for an arbitrary language L (even with functions), the empty L-theory has a model completion EC_L: i.e., EC_L has quantifier elimination, and every L-structure extends to a model of EC_L, so that models of EC_L are exactly the existentially closed L-structures. Furthermore, EC_L is not entirely wild in terms of classification theory: it eliminates exists^infty, and it has the no strict order property, even NSOP_3. (However, unlike the theory of the random graph, it is neither simple nor omega-categorical, and it has the tree property TP_2.) Consequently, various locally finite theories, such as partial orders with arbitrarily long chains, are not interpretable in any consistent existentially axiomatized theory.
    • 15.12.14   13:30
    • Emil Jerabek
    • (ASCR)
    • Recursive functions meet existentially closed structures
    • Abstract:
    • Robinson's theory R, which axiomatizes the true Sigma_1 sentences, is one of the weakest known essentially undecidable theories. It also has an interesting structural characterization due to Visser, being the strongest locally finite r.e. theory with respect to interpretation. The essential undecidability of R is a consequence of the fact that it can represent all recursive functions, and it is a natural question whether the converse also holds: i.e., does every r.e. theory that represents all (partial) recursive functions interpret R? The answer is negative, and more generally, R is not interpretable in any consistent theory axiomatized by existential sentences. The explanation comes from model theory. Generalizing the theory of random relational structures (graphs), we will show that for an arbitrary language L (even with functions), the empty L-theory has a model completion EC_L: i.e., EC_L has quantifier elimination, and every L-structure extends to a model of EC_L, so that models of EC_L are exactly the existentially closed L-structures. Furthermore, EC_L is not entirely wild in terms of classification theory: it eliminates exists^infty, and it has the no strict order property, even NSOP_3. (However, unlike the theory of the random graph, it is neither simple nor omega-categorical, and it has the tree property TP_2.) Consequently, various locally finite theories, such as partial orders with arbitrarily long chains, are not interpretable in any consistent existentially axiomatized theory.
    • 08.12.14   13:30
    • Mateus de Oliveira Oliveira
    • (Institute of Mathematics ASCR)
    • On the Parameterized Complexity of Equational Logic
    • Abstract:
    • In this work we study the validity problem in equational logic under the perspective of parameterized complexity theory. First we introduce a variant of equational logic in which sentences are pairs of the form $(t_1=t_2,omega)$ where $omega$ is an arbitrary ordering of the positions corresponding to subterms of $t_1$ and $t_2$. We call such pairs {em ordered equations}. To each ordered equation one may naturally associate a notion of width and to each proof of validity of an ordered equation one may naturally associate a notion of depth. We define the width of such a proof to be the maximum width of an ordered equation occurring in it. Finally, we introduce a parameter $b$ which restricts the way in which variables are substituted for terms. We say that a proof is $b$-bounded if all substitutions used in it satisfy such restriction. In a surprising result, we show that one may determine whether an ordered equation $(t_1=t_2,omega)$ has a $b$-bounded proof of width $c$ and depth $d$ from a finite set of axioms $E$, in time $f(E,d,c,b)cdot |t_1=t_2|$. In other words this task is fixed parameter linear with respect to the depth, width and bound of the proof. Subsequently, we restrict ourselves to what we call {em oriented proofs}, where the order of a term is always smaller than the order of its subterms. We show that given a classical equation $t_1=t_2$, one may determine whether there exists an ordering $omega$ such that $(t_1=t_2,omega)$ has a $b$-bounded oriented proof of depth $d$ and width $c$ in time $f(E,d,c,b)cdot |t_1= t_2|^{O(c)}$. In other words this task is fixed parameter tractable with respect to the depth and bound of the proof, and is in polynomial time for constant values of width. Observe that this last result is particularly interesting because the ordering $omega$ is not given a priori, and thus, we are indeed parameterizing the provability of equations in classical equational logic. In view of the expressiveness of equational logic, our results give new fixed parameter tractable algorithms to a whole spectrum of problems, such as polynomial identity testing, program verification, automatic theorem proving and the validity problem in undecidable equational theories.
    • 01.12.14   13:30
    • Petr Glivicky
    • Definability in (discretely) ordered integrally divisible modules
    • Abstract:
    • An ordered R-module M with a distinguished element 1 > 0 is called integrally divisible if for each scalar 0 < r in R, any m from M can be divided by r with a remainder (i.e. m = rn + i for some n, i from M with 0
    • 24.11.14   13:30
    • Petr Glivický
    • (Institute of Mathematics)
    • Definability in (discretely) ordered integrally divisible modules
    • Abstract:
    • An ordered R-module M with a distinguished element 1 > 0 is called integrally divisible if for each scalar 0 < r in R, any m from M can be divided by r with a remainder (i.e. m = rn + i for some n, i from M with 0
    • 10.11.14   13:30
    • Ján Pich
    • (Charles University)
    • The PCP theorem in Bounded Arithmetics, Part 2
    • Abstract:
    • We will prove the exponential PCP theorem in the theory APC_1, the PCP theorem in PV_1, assuming certain facts about (n,d,lambda)-graphs, and will discuss the possibility of deriving the PCP theorem in S^1_2 unconditionally.
    • 28.04.14   13:30
    • Petr Glivický
    • (Institute of Mathematics, AS CR)
    • Fermat's Last Theorem and Catalan's conjecture in Weak Exponential Arithmetics
    • Abstract:
    • Wiles's proof of Fermat's Last Theorem (FLT) has stimulated a lively discussion on how much is actually needed for the proof. Despite the fact that the original proof uses set-theoretical assumptions unprovable in Zermelo-Fraenkel set theory with axiom of choice (ZFC), it is widely believed that much less is needed in principle. Harvey Friedman even conjectured that Fermat's Last Theorem is provable in so called elementary function arithmetic (EFA) (which is just ISigma_0 + "2^x is total" in a different language). Smith has showed that EFA proves Fermat's Last Theorem for some small even exponents n (e.g. for n = 4, 6, 10). On the other hand Shepherdson and recently Kolodziejczyk constructed models of IOpen and T^0_2 respectively, where FLT does not hold for n=3. I will present a joint work with Vítězslav Kala. We consider structures and theories in the language L^e=(0,1,+,*,e,
    • 07.04.14   13:30
    • Ján Pich
    • (Charles University)
    • The PCP theorem in Bounded Arithmetics
    • Abstract:
    • We will prove the exponential PCP theorem in the theory $APC_1$, the PCP theorem in $PV_1$, assuming certain facts about $(n,d,lambda)$-graphs, and will discuss the possibility of deriving the PCP theorem in $S^1_2$ unconditionally.
    • 10.03.14   13:30

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

  •