Logic seminar

Logic seminar talks


Summer term 2019

Tuesday, September 17, 2019, in S2|15-244, at 15:00
Dr. Makoto Fujiwara, Institute of Science and Technology, Meiji University
Weihrauch and constructive reducibility between existence statements
We formalize the primitive recursive variants of Weihrauch reduction between existence statements in finite-type arithmetic and show a meta-theorem stating that the primitive recursive Weihrauch reducibility verifiably in a classical finite-type arithmetic is identical with the formal reducibility in the corresponding (nearly) intuitionistic finite-type arithmetic for all existence statements formalized with existential free formulas.
In addition, we demonstrate that our meta-theorem is applicable in some concrete examples from classical and constructive reverse mathematics.
Friday, August 23, 2019, in S2|15-201, at 13:30
Anantha Padmanabha, Institute of Mathematical Sciences, Chennai
Term Modal Logic: Satisfiability problem
Multi-modal logics are ubiquitously used in various fields of theoretical computer science.
Typically, we have formulas of the form □iα where i comes from a fixed finite set of agents
or indices. In dynamic settings like client-server systems; multi-thread processes; large games
etc, the number of agents cannot be fixed a priori, and may even change from state to state.
We are thus led to Term Modal Logic (TML) where we use variables ranging over agent names
and quantification of such variables; the logic has formulas such as ∀x(P(x) → □xα). Thus
TML is a first order logic in which we can talk of agent properties as predicates and also use
modalities to talk of moves by agents. TML bears some interesting relationship with First
Order Modal Logic. As expected, this logic is highly undecidable and we will look at some
tight undecidability results. Further, we will discuss some interesting decidable fragments: the
monodic, the bundled and the two-variable fragments.
This is a joint work with Prof. R. Ramanujam.
Friday, May 3, 2019, in S2|15-201, at 13:30
Prof. em. Adrian R. D. Mathias, LIM, Université de la Réunion
Using generic extensions of ill-founded models of weak set theories to build standard models of the same
Tuesday, April 9, 2019, in S2|15-201, at 13:30
Miroslav Chodil, Masaryk University, Brno
The satisfiability problem for two simple fragments of Probabilistic CTL
PCTL is a probabilistic extension of the popular branching-time logic CTL. It has various practical uses, for example in formalizing behavior of stochastic systems. The problem of determining whether a PCTL formula is satisfiable is not known to be decidable, and has been open for decades. In this talk, we will focus on the satisfiability problem for two simple fragments of PCTL. For the first fragment, we will show that finite satisfiability is decidable. For the second fragment, we will discuss why the situation is perhaps not so simple, despite it being a reasonable extension of a fragment with particularly well-behaved models.
Friday, April 5, 2019, in S2|15-201, at 13:30
Prof. Martin Ziegler, KAIST School of Computing, Daejon
Representation Theory of Compact Metric Spaces and Computational Complexity of Continuous Data
Choosing an encoding over binary strings for input/output to/by a Turing Machine is usually straightforward and/or inessential for discrete data (like graphs), but delicate -- heavily affecting computability and even more computational complexity -- already regarding real numbers, not to mention more advanced (e.g. Sobolev) spaces. For a general theory of computational complexity over continuous data we introduce and justify QUANTITATIVE admissibility as requirement for sensible encodings of arbitrary compact metric spaces, a refinement of qualitative 'admissibility' due to [Kreitz&Weihrauch'85]:
An admissible representation of a T0 space X is a (i) continuous partial surjective mapping from the Cantor space of infinite binary sequences which is (ii) maximal w.r.t. continuous reduction. By the Kreitz-Weihrauch (aka “Main”) Theorem of computability over continuous data, for fixed spaces X,Y equipped with admissible representations, a function f:X→Y is continuous iff it admits continuous a code-translating mapping on Cantor space, a so-called REALIZER. We define a QUANTITATIVELY admissible representation of a compact metric space X to have (i) asymptotically optimal modulus of continuity, namely close to the entropy of X, and (ii) be maximal w.r.t. reduction having optimal modulus of continuity in a similar sense.
Careful constructions show the category of such representations to be Cartesian closed, and non-empty: every compact X admits a linearly-admissible representation. Moreover such representations give rise to a tight quantitative correspondence between the modulus of continuity of a function f:X→Y on the one hand and on the other hand that of its realizer: the MAIN THEOREM of computational complexity. This suggests (how) to take into account the entropies of the spaces under consideration when measuring algorithmic cost over continuous data.
This is joint work with Akitoshi Kawamura, Donghyun Lim, and Svetlana Selivanova.

Winter term 2018/19

Friday, March 8, 2019, in S2|15-201, at 13:30
Prof. Genaro López Acedo, University of Seville
An application of Proof Mining to Game Theory
In this talk we analyze a discrete pursuit-evasion game, based on Rado's lion and man celebrated problem. Using ideas stemming from proof mining, we prove that in uniformly convex bounded domains the lion always wins, and we extract a uniform rate of convergence for the successive distances between the lion and the man.
[1] S. Alexander, R. Bishop and R. Ghrist, 'Total curvature and simple pursuit on domains of curvature bounded above', Geom. Dedicata 149 (2010) 275--290.
[2] U. Kohlenbach, G. López-Acedo and A.Nicolae, A quantitative analysis of the “Lion-Man'' game (submitted).
[3] G. López-Acedo, A. Nicolae, B. Piatek, ”Lion-Man'' and the Fixed Point Property, Geometria Dedicata. https://doi.org/10.1007/s10711-018-0403-9
[4] G. López-Acedo, A. Nicolae, B. Piatek, "Lion-Man'' and geodesic rays (in progress).
[5] J. E. Littlewood, Littlewood's Miscellany (ed: B. Bollobás) (Cambridge University Press, Cambridge 1986).
Friday, February 15, 2019, in S2|15-201, at 13:30
Silke Meißner, TU Darmstadt
Elementary Model-Theoretic Techniques for Inquisitive Modal Logic
Inquisitive modal logic INQML is an extension of modal logic ML, which allows modelling not only statements, but also more complex matters such as questions. We consider INQML from a model-theoretic perspective. A new, efficient standard translation from INQML into first-order logic FO is presented. This standard translation can be used to give a new and purely model-theoretic proof of compactness for INQML.
Tuesday, January 29, 2019, in S2|15-201, at 14:00
Prof. Yong Cheng, Wuhan University, School of Philosopy
Finding the limit of incompleteness for subsystems of PA
Gödel's incompleteness theorem is the most profound and important theorem in foundations of mathematics. There are still some open problems related to incompleteness. In this talk, I will firstly give an overview of the current state of research on incompleteness from different perspectives and classify some misinterpretations of Gödel's incompleteness theorem.
In the second part of the talk, I will focus on the open problem of finding the limit of incompleteness for subsystems of PA. Let T be a recursively axiomatizable consistent theory. We say that G1 holds for T iff for any recursively axiomatizable consistent theory S, if T is interpretable in S, then S is undecidable. It is well known that G1 holds for Robinson's Q and its sub-theory R. I examine the following question: whether there exists a theory with the minimal degree of interpretability for which G1 holds. As the first step toward this question, a natural question is: could we find a theory T such that G1 holds for T and the interpretation degree of T is less than the interpretation degree of R (i.e. R interprets T, but T does not interpret R). I will talk about some recent progress on these questions as well as some open questions.
Friday, November 23, 2018, in S2|15-201, at 13:30
Prof. Anuj Dawar, University of Cambridge
Definable Inapproximability: New Challenges for Duplicator
We consider the hardness of approximation of optimization problems from the point of view of definability. For many NP-hard optimization problems it is known that, unless P =3D NP, no polynomial-time algorithm can give an approximate solution guaranteed to be within a fixed constant factor of the optimum. We show, in several such instances and without any complexity theoretic assumption, that no algorithm that is expressible in fixed-point logic with counting (FPC) can compute an approximate solution. Since important algorithmic techniques for approximation algorithms (such as linear or semidefinite programming) are expressible in FPC, this yields lower bounds on what can be achieved by such methods. The results are established by showing lower bounds on the number of variables required in first-order logic with counting to separate instances with a high optimum from those with a low optimum for fixed-size instances.
This is joint work with Albert Atserias (Barcelona)

Winter term 2017/18

Summer term 2017