# 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 participants speak Czech (which never seems to 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.

Kód předmětu (MFF UK): AIL056 (zimní semestr) a AIL080 (letní semestr)

### Past programme 2012-2014

• 8th October 2012 - Emil Jeřábek, "Integer factoring by parity arguments" - Papadimitriou introduced several classes of NP search problems based on combinatorial tasks. In particular, the class PPA (polynomial parity argument) consists of problems reducible to the following problem: given a circuit representing an undirected graph of maximum degree 2, and a vertex of degree 1, find another vertex of degree 1. Equivalently, a problem is in PPA if it is reducible to finding a fixpoint of a given involutive function (represented by a circuit) on a domain of odd size. The main result of this talk is that integer factoring has a randomized reduction to a PPA problem. (The reduction can be derandomized assuming a suitable version of the generalized Riemann hypothesis.) This improves a previous result of Buresh-Oppenheim that PPA can factor integers n = 1 (mod 4) having a prime divisor p = 3 (mod 4). The main ingredient of our proof is that the following problem is in PPA: given integers a,n such that the Jacobi symbol (a|n) = 1, find either a square root of a mod n, or a factor of n. We can show this by proving the law of quadratic reciprocity and multiplicativity of the Jacobi symbol in a suitable extension of bounded arithmetic corresponding to PPA, and applying a witnessing theorem. We may also discuss some related results, such as a randomized reduction of factoring to PPP (more precisely, the weak pigeonhole principle), and computing square roots mod n in PPA.

• 16th October - Neil Thapen, "Automatizability and games" - Parity games, mean payoff games and simple stochastic games are families of two-player games played on finite graphs. In each game, deciding which player has a winning strategy is in NP intersect coNP, and it is an open problem to establish whether or not it is in P. A proof system is called weakly automatizable if, roughly speaking, there is a polynomial time algorithm which distinguishes between formulas that are satisfiable and formulas which have a short refutation in the system. Recent papers by Atserias and Maneva and by Huang and Pitassi have shown that the decidability of mean payoff games and simple stochastic games is reducible to the weak automatizability of certain constant-depth proof systems. We simplify and extend their results, in particular showing that if resolution is weakly automatizable, then parity games can be decided in polynomial time. Joint work with Arnold Beckmann and Pavel Pudlak.

• 29th October - Pavel Pudlák, "How difficult is it to prove that a graph is non-Ramsey?" - We will prove a lower bound on resolution proofs of a tautology expressing that a given graph does not have homogeneous sets of size c.log n, where n is the number of vertices.

• 12th November - Wojciech Dzik, "Unification of terms in equational theories and in logic" - Unifiers, i.e. substitutions making two terms equal, modulo a given theory, are quasi-ordered by the relation of "being more general than". Unification type of a theory (or a logic) can be unitary, finitary, infinitary or nullary, depending on the number of maximal (with respect to the quasi-order) unifiers. I will show that in case of (weakly) transitive theories (logics) there is a particular splitting (join-splitting) in the lattice of all theories (logics) which determines particular unification types. I will also give some applications of (projective) unifiers to the problem of admissible rules in logic.

• 26th November - Michal Garlík, "On a Proof of Ajtai's Completeness Theorem for Nonstandard Finite Structures" - Ajtai's generalization of Gödel's completeness theorem describes a definability condition equivalent to the existence of an extension and expansion of a given nonstandard finite structure to a model of a given recursive theory. I will present a proof of the theorem and discuss some applications of the theorem which relate to problems in computational complexity.

• 10th December - Michal Garlík, "On a Proof of Ajtai's Completeness Theorem for Nonstandard Finite Structures", Part 2
• 14th January 2013 - Jan Pich, "Intuitionism and Natural Proofs" - We will discuss the question whether intuitionistic proofs of superpolynomial circuit lower bounds in theories of bounded arithmetic are natural and the problem of efficient witnessing errors of p-time SAT algorithms.

• 18th February - Jindřich Zapletal, "Canonical Ramsey Theory on Polish Spaces" - I will outline the subject of my new book with Vladimir Kanovei and Marcin Sabok. It concerns the classification effort for Borel equivalence relations in descriptive set theory.

