Logic Seminar, Institute of Mathematics, Prague

Logic Seminar
The seminar is usually on Mondays, from 14:00 to 15:30. The location is the Institute of Mathematics, Žitná 25, in the lecture hall on the ground floor of the rear building. The programme is announced via the mailing list.

Monday 12th December, 2:00pm - Sebastian Müller, "Proof Complexity of Random 3CNF Formulas"
Random 3CNF formulas constitute an important distribution for measuring the average-case behavior of propositional proof systems. Lower bounds for random 3CNF refutations in many propositional proof systems are known. Most notable are the exponential-size resolution refutation lower bounds for random 3CNF formulas with Omega(n^{1.5-epsilon}) clauses (Ben-Sasson and Wigderson). On the other hand, the only known non-trivial upper bound on the size of random 3CNF refutations in a non-abstract propositional proof system is for resolution with Omega(n^{2/ log n}) clauses, shown by Beame et al. Using a technique by Feige, Kim and Ofek we will see that already standard propositional proof systems, within the hierarchy of Frege proofs, admit short refutations for random 3CNF formulas, for sufficiently large clause-to-variable ratio. Specifically, we will construct polynomial-size propositional refutations whose lines are TC0 formulas (i.e., TC0-Frege proofs) for random 3CNF formulas with n variables and Omega(n^1.4) clauses. Part of the argument is a spectral one and we therefore need to develop an appropriate way to reason about objects such as some Eigenvalues in a weak arithmetic.

The logic seminar is intended for people doing research in mathematical logic, including doctoral students. Talks are given by regular participants and guests on their own work as well as on interesting recent developments in the field. The prevailing themes in recent years are proof complexity, bounded arithmetic and logical aspects of computational complexity theory in general. Regular participants include members of the logic group, including a number of postdoctoral visitors and Ph.D. students. The seminars are conducted in English unless all participants speak Czech (which seems to never happen).
There is also a student logic seminar at Charles University, intended for undergraduate students.
The seminar has been organized continuously since the early 1970s, first by Petr Hájek for more than twenty years, from the early 90s until the summer of 2008 mostly by Jan Krajíček, and since fall 2008 by Neil Thapen.
Kod predmetu (MFF UK): AIL056 (zimni semestr) a AIL080 (letni semestr)

Past programme

12th October 2009 - Lou van den Dries, "Model theory of reals and o-minimality"

19th October - Lou van den Dries, "Logarithmic - exponential series"

2nd November - Stefan Dantchev, "Proof Complexity lowerbounds via reductions to the Pigeon-Hole Principle" - I will show how a number of known lowerbounds in Proof Complexity plus a few new ones can be obtained in a uniform way, by a kind of reduction to proving a lower bound for the Pigeon-Hole Principle (PHP). This approach makes somewhat stronger cases for studying the so-called Structured PHP (introduced by Krajicek) and for trying to find the precise connection between proof systems and pebble games studied in Finite Model Theory. I will keep all this very informal and, in particular, I will discuss many open questions and possible conjectures.

9th November - Sebastian Müller, "Heuristic Proof Systems" - Heuristic Proof Systems are randomized proof systems that may prove false statements, but only with a negligibly small probability. Hirsch and Itsykson recently introduced a class of randomized proof systems that can be shown to be optimal (in a certain sense) for such heuristic proof systems. We will discuss their approach and talk about the relevant proofs and assumptions.

23rd November - Pavel Pudlák, "Alternating minima and maxima, Nash equilibria and Bounded Arithmetic" - We show that the least number principle for strict \Sigma_k^b formulas can be characterized by the existence of alternating minima and maxima of length k. We show simple prenex forms of these formulas whose herbrandizations (by polynomial time functions) are \forall\Sigma_1^b formulas that characterize \forall\Sigma_1^b theorems of the levels T_2^k of the Bounded Arithmetic Hierarchy, and we derive from this another characterization, in terms of a search problem about finding pure Nash equilibria in k-turn games.

30th November - Pavel Pudlák, "Alternating minima and maxima, Nash equilibria and Bounded Arithmetic", Part 2

7th December - Neil Thapen, "A uniform no-gap theorem" - I will talk about some work in progress on the low-complexity consequences of bounded arithmetic theories. If the \forall \Sigma^b_1 consequences of T^{k+1}_2 are already provable in T^k_2, then the \forall \Sigma^b_1 consequences of T^j_2 are already provable in T^k_2, for any j>k. I will show that this can be done in a uniform way, and will describe a CNF formula F with the property that a bounded depth Frege lower bound for F would imply that CNFs exist separating depth k+1 from depth k Frege for all k.

