Logic Seminar
The seminar is usually on Mondays, from 11.00 to 12.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 7th DecemberNeil 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.
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
- 6th October 2008 - Leszek Kołodziejczyk, "Building models for very weak theories of arithmetic" - I will discuss a new method for constructing nonstandard models of weak fragments of bounded arithmetic, developed primarily in a paper by Boughattas and Ressayre. The method, inspired by algebraic techniques used in the study of open induction, is based on the idea that a model can be built from nonstandard reals rather than just nonstandard integers. It has been applied to obtain new independence results for weakened versions of \Sigma^b_1 induction and for Buss' theory T^0_2.
- 13th October - Phuong Nguyen, "Separating DAG-like and Tree-like Proof Systems" - I will present my paper "Separating DAG-like and Tree-like Proof Systems" in LICS 2007. In particular, I will show that constant-depth treelike Frege proof systems do not simulate cut-free daglike Frege, and that depth-d treelike Frege does not simulate depth-(2d+5) treelike Frege. The latter implies that the Sigma_0^B consequences of V^0 is not finitely axiomatizable. The proof method is an improvement and simplification of an earlier paper by Maciel and Pitassi, and is applicable to the sequents invented by Statman whose lowerbounds and upperbounds have been shown by elegant arguments.
- 20th October - Emil Jeřábek, "Abelian groups and quadratic residues in weak arithmetic" - We investigate the provability of some properties of abelian groups and quadratic residues in variants of bounded arithmetic. Specifically, we show that the structure theorem for finite abelian groups is provable in T^2_2, and use it to derive Fermat's little theorem and Euler's criterion for the Legendre symbol in T^2_2 extended by the pigeonhole principle. We prove the quadratic reciprocity theorem (including the supplementary laws) in bounded arithmetic extended with modulo-2 counting principles.
- 3rd November - Emil Jeřábek, "Abelian groups and quadratic residues in weak arithmetic", Part 2
- 10th November - Arnold Beckmann, "Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic" - The complexity class of \Pi^p_k-polynomial local search (PLS) problems is introduced and is used to give new witnessing theorems for fragments of bounded arithmetic. These \Pi^p_k-PLS problems can be defined in a weak base theory such as S^1_2, and proved to be total in T^{k+1}_2 . Furthermore, the \Pi^p_k-PLS definitions can be skolemized with simple polynomial time functions, and the witnessing theorem itself can be formalized, and skolemized, in a weak base theory. This gives rise to a new \forall\Sigma^b_1(X)-principle that is conjectured to separate T^k_2(X) and T^{k+1}_2(X).
- 14th November - Barbara Csima, "Computable structure theory" - In computable structure theory, one examines various countably infinite structures (such as linear orderings and graphs) for their computability theoretic properties. For example, the standard theorem that any two countable dense linear orders without endpoints are isomorphic can be carried out computably, in the sense that if the two countable dense linear orders are nicely presented, then there must be a computable isomorphism between them. However, there are many examples of computable structures that are isomorphic but not computably isomorphic. This talk will be an introduction to computable structure theory, explaining some standard examples, and indicating areas of current research.
- 8th December - Iddo Tzameret, "The Proof Complexity of Polynomial Identities" -Devising an efficient deterministic -- or even a non-deterministic sub-exponential time -- algorithm for testing polynomial identities is a fundamental problem in algebraic complexity and complexity at large. Motivated by this problem, as well as by results from proof complexity, we investigate the complexity of proving polynomial identities. To this end, we study a class of equational proof systems, of varying strength, operating with polynomial identities written as arithmetic formulas over a given ring. A proof in these systems establishes that two arithmetic formulas compute the same polynomial, and consists of a sequence of equations between polynomials, written as arithmetic formulas, where each equation in the sequence is derived from previous equations by means of the polynomial-ring axioms. This works establishes non-trivial upper and lower bounds on the size of equational proofs of polynomial identities. In this talk I will present the basic model of equational proofs, argue for its relevance and importance in both algebraic complexity and proof complexity, and demonstrate several upper and lower bounds, in various fragments of equational proofs. Joint work with Pavel Hrubes.
- 15th December - Iddo Tzameret, "The Proof Complexity of Polynomial Identities", Part 2
- 12th January 2009 - Iddo Tzameret, "The Proof Complexity of Polynomial Identities", Part 3
- 26th January - Jindřich Zapletal, "Borel equivalences and their applications" - The study of Borel equivalence relations is growing at a very fast rate. These equivalences are compared according to a natural notion of complexity, resulting in a rich map. It turns out that such branches of mathematics as algebra, ergodic theory, or functional analysis contain key equivalences that can be placed on this map, leading to a precise quantification of their difficulty. The lecture is an invitation to a course I will teach this term at the Department of Mathematical Analysis at Charles University.
- 9th February - Olaf Beyersdorff, "The complexity of reasoning for fragments of default logic" - Default logic was introduced by Reiter in 1980. In 1992, Gottlob classified the complexity of the extension existence problem for propositional default logic as $\Sigma_2^p$-complete, and the complexity of the credulous and skeptical reasoning problem as $\Sigma_2^p$-complete, resp. $\Pi_2^p$-complete. Additionally, he investigated restrictions on the default rules, i.e., semi-normal default rules. Selman made in 1992 a similar approach with disjunction-free and unary default rules. In this talk we systematically restrict the set of allowed propositional connectives. We give a complete complexity classification for all sets of Boolean functions in the meaning of Post's lattice for all three common decision problems for propositional default logic. We show that the complexity is a trichotomy ($Sigma_2^p$-, NP-complete, trivial) for the extension existence problem, whereas for the credulous and sceptical reasoning problem we get a finer classification down to NL-complete cases. The results described in the talk are joint work with Arne Meier, Michael Thomas, and Heribert Vollmer.
- 16th February - Pavel Pudlák, "On platonism, intuitionism and Hilbert" - I will present a part of a chapter of the book I am writing. I plan to say more about the philosophy of mathematics later this semester.
- 2nd March - Stefano Cavagnetto, "Euclid’s Elements" - Euclid’s Elements is one of the most beautiful and influential works of mathematics in the history of science. Its beauty relies on its logical development of geometry and other branches of mathematics. The Elements have influenced all branches of science but none as much as mathematics. Entire generations of mathematicians have been shaped by this masterpiece and its influence is still vivid in modern mathematics. Although many of the results contained in this work originated earlier, one of Euclid’s achievements was to present them in a single and logically coherent framework. This made it easy to use the contents and easy to reference them for other mathematicians. The system of rigorous mathematical proofs still remains the basis of modern mathematics. In this talk I will give a quick overview of the contents of the Elements in the order they appear in the thirteen books. I’ll focus in some detail on the first two books and on their logical structure with the aim of giving a good grasp of Euclid’s modernity. Finally I’ll discuss a small fragment of papyrus containing the Proposition 5 of Book II. This fragment was found among the remarkable rubbish pile of Oxyrhynchus in 1896-97 and it can be interpreted in modern terms, as other results in Book II, as a geometric formulation of algebraic problems.
- 9th March - Nicola Galesi, "Lower bounds in Polynomial Calculus and its extensions to k-DNF Resolution" - We consider an algebraic proof system PCR[k], which combines together Polynomial Calculus (PC) and k-DNF Resolution (RES[k]). We study the complexity of proofs in this family of systems, extending to PCR[k] some of the results known for RES[k]. We prove that random 3-CNF formulas with a linear number of clauses are hard to prove in PCR[k]; We prove a strict hierarchy result showing that PCR[k+1] is exponentially stronger than PCR[k]. The results rely on proving degree lower bounds for PCR refutations of a Graph Ordering Principle, which gives the first example of a family of contradictions having PCR short refutations but requiring high degree and thus also proving the optimality of the size-degree tradeoffs for PCR. Finally we consider the question of whether PC/PCR are automatizable and we prove, exactly as for Resolution, that the answer is no, conditioned on a complexity assumption. The talk is based on joint work with Massimo Lauria.
- 16th March - Jan Krajíček, "A form of feasible interpolation for constant depth Frege systems" - Let L be a first-order language and Phi and Psi two Sigma^1_1 L-sentences that cannot be satisfied simultaneously in any finite L-structure. Then obviously the following principle Chain_{L,Phi,Psi}(n,m) holds: For any chain of finite L-structures C_1, ..., C_m with the universe [n] one of the following conditions must fail: (1.) C_1 satisfies Phi, (2.) C_i is isomorphic to C_{i+1}, for i = 1, ..., m-1, (3.) C_m satisfies Psi. For each fixed L and parameters n, m the principle can be encoded into a propositional DNF formula of size polynomial in n,m. For any language L containing only constants and unary predicates we show that if a constant depth Frege system in DeMorgan language proves Chain_{L,Phi,Psi}(n,n) by a size s proof then the class of finite L-structures with universe [n] satisfying Phi can be separated from those L-structures on [n] satisfying Psi by a depth 3 formula of size exponential in polylog(s) and with bottom fan-in polylog(s).
- 23rd March - Neil Thapen, "Search problems for stronger bounded arithmetic theories" - We define the "local improvement principle" LI, an NP search problem about labellings of bounded degree, acyclic graphs. This can be seen as a generalization of the game induction principle, or, in some sense, as an exponentially larger version of PLS. We show that versions of LI characterize over PV the \forall \Sigma^b_1 sentences provable in T^i_2, U^1_2 and V^1_2 and characterize over ID_0 the \forall \Sigma^B_0 sentences provable in V^1_1. By RSUV isomorphism, this last result can be interpreted as a characterization of the \forall \pi^b_1 sentences provable in S^1_2. Joint work with Leszek Kolodziejczyk and Phuong Nguyen.
- 30th March - Neil Thapen, "Search problems for stronger bounded arithmetic theories", Part 2
- 6th April - Stefan Dantchev, "Parameterized Proof Complexity" - We propose a proof-complexity approach for separating certain parameterized complexity classes. We consider proofs showing that a given propositional formula cannot be satisfied by a truth assignment that sets at most k variables to true, considering k as the parameter (we call such a formula a parameterized contradiction). One could separate the parameterized complexity classes FPT and W[SAT] by showing that there is no fpt-bounded parameterized proof system for parameterized contradictions, i.e., that there is no proof system that admits proofs of size f(k).poly(n) where f is an arbitrary computable function and n is the size of the propositional formula. By way of a first step, we introduce the system of parameterized tree-like resolution, and show that this system is not fpt-bounded. Indeed, we give a general result on the size of shortest tree-like resolution proofs of parameterized contradictions that uniformly encode first-order principles over a universe of size n. We establish a dichotomy theorem that splits the exponential case of Riis's Complexity Gap Theorem into two sub-cases, one that admits proofs of size exp(k) . poly(n) and another that requires proofs of size at least n ^ (k ^ \alpha) for some constant \alpha greater than zero.
- 20th April - Jindřich Zapletal, "Woodin's work on absoluteness" - Woodin suggests that he made progress towards resolving the continuum hypothesis. I will outline the work that lead him to this conclusion.
- 11th May - Pavel Pudlák, "Consistency, reflection principles, transfinite iterations, etc." - Assuming that an arithmetical theory T is true we can derive several true arithmetical sentences that are not provable in T. The simplest is Con(T) (the arithmetization of the statement that T is consistent). Then there is a hierarchy of reflection principles. One can make T even stronger by adding a truth predicate to it. One can further iterate these extensions along recursive ordinals. This also naturally leads to subsystems of Second Order Arithmetic. The main question I want to address is: Does it mean that there is no limit on the theories that we can recognize as true?
- 12th October - 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 Pudlak, "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 Pudlak, "Alternating minima and maxima, Nash equilibria and Bounded Arithmetic", Part 2
Programme archive for 1995 - Summer 2008
Auxiliary Links
Jech's library of preprints/reprints in set theory is available to students in our department
14/10/09 Neil Thapen
