•  
    • Emil Jerabek
    • (ASCR)
    • Recursive functions meet existentially closed structures, Part 2
    • Abstract:
    • 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.
    • 15.12.14   13:30
    • Emil Jerabek
    • (ASCR)
    • Recursive functions meet existentially closed structures
    • Abstract:
    • 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.
    • 08.12.14   13:30
    • Mateus de Oliveira Oliveira
    • (Institute of Mathematics ASCR)
    • On the Parameterized Complexity of Equational Logic
    • Abstract:
    • 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. Subsequently, we restrict ourselves to what we call {em oriented proofs}, where the order of a term is always smaller than the order of its subterms. We show that given a classical equation $t_1=t_2$, one may determine whether there exists an ordering $omega$ such that $(t_1=t_2,omega)$ has a $b$-bounded oriented proof of depth $d$ and width $c$ in time $f(E,d,c,b)cdot |t_1= t_2|^{O(c)}$. In other words this task is fixed parameter tractable with respect to the depth and bound of the proof, and is in polynomial time for constant values of width. Observe that this last result is particularly interesting because the ordering $omega$ is not given a priori, and thus, we are indeed parameterizing the provability of equations in classical equational logic. 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.
    • 01.12.14   13:30
    • Petr Glivicky
    • Definability in (discretely) ordered integrally divisible modules
    • Abstract:
    • 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
    • 24.11.14   13:30
    • Petr Glivický
    • (Institute of Mathematics)
    • Definability in (discretely) ordered integrally divisible modules
    • Abstract:
    • 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
    • 10.11.14   13:30
    • Ján Pich
    • (Charles University)
    • The PCP theorem in Bounded Arithmetics, Part 2
    • Abstract:
    • 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.
    • 28.04.14   13:30
    • Petr Glivický
    • (Institute of Mathematics, AS CR)
    • Fermat's Last Theorem and Catalan's conjecture in Weak Exponential Arithmetics
    • Abstract:
    • 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 ISigma_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,
    • 07.04.14   13:30
    • Ján Pich
    • (Charles University)
    • The PCP theorem in Bounded Arithmetics
    • Abstract:
    • 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.
    • 10.03.14   13:30

    Pavel Pudlak, Neil Thapen, Jan Krajíček
    organizers

  •