14th December - Pavel Pudlák, "Truth, soundness and what we actually mean when we accept some axioms" - I will present some thoughts from the book I am writing which concern the concepts mentioned above. I will also explain mistakes in the attempts to apply Godel's Incompleteness Theorem to human mind.

4th January 2010 - Petr Hájek, "Mathematical fuzzy logic and axiomatic arithmetic" - Basic notions of mathematical fuzzy predicate logic (t-norm based) will be briefly surveyed; then various results on properties of Peano- or Robinson-like arithmetic over fuzzy predicate logic will be explained, among them classical Peano arithmetic with a fuzzy truth predicate and essential undecidability of some extremely weak variants of Robinson arithmetic over fuzzy logic.

11th January - Pavel Pudlák, "How to find new axioms?" and "Worlds with different arithmetic" - I will continue with more thoughts about the philosophy and foundations of mathematics that will appear in the book I am writing. As the title says, I will discuss the problem of finding new axioms. But rather than just looking for new set-theoretical axioms as is done in set theory, I am interested in looking for axioms of an essentially different nature. The second topic will be speculations about the possibility that the arithmetical truth that we have in our world is not the only possible one.

15th March - Stefan Hetzl, "On the non-confluence of cut-elimination" - This talk is about cut-elimination in classical first-order logic. I will show how to construct a sequence of polynomial-length proofs having a non- elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand- disjunctions but also have different proof skeletons. This result illustrates that the constructive content of a proof in classical logic can strongly depend on the chosen method for extracting it. Joint work with M. Baaz.

22nd March - Pavel Pudlák, "Visions of future foundations" - This will be a continuation of my talks about the philosophy of mathematics. I will present the last section of my book in which I propose new directions in which one can develop the foundations of mathematics. In particular I will talk about: 1. worlds with different arithmetic than ours and how we can model this by nonstandard models; 2. the relation of the foundations of mathematics to the foundations of physics; I will argue that one should look for a unified foundation of both sciences.

29th March - Pavel Pudlák, "Visions of future foundations", Part 2

12th April - Nicola Galesi, "Hardness of Parameterized Resolution" - Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that paper, Dantchev et al. show a complexity gap in tree-like Parameterized Resolution for propositional formulas arising from translations of first-order principles. We broadly investigate Parameterized Resolution obtaining the following main results: 1) We introduce a purely combinatorial approach to obtain lower bounds to the proof size in tree-like Parameterized Resolution. For this we devise a new asymmetric Prover-Delayer game which characterizes proofs in (parameterized) tree-like Resolution. By exhibiting good Delayer strategies we then show lower bounds for the pigeonhole principle as well as the order principle. 2) Interpreting a well-known FPT algorithm for vertex cover as a DPLL procedure for Parameterized Resolution, we devise a proof search algorithm for Parameterized Resolution and show that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNF's. 3) We answer a question posed by Dantchev, Martin, and Szeider showing that dag-like Parameterized Resolution is not fpt-bounded. We obtain this result by proving that the pigeonhole principle requires proofs of size $n^{\Omega(k)}$ in dag-like Parameterized Resolution. For this lower bound we use a different Prover-Delayer game which was developed for Resolution by Pudlak. Joint work with O. Beyersdorff and M Lauria.

19th April - Radek Honzík, "Failures of GCH and SCH with large cardinals" -We will study the implications large cardinals have on the behaviour of the function \alpha \to 2^\alpha for regular and singular \alpha's. The talk will be in essence introductory, no expertise in set theory is assumed. We will start by motivating the notion of large cardinals and explain the effects they have on the basic cardinal arithmetics (in terms of implications, and in terms of consistency results). In the course of the talk, some original results in this area will be stated.

26th April - Radek Honzík, "Failures of GCH and SCH with large cardinals", Part 2

3rd May - Emil Jeřábek, "Proofs with monotone cuts" - The monotone sequent calculus (MLK) is the subsystem of the usual propositional sequent calculus (LK) obtained by restricting all formulas in the proof to be monotone. Atserias, Galesi and Pudlak showed that MLK quasipolynomially simulates LK-proofs of monotone sequents. We consider a conservative extension of MLK, called MCLK (LK with monotone cuts) which allows arbitrary formulas to appear in the proof, but requires all cut formulas to be monotone. We show that MCLK quasipolynomially simulates LK (even for nonmonotone sequents). We will also mention some connections to monotone decision trees.

