Logic Seminar
The seminar is usually on Mondays, from 13:30 to 15:00. 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.
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 partic ipants 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.
Programme archive for 2008 / 2009
Programme archive for 1995 - Summer 2008
Auxiliary Links
Jech's library of preprints/reprints in set theory is available to students in our department
10/03/10 Neil Thapen