• 25th February - Neil Thapen, "The complexity of proving that a graph is Ramsey" - Say that an graph with n vertices is c-Ramsey if it contains no clique or independent set of size c log n. Such a graph witnesses that the Ramsey number r(k) > 2^{k/c}. We define a propositional formula which expresses that a given graph G is c-Ramsey, and show that this formula requires superpolynomial size to prove in resolution, for every graph G. In particular it follows that no polynomial time algorithm for constructing c-Ramsey graphs has a polynomial size resolution proof of its correctness. We rely on a property of c-Ramsey graphs, that every such graph must contain a large subgraph with some of the density properties of the random graph. Other than this, I aim to give a fairly self-contained presentation and will review the necessary background in proof complexity. This is an update of material which Pavel Pudlák presented in the seminar last year.

• 4th March - Neil Thapen, "The complexity of proving that a graph is Ramsey", Part 2

• 11th March - Jan Pich, "Circuit lower bounds in bounded arithmetics" - We will present a natural formalization of polynomial circuit lower bounds in the language of bounded arithmetic, show its properties and some new unprovability results.

• 18th March - Jan Pich, "Circuit lower bounds in bounded arithmetics", Part 2

• 25th March - Albert Atserias, "Quasipolynomial Upper and Lower Bounds for DNF-refutations of a Relativized Weak Pigeonhole Principle" - The relativized weak pigeonhole principle states that if 2n out of n^2 pigeons fly into n holes then some hole must be doubly occupied. By interpreting the usual weak pigeonhole principle in it we note that it has quasipolynomial size n^{polylog(n)} refutations in R(log). We prove a matching lower bound: any R(log), and indeed any DNF-refutation, must have size n^{(log n)^{1/2-\eps}} for every \eps and sufficiently large n. This is joint work with Moritz Müller (Vienna), and Sergi Oliva (Barcelona)

• 8th April - Helmut Schwichtenberg, "Proofs, computations and analysis" - Algorithms are viewed as one aspect of proofs in (constructive) analysis. Data for such algorithms are finite or infinite lists of signed digits -1, 0, 1 (i.e., reals as streams), or possibly non well-founded labelled (by lists of signed digits -1, 0, 1) ternary trees (representing uniformly continuous functions). A theory of computable functionals (TCF) suitable for this setting is described. The main tools are (i) a distiction between computationally relevant and irrelevant logical connectives and (ii) simultaneous inductively/coinductively defined predicates. A realizability interpretation of proofs in TCF can be given, and a soundness theorem holds.

• 15th April - Jan Krajíček, "On the computational complexity of finding hard tautologies" - It is well-known that a polynomial time algorithm finding tautologies hard for a propositional proof system P exists iff P is not optimal. Such an algorithm takes 1^(k) and outputs a tautology A_k of size at least k such that P is not p-bounded on the set of all A_k's. We consider two more general search problems involving finding a hard formula, Cert and Find, motivated by two hypothetical situations: that one can prove that NP and coNP differ and that no optimal proof system exists. In Cert one is asked to find a witness that a given non-deterministic circuit with k inputs does not define TAUT restricted to size k. In Find, given 1^k and a tautology B of size at most k^c, one should output a size k tautology that has no size k^d P-proof from substitution instances of B. We shall prove, assuming the existence of an exponentially hard one-way permutation, that Cert cannot be solved by an algorithm in time exp(k). Using a stronger hypothesis about the proof complexity of Nisan-Wigderson generator we show that both problems Cert and Find are actually undefined for infinitely many k. The results are based on interpreting the Nisan-Wigderson generator as a proof system.

• 22nd April - Petr Glivický, "Descriptive analysis of linear theories and dependency problem in Peano arithmetic" - There is a large gap between the Presburger (Pr) and Peano arithmetics. One way how to explore this space is to consider various extensions of Pr by fragments of product. Linear theories are certain extensions of Pr by multiplication by a set of scalars and with full induction for their language. We show a quantifier elimination result for linear theories, and we perform a detailed analysis of definable sets and functions in their models. In particular, we state that every definable set in a model A of a linear theory is a finite union of linear images of polyhedra in A^k, for some k. As an application of these results, we solve an important instance of the dependency problem in Peano arithmetic. We prove that, for a fixed saturated model B of Pr, the only values of a Peano product on B which are uniquely determined by its values on the line {a} x B (a is from B) are the trivial ones. This enables us to construct a new product on B which satisfies certain amount of induction.