10th May - Ján Pich, "Nisan-Wigderson generators in proof systems with forms of interpolation" - Razborov conjectured that the Nisan-Wigderson generators based on suitable functions and matrices should be hard for strong proof systems like Extended Frege. We will discuss the conjecture and prove that the Nisan-Wigderson generators are hard for proof systems that admit feasible interpolation.

17th May - Iddo Tzameret, "Algebraic Proofs over Noncommutative Formulas" - I will discuss algebraic propositional proofs, where polynomials in proof-lines are written as noncommutative formulas. Possible formulations of such proofs lead to systems as strong as Frege. For apparently weaker formulations, we establish non-trivial upper bounds, and discuss possible lower bounds approaches. This work is motivated by the search for lower bound techniques based on rank arguments in propositional proof complexity.

11th October - Neil Thapen, "Approximate counting and search problems" - I will talk about work in progress looking at the relative strengths of some theories of weak induction and some theories connected to approximate counting, as measured by their provable \Sigma^b_1 sentences (also known as total search problems). One motivation is to understand why it is hard to prove separation results for T^2_2 at this level. I will give one proof, that T^1_2 together with the injective weak pigeonhole principle for polynomial time functions does not capture all of the \Sigma^b_1 consequences of T^2_2.

18th October - Pavel Pudlák, "On a theorem of Razborov" - Razborov proved a theorem that characterizes circuit complexity by a communication complexity game. In a sense it is a generalization of the theorem of Karchmer and Wigderson that characterizes circuit depth. This theorem has an important application in proof complexity. It was used by Krajicek to prove his Feasible Interpolation Theorem for Resolution proofs. This seminar will be a sort of an introduction to the problem that we will consider on a future seminar: How to generalize Razborov's theorem to higher levels of the hierarchy of Frege systems.

25th October - Vladimir Voevodsky (recorded talk at Princeton), "What if Current Foundations of Mathematics are Inconsistent?"

8th November - Albert Atserias, "Mean-Payoff Games and Propositional Proofs" - We associate a CNF-formula to every instance of the mean-payoff game problem in such a way that if the value of the game is non-negative the formula is satisfiable, and if the value of the game is negative the formula has a polynomial-size refutation in $\Sigma_2$-Frege (i.e.~DNF-resolution). This reduces mean-payoff games to the weak automatizability of $\Sigma_2$-Frege, and to the interpolation problem for $\Sigma_{2,2}$-Frege. Since the interpolation problem for $\Sigma_1$-Frege (i.e.~resolution) is solvable in polynomial time, our result is close to optimal up to the computational complexity of solving mean-payoff games. The proof of the main result requires building low-depth formulas that compute the bits of the sum of a constant number of integers in binary notation, and low-complexity proofs of the required arithmetic properties.

15th November - Pavel Pudlák, "On a theorem of Razborov", Part 2

22nd November - Moritz Müller, "Undefinable forcing" - In set theory one defines forcing semantically via truth in all generic extensions and proves it equivalent to a handier, syntactical notion that is defined via recursion on logical syntax. This Forcing Completeness Theorem is the key to the fundamental forcing lemmas, most importantly, the Definability Lemma that states that the forcing relation is definable in the ground model. In turn, the forcing lemmas yield the Principal Theorem stating that generic extension are models of ZFC. Then an independence question is reduced to the combinatorial task for the design of a suitable forcing frame. In this sense forcing in set theory is a method. Some independence results in bounded arithmetic have been obtained via forcing type arguments. But in contrast to set theory, no general forcing theory is available. These arguments substantially differ from the set theoretic setting in that they produce expansions instead of extensions and work without a Forcing Completeness Theorem and without a Definability Lemma. It is not completely clear in what sense they are of the forcing type. The talk presents work in progress, a trial to develop forcing in bounded arithmetic as a method. It presents a proposal of some general frame for forcing that can be seen as a common generalization of Cohen forcing in set theory and the mentioned forcing type arguments in arithmetic. This amounts to develop forcing without a Definability Lemma. For fragments of arithmetic a Principal Theorem would state that generic expansions satisfy the least number principle for a certain fragment of formulas. Such Principal Theorems can be obtained when using a forcing that is in a certain weak sense definable for the fragment in question. In this sense an independence question is again reduced to a combinatorial question for the design of a suitable forcing frame.

29th November - Neil Thapen, "Interpolation and a kind of generalized circuit" - I will talk about some work in progress on how the feasible interpolation theorem for resolution could be extended to higher-depth proof systems.

