Logic seminar

Logic seminar talks


Winter term 2019/20

C A N C E L L E D : March 25
Prof. Dag Normann, University of Oslo
The Skolem paradox and higher order computability models
The non-paradoxical fact that there is a countable elementary substructure of the continuum is sometimes referred to as “Skolem's paradox”. This non-paradox gives us much freedom in constructing higher-order models where the independence of classical mathematical theorems from second order arithmetics can be shown.
In this talk we will see how methods from higher order computability theory can be applied to construct a plethora of models giving examples of theorems, simple from the point of view of undergraduate students, that cannot be proved in full second order number theory in conjunction with strong recursion principles like those in Gödel's T.
Friday, February 21, in S2|15-201, at 13:30
Prof. Keita Yokoyama, Japan Advanced Institute of Science and Technology
Kripke models of HA and separations of non-constructive principles
In [1], Akama/Berardi/Hayashi/Kohlenbach gave separations of non-constructive principles such as LPO LLPO over Heyting arithmetic by using several different methods. In this study, we will try to find a uniform technique with Kripke models to separate those principles. For this, we sharpen Smorynski's construction for the refinement of de Jongh's theorem in [2].
This is a joint work with Makoto Fujiwara, Hajime Ishihara, Takako Nemoto and Nobu-Yuki Suzuki.
[1] Yoji Akama, Stefano Berardi, Susumu Hayashi and Ulrich Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles. In: Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS?04), pp. 192-201, IEEE Press (2004).
[2] Craig A. Smorynski, Applications of Kripke models, Metamathematical investigation of intuitionistic arithmetic and analysis, pp. 324?391, Lecture Notes in Mathematics, Vol. 344, Springer, Berlin, 1973.
Friday, February 14, in S2|15-201, at 13:30
Prof. Kirstin Peters, TU Darmstadt
Session Types for Fault-Tolerant Distributed Algorithms
We strive to use session type technology to prove behavioural properties of fault-tolerant distributed algorithms. Session types are designed to abstractly capture the structure of (even multiparty) communication protocols. The goal of session types is the analysis and verification of the protocols? behavioural properties. One important such property is progress, i.e., the absence of (unintended) deadlock. Distributed algorithms often resemble (compositions of) multiparty communication protocols. In contrast to protocols that are typically studied with session types, they are often designed to cope with faults, like system failures. An essential behavioural property is (successful) fault-tolerant termination, but it is often elaborate to prove for distributed algorithms. We extend multiparty session types to capture faults due to message loss and process crashes. We implement both reliable and unreliable communication and also an unreliable subsession mechanism in types and augment the semantics of processes by failure patterns that can be used to represent system requirements (as, e.g., failure detectors).
Friday, January 31, in S2|15-201, at 15:30
Prof. Peter Schuster, University of Verona
Resolving Finite Indeterminacy. A Definitive Constructive Universal Prime Ideal Theorem
Joint work with Daniel Wessel
Dynamical proofs were designed to eliminate the ideal objects abstract algebra abounds with. Typically those ideal objects are granted by an incarnation of Zorn's Lemma and serve for proving the semantic conservation of additional non-deterministic sequents, that is, with finite but not necessarily singleton succedents. This was possible also because (finitary) coherent or geometric logic predominates in that area: the use of a non-deterministic axiom can be captured by a finite branching of the proof tree. Incidentally, a paradigmatic case has widely been neglected in dynamical algebra: Krull's Lemma for prime ideals. Digging deeper just about that case, which has been settled only recently, we manage to unearth the underlying general phenomenon: Given a concrete claim of computational nature that usually is proved by the semantic conservation of certain additional non-deterministic axioms, there is a finite labelled tree belonging to a suitable inductively generated class which tree encodes the desired computation. Our characterisation works in the the fairly universal setting of a consequence relation enriched with non-deterministic axioms; uniformises most if not all of the known instances of the dynamical method; generalises the proof-theoretic conservation criterion that has been offered before; and last but not least links the syntactical with the semantic approach: every ideal object used for the traditional proof of a concrete claim is the shadow one of the corresponding tree's branches.
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