• 6th May - Hong Van Le, "Voevodsky's homotopy type theory and univalent foundations" - Voevodsky's univalent foundation is an application of his homotopy type theory, relating symbolic logic with topology and computer science. In this talk I will discuss basic concepts, examples, and advantages of homotopy type theory, especially Voevodsky's univalent homotopy type theory. The main references are talks by Voevodsky placed on his website, sources from nLab, wiki and the website http://homotopytypetheory.org/ as well as a paper by Awodey "Type theory and Homotopy".

• 13th May - Emil Jeřábek, "Open induction in VTC^0 + IMUL" - Basic arithmetic operations are computable in uniform TC^0, with multiplication being TC^0-complete. We can define addition, multiplication, and ordering on binary integers in the corresponding bounded arithmetic theory VTC^0, and prove that they form a discretely ordered ring. It is a natural question what other first-order properties of elementary arithmetic operations are provable in VTC^0. Since it is not known whether VTC^0 can formalize the Hesse-Allender-Barrington uniform TC^0 algorithms for division and iterated multiplication, we can also consider the same question for the theory VTC^0 + IMUL, including an axiom for iterated multiplication. In previous work, I have proved that there are uniform TC^0 algorithms for approximation of complex roots of constant-degree univariate rational polynomials, which means that VTC^0 extended with all true \forall\Sigma^B_0 sentences proves induction for open formulas in the language of ordered rings (IOpen). In this talk, I will establish that IOpen is in fact provable in VTC^0 + IMUL.

• 20th May - Alexandre Borovik, "Logical and model-theoretic issues of black box group theory" - The talk will describe a peculiar and perhaps unique phenomenon in mathematics: the so-called "black box" probabilistic algorithms of computational finite group theory and discuss its logical and model-theoretic connections. (Joint work with Sukru Yalcinkaya.)

• 27th May - Emil Jeřábek, "Open induction in VTC^0 + IMUL", Part 2 - We will continue the proof that VTC^0 + IMUL includes open induction in the language of ordered rings. In this second part of the talk, I will finish the computations involved with the formalization of the Lagrange inversion formula, and then I will give a model-theoretic argument using some properties of valued fields to establish the main result.

• 10th June - Mikoláš Janota, "On Propositional QBF Expansions and Q-Resolution" - Quantified Boolean formulas (QBFs) naturally extend propositional logic with quantification and thus providing higher expressivity at the cost of higher complexity---deciding a QBF is PSPACE-complete. Just as resolution serves as a basis of modern SAT solvers, Q-resolution is the basis for DPLL-based QBF solvers. However, there are competitive QBF solvers that solve a given formula by eliminating all but one quantifier, which is solved by a SAT solver. Inspired by this approach, we define a proof system for QBF, which expands all universal quantifiers by rewriting them to conjunctions. The resulting formula is then refuted by propositional resolution. We will show that such system p-simulates tree Q-resolution. In the opposite direction we will show that Q-resolution p-simulates a certain fragment of our proof system. We conclude by showing certain formulas that hint towards an incomparability of the two systems.

• 7th October - Neil Thapen, "The weak pigeonhole principle over T^1_2 and a random restriction" - I will discuss some recent work related to a long-standing problem about the strength of the bounded arithmetic hierarchy. The problem is this: the theory T^i_2 has induction for \Sigma^b_i (that is, bounded \Sigma_i) formulas. Are strictly more \forall \Sigma^b_1 sentences provable in T^{i+1}_2 than in T^i_2? It is open for all i >= 2. Recently some separations have been shown for theories slightly weaker than T^2_2, involving the weak pigeonhole principle and related to Jerabek's theories of approximate counting. I will describe some joint work with Albert Atserias where we show that T^1_2 plus the surjective weak pigeonhole principle for polynomial time functions does not prove a certain \forall \Sigma^b_1 sentence HOP. HOP, roughly speaking, asserts that every total order on a bounded interval must have a least element. The result follows from a purely complexity-theoretic lemma where we show that a certain decision tree, representing the computation of a polynomial time machine with an oracle for an ordering, is drastically simplified under a randomly chosen partial ordering. Since there are likely to be people in the audience who are not familiar with bounded arithmetic, I will begin slowly with an introduction to the area and the problem.