28th February 2011 - Emil Jeřábek, "Real closures of models of arithmetic" - This is a joint work with Leszek Kołodziejczyk. If R is a countable recursively saturated real-closed field, and T any consistent r.e. extension of IOpen, then R has an integer part M which is a model of T by resplendence. In a recent paper, D'Aquino, Knight and Starchenko have shown a kind of converse: if R is a real-closed field with an integer part M which is a model of I\Sigma_4, then R is recursively saturated. We will generalize this result to fragments of bounded arithmetic (IE_2, PV, \Sigma^b_1-IND^{|x|_k}). This suggests that recursive saturation of real closure is a Tennenbaum-like property.

7th March - Pavel Pudlák, "Logic of space-time and relativity theory" - I will present "Logic of space-time and relativity theory" by Andreka, Madarasz and Nemeti. They propose first order axiomatizations of special and general theories of relativity. The talk should be understanble without a deeper background in physics.

28th March - Pavel Pudlák, "Finitism and physical reality" - This will be another seminar about the philosophy of mathematics. The main question about which it will revolve is: Are the physical natural numbers the same as the mathematical natural numbers?

4th April - Jan Krajíček, "On the proof complexity of TC^0 Frege systems" - We make some observations on the relation of AC^0 and TC^0 Frege proof systems.

11th April - Petr Glivicky, "Quantifier elimination in Linear Arithmetic and Peano Products" - While Presburger arithmetic (Pr) is a descriptively simple theory (has an elimination set consisting of $\Sigma$-formulas), Peano arithmetic (P) has no elimination at all. I will introduce a theory of Linear arithmetic (LA) which extends Pr by multiplication by one scalar (with full induction) and prove that it has still an elimination set consisting of $\Sigma$-formulas. I will use this result to show some properties of products in models of Peano arithmetic (Peano products) concerning in particular mutual (in)dependence of values of a Peano product in different points.

18th April - Jan Krajíček, "Algorithmic dense model theorem, a survey" - The following is from an abstract of Impagliazzo's talk. "Green and Tao used the existence of a dense subset indistinguishable from the primes under certain tests from a certain class to prove the existence of arbitrarily long prime arithmetic progressions. Reingold, Trevisan, Tulsiani and Vadhan, and independently, Gowers, give a quantitatively improved characterization of when such dense models exist. An equivalent formulation was obtained earlier by Barak, Shaltiel and Wigderson." Impagliazzo found a connection with the hard core theorems about pseudorandom generators. The theorem may also be potentially useful in proof complexity.

2nd May - Jan Krajíček, "Algorithmic dense model theorem, a survey", Part 2

9th May - Marta Bílková, "Moss' coalgebraic modal logic" - Coalgebras provide a uniform framework to deal with various semantic structures for existing modal languages (various types of Kripke frames), as well as various state based transition systems (automata). [ Technically, given a functor T: Set --> Set, a T-coalgebra is a map c: X -->TX, (X is a set of "states", T is the type of "behaviour" or "future", and c is the transition map.) ] Recently various people concentrate both on coalgebraic approach to existing modal logics and finding expressive modal languages for interesting classes of colgebras. In this talk I'll concentrate on one of the possible approaches to the latter, proposed by Larry Moss in 90's. The main idea is that to define a language for T-coalgebras one can deal with a single modality coming from the functor T (its semantics as well as syntax is given by the functor). I'll show how to give a uniform axiomatization and to define cut-free sequent style proof systems for such languages. I'll also try to say how useful can such a language be for ordinary modal language (it provides a disjunctive normal form which e.g. simplifies some interpolation proofs).

16th May - Massimo Lauria, "The proof complexity of Paris-Harrington tautologies" - We initiate the study of the proof complexity of propositional encoding of (weak cases of) concrete independence results. We study the proof complexity of Paris-Harringtons Large Ramsey Theorem for bicolorings of graphs. We prove a non-trivial conditional lower bound in Resolution and a quasi-polynomial upper bound in bounded-depth Frege. The lower bound is conditional on a hardness assumption for a Weak (quasi-polynomial) Pigeonhole Principle in Res(2). The proof technique of the lower bound extends the idea of using a combinatorial principle to blow-up a counterexample for another combinatorial principle beyond the threshold of inconsistency. A strong link with the proof complexity of an unbalanced Ramsey principle for triangles is established. This is obtained by applying some highly non-trivial constructions due to Erdos and Mills. (Joint work with Lorenzo Carlucci and Nicola Galesi.)

