Logic seminar

Logic seminar talks


Winter term 2019/20

Friday, November 15, 2019, in S2|15-201, at 13:30
Dr. Bruno Dinis, University of Lisbon
Gotta catch 'em all: a parametrised functional interpretation
Since Godel published his functional (“Dialectica”) interpretation in 1958, various other functional interpretations have been proposed. These include Kreisel's modified realizability, the Diller-Nahm variant of the Dialectica interpretation, Stein's family of interpretations, and more recently, the bounded functional interpretation, the bounded modified realizability, and “Herbrandized” versions of modified realizability and the Dialectica. It is then natural to ask how are these different interpretations related to each other and what is the common structure behind all of them.
These questions were addressed by Paulo Oliva and various co-authors in a “unification programme”. Starting with a unification of interpretations of intuitionistic logic, which was followed by various analysis of functional interpretations within the finer setting of linear logic, a proposal on how functional interpretations could actually be combined in the so-called hybrid functional interpretations, and the inclusion of truth variants in the unification. This unification programme has so far been unable to capture the two more recent families of functional interpretations, namely the bounded functional interpretations, and the Herbrandized functional interpretations.
In this talk I will present a more general framework for unifying functional interpretations, based on two families of parameters, one for interpreting the contraction axiom, and another for interpreting typed quantifications, hich allow to include in the unification the more recent bounded and Herbrandized functional interpretations. I will start by presenting this parametrised interpretation in the setting of affine logic. Then, via the two well-known Girard translations from intuitionistic logic into affine logic, one obtains two parametrised interpretations of intuitionistic logic. I will explain how all of the functional interpretations mentioned above can be recovered by suitable choices of these two parameters and how this framework can be used to discover some new interpretations. I will finish with some open questions.
(This is joint work with Paulo Oliva)
Friday, October 25, 2019, in S2|15-201, at 13:30
Dr. Anton Freund, TU Darmstadt
Reflection and induction in set theory
Equivalences between reflection and induction principles are well-known from the context of first and second order arithmetic. In this talk I present an analogous result in set theory: The principle that any true first order formula with real parameters reflects into some transitive set model is equivalent to induction along $\Delta(\R)$-definable well-founded classes, over a suitable weak base theory (see arXiv:1909.00677 for full details).
Tuesday, October 8, 2019, in S2|15-201, at 16:15
Prof. Tatsuji Kawai, Japan Advanced Institute of Science and Technology
The domain of a definable function of intuitionistic arithmetic in all finite types
Brouwer (1927) claimed that every function from the Baire space to the set of natural numbers is induced by a neighbourhood function (or associate) whose domain admits so called bar induction. We show that Brouwer's claim holds for any definable function of the intuitionistic arithmetic in all finite types (HA omega). Our proof does not rely on proof theoretic methods such as normalisation or ordinal analysis. Instead, we internalise in HA omega the dialogue-tree interpretation of Gödel's system T due to Martin Escardo (2013). The interpretation determines a syntactic translation on the terms of HA omega, which yields a neighbourhood function from a closed term of HA omega with the required property.
As applications of this result, we revisit some well-known properties of HA omega: uniform continuity of definable functions the Cantor space; closure under the rule of bar induction; and closure of bar recursion for the lowest type with a definable stopping function.

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

Winter term 2017/18

Summer term 2017