• 14th October - Neil Thapen, "The weak pigeonhole principle over T^1_2 and a random restriction", Part 2

• 21st October - Barnabás Farkas, "The extended Cichon's diagram" -This talk will cover some nice and not very difficult ideas about how to prove inequalities between interesting cardinal invariants of ideals using Galois-Tukey connections, and some motivations of and partial results on open problems.

• 4th November - Nicola Galesi, "Space Lower Bounds for Random Formulae in Algebraic Proof Systems" - The study of space measure in Proof Complexity has gained in the last years more and more importance: first it is clearly of theoretical importance in the study of complexity of proofs; second it is connected with SAT solving, since it might provide theoretical explanations of efficiency or inefficiency of specific Theorem Provers or SAT-solvers; finally it is connected with important characterizations studied in Finite Model Theory, thus providing a solid link between the two research fields. In the talk we will present recent work where we devise a new general combinatorial framework for proving space lower bounds in algebraic proof systems like Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR). Our method can be viewed as a Spoiler-Duplicator game, which is capturing boolean reasoning on polynomials. Hence, for the first time, we move the problem of studying the space complexity for algebraic proof systems in the range of 2-players games, as is the case for Resolution. This can be seen as a first step towards a precise characterization of the space for algebraic systems in terms of combinatorial games, like Ehrenfeucht-Fraisse, which are used in Finite Model Theory. A simple application of our method allows us to obtain all the currently known space lower bounds for PCR, like the Pigeonhole Principle. But more importantly, using our approach in its full potentiality, we answer the open problem of proving space lower bounds in Polynomial Calculus and Polynomials Calculus with Resolution for the polynomial encoding of randomly chosen $k$-CNF formulas. Our method also applies to the well studied Graph Pigeonhole Principle which is a Pigeonhole principle over a constant (left) degree bipartite expander graph. In the talk we will discuss a number of open problems which arise from our works which might be solved generalizing our approach Joint Work with Ilario Bonacina.

• 11th November - Ilario Bonacina, "Proof of Space: an application of Pebbling Games to Cryptography" - In the context of delegation of computation a delegator outsources to a worker the computation of a function f on a certain input x. The delegation problem can be described as follows: the worker computes y=f(x) and proves to delegator, using an interactive proof systems, that indeed y=f(x). Killian showed, using the PCP Theorem, that we can rule out malicious workers provided that they are computationally bounded. What happens if we are just interested to force the worker to carry on a space consuming computation? This means that, with high probability, delegator will accept as valid answers a variety of possible answers all of them space consuming. Clearly using the PCP theorem is an overkill. We propose a model for this problem, that we called Proof-of-Space, and we provide a direct interactive protocol that solve that problem. The protocol ultimately is based on the graph labeling problem, pebbling games and super-concentrator graphs. In particular, as we allow the worker to lie (a bit) we devise a variation of the standard Pebbling Game on graphs to model this behaviour. This is based on a joint work with: Giuseppe Ateniese, Antonio Faonio and Nicola Galesi.

• 18th November - David Chodounský, "The Katowice Problem" - Let P(A)/fin denote the powerset of A modulo the ideal of finite sets. The question whether P(A)/fin can be isomorphic (as a Boolean algebra) to P(B)/fin even if the cardinalities of A and B are different has been resolved for sets of all cardinality except Aleph_0 and Aleph_1. This remaining unsolved instance of this question is called The Katowice Problem. The talk will present basic set theoretic ideas, the reduction of the general question to the Katowice Problem and, time permitting, some partial results on the Katowice Problem.

• 25th November - Jan Krajíček, "A reduction of proof complexity to computational complexity for AC^[p] Frege systems", Part 1 - I will describe an application of the Razborov-Smolensky approximation method to proof complexity, offering a reduction of lengths-of-proofs questions for AC^0[p] Frege systems to computational complexity problems.

• 2nd December - Jan Krajíček, "A reduction of proof complexity to computational complexity for AC^[p] Frege systems", Part 2

