-
Wieslaw Kubis
-
(Institute of Mathematics)
-
The weak amalgamation property and infinite games, part 2
- Abstract:
-
I will present a generalization of the Fraisse theory of universal homogeneous structures, where the crucial amalgamation property is replaced by a much weaker condition. I will characterize the new Fraisse limits by the existence of a winning strategy in a very natural game in which two players alternately choose finitely generated structures, building an infinite chain. One of the players wins if the union of this chain is isomorphic to a specific, chosen in advance, structure. This is joint work with A. Krawczyk (University of Warsaw).
-
Wieslaw Kubis
-
(Institute of Mathematics)
-
The weak amalgamation property and infinite games
- Abstract:
-
I will present a generalization of the Fraisse theory of universal homogeneous structures, where the crucial amalgamation property is replaced by a much weaker condition. I will characterize the new Fraisse limits by the existence of a winning strategy in a very natural game in which two players alternately choose finitely generated structures, building an infinite chain. One of the players wins if the union of this chain is isomorphic to a specific, chosen in advance, structure.
This is joint work with A. Krawczyk (University of Warsaw).
-
Stefan Dantchev
-
(Durham University)
-
Tseitin contradictions on weak expanders
- Abstract:
-
Tseitin contradictions, which are certain inconsistent linear systems modulo two, have the distinction of being the earliest formulae shown to be provably hard for a propositional proof system, regular resolution, back in 1986. Since then, stronger results have been proven, culminating in two incomparable lower bounds for bounded-depth Frege proofs of the Tseitin contradictions based on expander graphs.
We generalise both lower bounds to the case of “weak expanders”, i.e. (families of) graphs that are not expanders but are of unbounded tree-width. We first look at Tseitin formulae on square grids and reduce them to both bijective pigeon-hole principle and Tseitin formulae on expanders. This implies, via a standard result from (effective) graph theory, that both lower bounds above, known in case of expanders, also hold for weak expanders. Since our reductions do not apply to resolution (and it is unlikely that there is a reduction that does), we provide a different proof of a tight lower bound in this case. The argument is a randomised adversary argument against a resolution refutation.
Finally, we discuss how one might prove similar lower bounds for matching formulae based on weak expanders.
-
Michal Garlík
-
(Institute of Mathematics)
-
Some subsystems of constant depth Frege with parity, part 2
- Abstract:
-
I shall discuss three families of subsystems of AC^0[2]-Frege for which exponential lower bounds on proof size are known. The strongest of these families of subsystems is a version of systems introduced by Krajíček which we call PK^{c}_{d}(\oplus). Lines in a PK^{c}_{d}(\oplus)-proof are cedents in which all formulas have depth at most d, parity connectives can only appear as the outermost connectives in formulas, and all but c formulas contain no parity connective at all. Comparing our systems with respect to formulas in De Morgan language, we show e.g. that treelike PK^{c}_{d}(\oplus) is quasipolynomially simulated by constant-depth Frege with parity axioms and that PK^{c}_{d}(\oplus) does not polynomially simulate AC^0[2]-Frege. Joint work with Leszek Ko?odziejczyk.
-
Michal Garlík
-
(Institute of Mathematics)
-
Some subsystems of constant depth Frege with parity
- Abstract:
-
I shall discuss three families of subsystems of AC^0[2]-Frege for which exponential lower bounds on proof size are known. The strongest of these families of subsystems is a version of systems introduced by Krajíček which we call PK^{c}_{d}(\oplus). Lines in a PK^{c}_{d}(\oplus)-proof are cedents in which all formulas have depth at most d, parity connectives can only appear as the outermost connectives in formulas, and all but c formulas contain no parity connective at all. Comparing our systems with respect to formulas in De Morgan language, we show e.g. that treelike PK^{c}_{d}(\oplus) is quasipolynomially simulated by constant-depth Frege with parity axioms and that PK^{c}_{d}(\oplus) does not polynomially simulate AC^0[2]-Frege. Joint work with Leszek Ko?odziejczyk.
-
Pavel Pudlák
-
(Institute of Mathematics)
-
Random resolution refutations, part 2
- Abstract:
-
The definition of random resolution attempts to capture the notion of a resolution refutation that may make mistakes but is correct most of the time. I will prove some upper and lower bounds, and discuss a separation between polylogarithmic width random resolution and quasipolynomial size resolution, which is connected to a question in bounded arithmetic. This is a continuation of Neil Thapen's talk on October 10th.
-
Neil Thapen
-
(Institute of Mathematics)
-
Random resolution refutations
- Abstract:
-
The definition of random resolution attempts to capture the notion of a resolution refutation that may make mistakes but is correct most of the time.
I will prove some upper and lower bounds, and discuss a separation between polylogarithmic width random resolution and quasipolynomial size resolution, which is
connected to a question in bounded arithmetic. Joint work with Pavel Pudlák.
-
Joost Joosten
-
(Universitat de Barcelona)
-
Turing Taylor Expansions of Arithmetical Theories
- Abstract:
-
Analytic functions can be endowed with a Taylor expansion around any given point in its domain. In a sense, one can project an analytical function f on a basis of orthogonal monomials x^n and f can be written as some sum of such monomials. We shall see that for a large class of arithmetical theories T something similar holds. The monomials are replaced by Turing progressions over Elementary Arithmetic and natural theories T can be expressed as the union of these monomials.
However, we only have orthogonality of the monomials on certain intervals. This is not a problem since we can show that any union of monomials is provably equivalent to one in such an interval. These intervals are seen to live in a well-known structure: Ignatiev's universal modal model of the closed fragment of Japaridze's polymodal provability logic GLP. This is very nice and thus, points in Ignatiev's model can be interpreted in various ways: Turing Taylor expansions of natural arithmetical theories, ordinals, natural sequences of iterating end-logarithms on ordinals, and of course, modal formulae. This cross-interpretability powers applicability of these polymodal provability logics which we shall discuss as well.
-
Kristina Hostáková
-
(Charles University)
-
The BSS model and hard to invert real functions
- Abstract:
-
Real numbers are usually represented by various discrete objects such as floating points or partial decimal expansions. This is mainly because the classical computability theory relates to computers which work with discrete data. Nevertheless, for theoretical purposes it is interesting to look at models of computation that deal with real numbers as with objects of unit size. A very natural such model was suggested by Blum, Shub and Smale in 1989.
In this talk, I will describe BSS machines over real numbers and their relationship with classical Turing machines. In addition, I will discuss the question whether there are real functions of one real variable that are easier to compute than to invert by a BSS machine.
-
Šárka Stejskalová
-
(Faculty of Arts, Charles University)
-
Woodin solution(s) of CH
- Abstract:
-
The continuum hypothesis says that any subset of the real numbers is at most countable or has the same size as the set of all real numbers. By the results of Godel and Cohen this hypothesis is independent over ZFC if ZFC is consistent. In the talk we focus on the atempt of Woodin to solve CH in the sense of finding a natural theory extending ZFC which decides CH.
-
Jan Pich
-
(University of Leeds)
-
Gentzen and Frege systems for QBF
- Abstract:
-
Recently Beyersdorff, Bonacina, and Chew [1] introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. We provide a comprehensive analysis of the new extended Frege systems from [1], denoted EF+$\forall$-red, which is a natural extension of classical extended Frege EF. Our main results are the following: Firstly, we prove that the standard Gentzen-style system $G_1^*$ p-simulates EF+$\forall$-red and that $G_1^*$ is strictly stronger under standard complexity-theoretic hardness assumptions. Secondly, we show a correspondence of EF+$\forall$-red to bounded arithmetic: EF+$\forall$-red can be seen as a nonuniform propositional version of intuitionistic $S^1_2$. Specifically, intuitionistic $S^1_2$ proofs of arbitrary statements in prenex form translate to polynomial-size EF+$\forall$-red proofs, and EF+$\forall$-red is in a sense the weakest system with this property. Finally, we show that superpolynomial lower bounds for EF+$\forall$-red would imply either $PSPACE \notin P/poly$ or superpolynomial lower bounds for classical EF, and in fact the converse implication holds as well. Therefore, the system EF+$\forall$-red naturally unites the central problems from circuit and proof complexity. Technically, our results rest on a formalized strategy extraction theorem for EF+$\forall$-red akin to witnessing in intuitionistic $S^1_2$ and a normal form for EF+$\forall$-red proofs.
-
Martin Escardo
-
(University of Birmingham)
-
Univalent Type Theory
- Abstract:
-
I will try to explain Voevodsky's univalence axiom as rigorously as I can in the given amount of time. This requires an explanation of Martin-L?f type theory. In particular, Martin-L?f's identity types and universes. Voevodsky's univalence axiom postulates a property of the identity types of universes in Martin-L?f type theory, with a model in homotopy theory.
-
Arnold Beckmann
-
(Swansea University)
-
Provably total NP search problems in strong theories
- Abstract:
-
The class of total NP search problems has been identified by Megiddo and Papadimitriou in the beginning of the 1990ies, who denoted this class TFNP. Total NP search problems whose totality can be proven within a mathematical theory, denoted provably total NP search problems, play an important role in the study of Bounded Arithmetic theories and related questions.
In this talk, I will present characterisations of the provably total NP search problems of strong theories like Peano Arithmetic, and a general research programme related to this.
-
Amir Tabatabai
-
(Institute of Mathematics)
-
Provability Interpretation of Propositional and Modal Logics, Part 2
- Abstract:
-
In 1933, Godel introduced a proof interpretation for propositional intuitionistic logic (IPC). The idea was translating IPC into another calculus (S4) which is a formalization of the concept of intuitive provability. Unfortunately, this approach does not introduce any kind of concrete proof interpretations. In fact, Godel himself showed that any naive interpretation would contradict with his second incompleteness theorem. After Godel, finding a concrete proof interpretation for S4 has been an open problem for years and leads to different fields like provability logics and logic of proofs.
In this talk, we intend to introduce a framework for concrete interpretations which leads to a generalization of Solovay's arithmetical interpretation and we will show that these natural interpretations capture different modal logics like K4, KD4, GL and S4. Moreover, we will show that there is not any provability interpretation for S5 as we expected from our informal interpretation of the provability predicate. In addition, we will use these results to propose a class of provability interpretations for propositional logics like Basic and Intuitionistic logics and also to show that classical logic does not admit any provability interpretation.
-
Amir Tabatabai
-
(Institute of Mathematics)
-
Provability Interpretation of Propositional and Modal Logics
- Abstract:
-
In 1933, Godel introduced a proof interpretation for propositional intuitionistic logic (IPC). The idea was translating IPC into another calculus (S4) which is a formalization of the concept of intuitive provability. Unfortunately, this approach does not introduce any kind of concrete proof interpretations. In fact, Godel himself showed that any naive interpretation would contradict with his second incompleteness theorem. After Godel, finding a concrete proof interpretation for S4 has been an open problem for years and leads to different fields like provability logics and logic of proofs.
In this talk, we intend to introduce a framework for concrete interpretations which leads to a generalization of Solovay's arithmetical interpretation and we will show that these natural interpretations capture different modal logics like K4, KD4, GL and S4. Moreover, we will show that there is not any provability interpretation for S5 as we expected from our informal interpretation of the provability predicate. In addition, we will use these results to propose a class of provability interpretations for propositional logics like Basic and Intuitionistic logics and also to show that classical logic does not admit any provability interpretation.
-
Yiannis N. Moschovakis
-
(UCLA and University of Athens)
-
Intrinsic complexities
- Abstract:
-
Sample result (without the precise definitions):
Proposition. For every first order structure
M = (U_M,c_1,...,R_1,..., f_1,...)
and every n-ary relation R(x) on the universe U_M of M, there is
a function
C_R : U_M^n --> {0,1,..., infty}
with the following properties:
(1) If C_R(x) = 0 for some tuple x of distinct elements,
then R is constant on U_M^n.
(2) If \alpha is any (deterministic or non-deterministic) algorithm
which decides R from the primitives of M, then for every x,
C_R(x)
-
Anna Horská
-
(Institute of Mathematics)
-
Gentzen's cut elimination strategy and Tait's cut elimination strategy in propositional sequent calculus
- Abstract:
-
Nowadays, we usually eliminate cuts by decreasing the cut-rank of the derivation (Tait's strategy). That is, a cut with the greatest complexity is chosen such that there are only smaller cuts above it and this one is then decomposed into smaller cuts. Gentzen applies another strategy in his article of 1935. He eliminates the highest cuts, i.e., cuts that there are no other cuts above them. Hence, this procedure does not pay attention to the complexity of the chosen cut. The main property of cut elimination that we are interested in is the growth of the height of the derivation during the elimination, especially we want to know the height of the cut-free derivation. I want to show that both strategies mentioned above give us the same cut-free derivation in propositional logic. Not only is the height of the cut-free derivations the same, but they also have the same structure. I will define a procedure for eliminating a single cut (according to Buss) which makes global changes to a derivation. Then, I use Church-Rosser property to obtain that cut-free derivations are unique, when the only difference during the elimination is the way we choose the next cut to eliminate.
-
Raheleh Jalali
-
(Mathematical Institute)
-
No Feasible Interpolation for TC^0-Frege Proofs
- Abstract:
-
This is a paper by M.L.Bonet, T.Pitassi and R.Raz from 1997. The interpolation method has been one of the main tools for proving lower bounds for propositional proof systems. Loosely speaking, if one can prove that a particular proof system has the feasible interpolation property, then a generic reduction can (usually) be applied to prove lower bounds for the proof system, sometimes assuming a (usually modest) complexity-theoretic assumption. In this paper, we show that this method cannot be used to obtain lower bounds for Frege systems, or even for TC^0-Frege systems. More specifically, we show that unless factoring is feasible, neither Frege nor TC^0-Frege has the feasible interpolation property. In order to carry out our argument, we show how to carry out proofs of many elementary axioms/theorems of arithmetic in polynomial-size TC^0-Frege. In particular, we show how to carry out the proof for the Chinese Remainder Theorem, which may be of independent interest. As a corollary, we obtain that TC^0-Frege as well as any proof system that polynomially simulates it, is not automatizable (under a hardness assumption).
Pavel Pudlak, Neil Thapen, Jan Krajíček
organizers