17th October - Pavel Pudlák, "Models explaining pseudorandomness by randomess" - We construct a nonstandard model of arithmetic M_0, an element \Delta \in M_0, a system S of extensions of M_0 and a probability measure on S such that: M_0 is a model of PV; every N \in S is an elementary extension of M_0 w.r.t. polynomial time computable predicates; and for every pseudorandom function f with two values -1 and 1, the probability that f(\Delta)=1 is 1/2 for random N.

24th October - Emil Jeřábek, "Root finding in TC^0" - We show that for any constant d, there is a uniform TC^0 algorithm computing approximations of complex zeros of degree d univariate rational polynomials (given by a list of coefficients in binary). The basic idea is to compute the inverse of the polynomial by a power series, using tools from complex analysis, and the result of Hesse, Allender and Barrington that division and iterated products are computable in uniform TC^0. This work is motivated by bounded arithmetic. The complexity class TC^0 contains the basic arithmetical operations (addition, multiplication, ordering), but it is not clear which properties of these operations are provable in the corresponding theory VTC^0 (for binary numbers, i.e., the string sort). It is not even known whether VTC^0 proves integer division to be total. Our result can be equivalently restated as follows: VTC^0 extended with the set of all true \forall\Sigma^B_0 sentences includes IOpen (induction for open formulas in the basic language of arithmetic).

31st October - Dai Tri Man Le, "Complexity Classes and Theories for the Comparator Circuit Value Problem" - Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem. He proved that several other problems are complete for CC, including the stable marriage problem, and finding the lexicographical first maximal matching in a bipartite graph. We suggest alternative definitions of CC based on different reducibilities and introduce a two-sorted theory VCC* based on one of them. We sharpen and simplify Subramanian's completeness proofs for the above two problems and show how to formalize them in VCC*.

14th November - Alexander Smal, "Optimal heuristic algorithms for the image of an injective function" - The existence of optimal algorithms is not known for any decision problem in NP - P. We consider the problem of testing the membership in the image of an injective function. We construct optimal heuristic algorithms for this problem in both randomized and deterministic settings (a heuristic algorithm can err on a small fraction 1/d of the inputs; the parameter d is given to it as an additional input). Thus for this problem we improve an earlier construction of an optimal acceptor (that is optimal on the negative instances only) and also give a deterministic version.

21st November - Jakob Nordström, "A general paradigm(?) for proving time-space trade-offs in proof complexity" - I will survey a recent line of work on proving time-space trade-offs for resolution (partly joint with Hastad and Ben-Sasson) and describe how these results can be viewed as a general technique of amplifying weak lower bounds to stronger lower bounds in proof complexity. I will then show that this general paradigm generalizes to the k-DNF resolution proof systems, and discuss whether it might be made to work for Polynomial Calculus and Cutting Planes as well. Time permitting, I might briefly mention some new results that can be interpreted as indicating that this should be the case.

28th November- Yuval Filmus, "Scales of prefix codes for N" - We consider monotone prefix codes for the natural numbers. These codes come up naturally in software engineering, and "universal" codes have been suggested by Elias (75). Elias suggested an infinite sequence of codes which get progressively better, and diagonalized his construction to produce an ultimate code. We show that Elias's ultimate code -- or any other single code, or even sequence of codes -- is not optimal by finding a code better than any given sequence of codes. This implies that a scale exists if CH holds, and that in Cohen's model without CH, there is no scale. Given a (uniformly) recursive sequence of codes, the code our construction produces is also recursive. Consequently, we also get a version of the fast-growing hierarchy for codes.

5th December - Neil Thapen, "More on approximate counting and search problems" - Jeřábek's theory for approximate counting consists of the bounded arithmetic theory T^1_2 together with the surjective weak pigeonhole principle (sWPHP) for P^NP functions. It is consistent with what is known that every \Sigma^b_1 sentence provable in bounded arithmetic is already provable in this theory, although it is expected that this is not the case. We consider the provable \Sigma^b_1 sentences (also known as total search problems) of natural subtheories of approximate counting. I will talk about some new results in this area: I will give a separation between T^2_2 and PV + sWPHP for P^NP functions in the relativized case; and I will describe a plausible conjecture about narrow resolution refutations that implies a similar separation for T^1_2 + sWPHP for polynomial time functions. Joint work with Sam Buss and Leszek Kołodziejczyk.

Programme archive for 2008 / 2009

Programme archive for 1995 - Summer 2008

Auxiliary Links
Fall schools
Colloquia lectures
Web connections
Proof complexity mailing list
Jech's library of preprints/reprints in set theory is available to students in our department
Baby logic seminar

9/5/10 Neil Thapen