• 16th December - Matatyahu Rubin, "The complete theory of every locally moving group is undecidable" - Definition: (a) Let X be a regular space and G be a group of auto-homeomorphisms of X. G is said to be a locally moving group for X, if for every nonempty open U \subseteq X, there is g \in G \ {Id} such that g \upharpoonright (X \ U) = Id. (b) A group H is called a locally moving group, if there are a regular space X and a locally moving group G for X such that H \cong G. Examples: The following groups are locally moving. (1) The group of auto-homeomorphisms of any nonempty open subset of any normed space. (2) The Thompson Group = The group of all piecewise linear homeomorphisms g of [0, 1] such that every slope of g is an integral power of 2, and every break-point of g is a dyadic number. (3) The automorphism group of the binary tree. (4) The group of measure preserving automorphisms of the quotient algebra of the Borel field of [0, 1] over the ideal of measure 0 sets. Theorem: The complete theory (in the language of groups of course) of every locally moving group is undecidable.

• 13th January 2014 - Neil Thapen, "Total space in resolution" - I will talk about some ongoing work with Ilario Bonacina and Nicola Galesi. Consider how a resolution refutation of a formula F could be presented on a blackboard with limited space. At every step in the presentation, the blackboard contains a set of clauses. Initially the board is empty, and at each step we either: write down a clause from F; write down a clause derived by the resolution rule from two clauses already on the board; or erase a clause from the board, in order to free the space for later use. The refutation is finished when we are able to write down the empty clause. The total space of the refutation is defined to be the minimal size of blackboard needed to present it in this way. That is, it is the maximum, taken over all steps i in the presentation, of the sum of the number of symbols in every clause on the board in step i. We will show that some standard constant-width CNFs require total space Omega(n^2). This is an optimal lower bound (up to the constant factor). In particular we will show that there is a constant c>0 such that at some point the blackboard must contain at least cn clauses each of width at least cn.

• 5th February - Sean Walsh, "Fragments of Arithmetic via Type-Lowering Operators" - Frege's Theorem says that second-order Peano arithmetic is mutually interpretable with full second-order comprehension and Hume's Principle, a type-lowering operator from second-order objects to first-order objects that sends second-order objects of the same cardinality to the same object. The work of Burgess, Heck, and others shows that when we reduce full second-order comprehension to first-order comprehension, we may still interpret Robinson's Q. The main aim of this talk is to present our result (in section 4.3, Corollary 92 p. 1704 of the below paper), that when we reduce full second-order comprehension to predicative comprehension (Delta^1_1 comprehension), our theory is strictly below first-order Peano arithmetic in interpretability strength. The exact strength of this system seems still open. Related questions can be asked by considering other type-lowering operators.

• 7th February - Pavel Pudlák, "A presentation of Martin's proof of Borel determinacy", Part 1 - Countably infinite games are, in general, not determined - there are games in which neither player has a winning strategy. A classical result of Martin shows that every game whose payoff set is Borel is determined. Recently Gowers proposed to use finite versions of the concepts involved in Martin's proof to solve the P vs. NP problem. Although it is not clear if this approach is likely to make a progress in the P vs. NP problem, it is worthwhile to recall Martin's proof.

• 3rd March - Pavel Pudlák, "A presentation of Martin's proof of Borel determinacy", Part 2

• 10th March - Ján Pich, "The PCP theorem in Bounded Arithmetics", Part 1 - We will prove the exponential PCP theorem in the theory APC_1, the PCP theorem in PV_1, assuming certain facts about (n,d,\lambda)-graphs, and will discuss the possibility of deriving the PCP theorem in S^1_2 unconditionally.

• 31st March - Jaroslav Nešetřil, "Structural limits - a unified approach" - We present a unified framework for limits of dense and sparse families of graphs together with a concept of modelling. This has been applied to limits of trees and graphs with bounded tree depth, as the first "intermediate classes" with known limit analysis. Joint work with Patrice Ossona de Mendez (Paris).

