•  
    • 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

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

  •