slideshow 3

Logic seminar

usually takes place each Monday at 16:00 in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.

Space proof complexity of random 3CNFs

Ilario Bonacina
Sapienza University of Rome
Monday, 25. May 2015 - 13:30
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.

Feasible incompleteness - conjectures and open problems

Pavel Pudlak
Monday, 18. May 2015 - 13:30
In this lecture I will briefly survey main feasible incompleteness conjectures and then focus on open problems.

The Power of Satisfaction Predicates

Ali Enayat
University of Gothenburg
Monday, 4. May 2015 - 13:30
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+... more

Cobham recursive set functions, part 3

Neil Thapen
Institute of Mathematics
Monday, 13. April 2015 - 13:30
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.