• 7th April - Petr Glivický, "Fermat's Last Theorem and Catalan's conjecture in Weak Exponential Arithmetics" - Wiles's proof of Fermat's Last Theorem (FLT) has stimulated a lively discussion on how much is actually needed for the proof. Despite the fact that the original proof uses set-theoretical assumptions unprovable in Zermelo-Fraenkel set theory with axiom of choice (ZFC), it is widely believed that much less is needed in principle. Harvey Friedman even conjectured that Fermat's Last Theorem is provable in so called elementary function arithmetic (EFA) (which is just I\Sigma_0 + "2^x is total" in a different language). Smith has showed that EFA proves Fermat's Last Theorem for some small even exponents n (e.g. for n = 4, 6, 10). On the other hand Shepherdson and recently Kolodziejczyk constructed models of IOpen and T^0_2 respectively, where FLT does not hold for n=3. I will present a joint work with Vítězslav Kala. We consider structures and theories in the language L^e=(0,1,+,*,e,<), where the symbol e is intended for a (partial or total) binary exponential. We show that FLT for e is not provable in the L^e-theory Th(N)+Exp, where Th(N) stands for the complete theory of the structure N=(N,0,1,+,*,<) and Exp is a natural set of (rather weak) axioms for e (consisting mostly of elementary identities). In more detail -- we construct a model (B,e) of Th(N)+Exp and its substructure (A,e) with e total and A model of Presburger arithmetic such that in both (B,e) and (A,e) the FLT for e is violated by cofinally many exponents n and cofinally (in all coordinates) many pairwise linearly independent triples a,b,c. On the other hand, under the assumption of ABC conjecture (in N), we show that the Catalan conjecture for e ("the only solution of e(a,n)-e(b,m)=1 with a,b,m,n>1 is a=m=3, b=n=2") is provable in Th(N)+Exp (even in a weaker theory) and thus holds in (B,e) and (A,e). This gives an interesting separation of the strengths of the two famous Diophantine problems.

• 28th April - Ján Pich, "The PCP theorem in Bounded Arithmetics", Part 2

• 5th May - Ján Pich, "The PCP theorem in Bounded Arithmetics", Part 3

• 12th May - Ján Pich, "The PCP theorem in Bounded Arithmetics", Part 4

• 19th May - Michal Garlík, "A restricted ultrapower construction of models of bounded arithmetic" - I will present a construction of a model of S^1_2 which resembles the ultrapower, except that we will not need an ultrafilter nor a full power. We will utilize it to derive a version of Buss's witnessing theorem and discuss its possible further use.

• 26th May - Pavel Pudlák, "On the complexity of finding falsifying assignments for Herbrand disjunctions" - Suppose that $\Phi$ is a consistent sentence. Then there is no Herbrand proof of $\neg \Phi$, which means that any Herbrand disjunction made from the prenex form of $\neg \Phi$ is falsifiable. We show that the problem of finding such a falsifying assignment is hard in the following sense. For every total polynomial search problem $R$, there exists a consistent $\Phi$ such that finding solutions to $R$ can be reduced to finding a falsifying assignments to Herbrand disjunctions made from $\neg \Phi$.

• 24th June - Leszek Kołodziejczyk, "Categorical characterizations of the natural numbers require primitive recursion" - Simpson and Yokoyama studied the reverse-mathematical strength of categoricity theorems for various second-order characterizations of the natural numbers. They showed that categoricity of the usual second-order Peano axioms is equivalent to WKL_0, but other reasonable characterizations are provably categorical already in RCA_0. On the other hand, they were not able to find a characterization that would be provably categorical in RCA*_0, a theory which differs from RCA_0 in that \Sigma_1 induction is replaced by B\Sigma_1 plus exponentiation. Thus, they left the existence of such a characterization as an open problem. We show that no second-order sentence can characterize the natural numbers provably in RCA*_0. On the other hand, it is possible to find a characterization by means of a definable set of second order sentences. Additionally, it is possible to find a single-sentence characterization provably categorical in a \Pi^1_1-conservative extension of RCA*_0, though any such characterization has to be inconsistent with Weak König's Lemma. Work joint with Keita Yokoyama.

• 20th October - Neil Thapen, "A trade-off between length and width in resolution" - We describe a family of CNF formulas in n variables, with small initial width, which have polynomial length resolution refutations. By a result of Ben-Sasson and Wigderson it follows that they must also have narrow resolution refutations, of width O(\sqrt{n log n}). We show that, for our formulas, this decrease in width comes at the expense of an increase in size, and any such narrow refutations must have exponential length. The formulas express the coloured polynomial local search principle, a form of reflection for resolution.

• 27th October - Neil Thapen, "A trade-off between length and width in resolution", Part 2

• 3rd November - Amir Tabatabai, "Constructive Feasible Arithmetic" - The approach of Bounded arithmetic is based on the idea of some reasonable fragmentation of the hierarchies of the axioms like the induction hierarchy to capture the behavior of the feasible part of arithmetic. Therefore, bounded arithmetic is some kind of approximation of feasible arithmetic by our classical arithmetic. In this talk we argue that this approach of fragmentation doesn’t work quite well, since there is some kind of intrinsic infeasibility in classical logic that is the core of the approach. Then, we formalize a theory called Constructive Feasible Arithmetic, which consists of all arithmetical sentences with constructive and feasible proofs. Despite of the approach of bounded arithmetic, this approach tries to study feasible part of arithmetic based on its own structural behavior as a whole and not just by approximation. We will investigate the metamathematical properties of the system and its relationship with the approach of bonded arithmetic on the one hand and the well-known conjectures of the theory of computational complexity on the other. In fact, we will show that with this extreme condition of constructiveness, how much mathematics can be reconstructed.

• 10th November - Petr Glivický, "Definability in (discretely) ordered integrally divisible modules" - An ordered R-module M with a distinguished element 1 > 0 is called integrally divisible if for each scalar 0 < r in R, any m from M can be divided by r with a remainder (i.e. m = rn + i for some n, i from M with 0 <= i < r1). I show that all definable sets in such a module M are "protoperiodic" and therefore M satisfies quantifier elimination up to bounded formulas. This result is particularly interesting if understood in a wider context of model theory of linear arithmetics. I will try to give a brief survey of this arithmetical background.

• 24th November - Petr Glivický, "Definability in (discretely) ordered integrally divisible modules", Part 2

• 1st December - Mateus de Oliveira Oliveira, "On the Parameterized Complexity of Equational Logic" - In this work we study the validity problem in equational logic under the perspective of parameterized complexity theory. First we introduce a variant of equational logic in which sentences are pairs of the form $(t_1=t_2,\omega)$ where $\omega$ is an arbitrary ordering of the positions corresponding to subterms of $t_1$ and $t_2$. We call such pairs {\em ordered equations}. To each ordered equation one may naturally associate a notion of width and to each proof of validity of an ordered equation one may naturally associate a notion of depth. We define the width of such a proof to be the maximum width of an ordered equation occurring in it. Finally, we introduce a parameter $b$ which restricts the way in which variables are substituted for terms. We say that a proof is $b$-bounded if all substitutions used in it satisfy such restriction. In a surprising result, we show that one may determine whether an ordered equation $(t_1=t_2,\omega)$ has a $b$-bounded proof of width $c$ and depth $d$ from a finite set of axioms $E$, in time $f(E,d,c,b)\cdot |t_1=t_2|$. In other words this task is fixed parameter linear with respect to the depth, width and bound of the proof. ... In view of the expressiveness of equational logic, our results give new fixed parameter tractable algorithms to a whole spectrum of problems, such as polynomial identity testing, program verification, automatic theorem proving and the validity problem in undecidable equational theories.

• 8th December- Emil Jeřábek, "Recursive functions meet existentially closed structures" - Robinson's theory R, which axiomatizes the true \Sigma_1 sentences, is one of the weakest known essentially undecidable theories. It also has an interesting structural characterization due to Visser, being the strongest locally finite r.e. theory with respect to interpretation. The essential undecidability of R is a consequence of the fact that it can represent all recursive functions, and it is a natural question whether the converse also holds: i.e., does every r.e. theory that represents all (partial) recursive functions interpret R? The answer is negative, and more generally, R is not interpretable in any consistent theory axiomatized by existential sentences. The explanation comes from model theory. Generalizing the theory of random relational structures (graphs), we will show that for an arbitrary language L (even with functions), the empty L-theory has a model completion EC_L: i.e., EC_L has quantifier elimination, and every L-structure extends to a model of EC_L, so that models of EC_L are exactly the existentially closed L-structures. Furthermore, EC_L is not entirely wild in terms of classification theory: it eliminates \exists^\infty, and it has the no strict order property, even NSOP_3. (However, unlike the theory of the random graph, it is neither simple nor \omega-categorical, and it has the tree property TP_2.) Consequently, various locally finite theories, such as partial orders with arbitrarily long chains, are not interpretable in any consistent existentially axiomatized theory.

Programme archive for 2008 - 2011