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 , 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 .
This is a joint work with Makoto Fujiwara, Hajime Ishihara, Takako Nemoto and Nobu-Yuki Suzuki.
 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).
 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
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.
 S. Alexander, R. Bishop and R. Ghrist, 'Total curvature and simple pursuit on domains of curvature bounded above', Geom. Dedicata 149 (2010) 275--290.
 U. Kohlenbach, G. López-Acedo and A.Nicolae, A quantitative analysis of the “Lion-Man'' game (submitted).
 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
 G. López-Acedo, A. Nicolae, B. Piatek, "Lion-Man'' and geodesic rays (in progress).
 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
Friday, February 9, 2018, in S2|15-201, at 13:30|
Dr. Florian Steinberg, INRIA
type-two poly-time and length revisions
“We present a new, and fairly simple characterization of the type-two poly-time computable functionals. While being machine based, it avoids the use of higher order objects as running times and instead uses an approach first put forward by Cook that sticks to first order functions to formulate time constraints. Cook's class is known to not only contain feasible operations and we thus impose further restrictions. The purpose of these restrictions is very simple: It is to avoid unbounded iteration of functional input. We prove that this leads to a subclass of all feasible functionals and that closing under composition leads back to the class of all feasible functionals. We also prove that the same is true for a more restrictive condition, namely for the notion of strong poly-time.”
This is joint work with Bruce Kapron.
Friday, February 2, 2018, in S2|15-201, at 13:30|
Dr. Adriana Nicolae, University of Seville
“Lion Man” and the Fixed Point Property
In this talk we are concerned with the relation between the ?xed point property for continuous mappings and a discrete lion and man game played in a strongly convex domain. Our main result states that in locally compact geodesic spaces or in R-trees, the ?xed point property of the domain is equivalent to the success of the lion. At the end we review a few applications of proof mining in the context of geodesic metric spaces.
This talk is based on a joint work with Genaro López-Acedo (University of Seville) and Bozena Piatek (Silesian University of Technology).
Friday, January 26, 2018, in S2|15-201, at 13:30|
Dr. Andrei Sipos
Contributions to proof mining
I will present the results of my PhD thesis, belonging to the area of proof mining, an applied subfield of mathematical logic. Proof mining (introduced and developed by U. Kohlenbach and his collaborators) aims to obtain quantitative information -- primarily witnesses and bounds for existentially quantified variables -- out of ordinary mathematical proofs of an apparently non-constructive nature. The results under discussion fall naturally within three categories. Firstly, there are some representative applications of such techniques in nonlinear analysis and convex optimization -- the extraction of rates of metastability, asymptotic regularity and even full convergence for some iterations studied in those fields, e.g. the parallel algorithm, the Ishikawa iteration or the proximal point algorithm. Secondly, as this kind of research can easily spill over in related areas, I present some advances in pure analysis, like a characterization of 2-uniformly convex Banach spaces or a general definition that encompasses all the known instances of resolvent operators used in convex optimization. Finally, I present some work in the foundations of proof mining, namely a suitable implicit characterization of the class of L^p spaces that is amenable to a logical treatment, i.e. it allows for a suitable metatheorem that underlies possible applications. This is followed by a derivation of the modulus of uniform convexity for this class of spaces from this axiomatization.
Some of these results are joint work with Laurentiu Leustean and Adriana Nicolae.
Friday, November 3, 2017, in S2|15-201, at 13:30|
Anton Freund, University of Leeds,
From Cut Elimination to Pi^1_1-Comprehension
I will begin with an informal explanation of cut elimination and its use in the ordinal analysis of Peano arithmetic. The latter shows that Pi^0_2-soundness is equivalent to the primitive recursive well-foundedness of an ordinal notation system. On a conceptual level, we observe that the focus is on low logical complexity. Next, I explain how an ordinal notation system can be relativized to a given well-order. This brings us to the level of Pi^1_2-statements. Many well-known axioms of that complexity have been characterized in terms of relativized ordinal notation systems: from arithmetical comprehension (Girard, Hirst) up to the existence of omega-models of bar induction (Rathjen and Vizcaíno). Finally, I present a new result at the next type-level: Following a suggestion by Montalbán and Rathjen, I relativize an ordinal notation system to a relativized ordinal notation system. In this way one can get a characterization of Pi^1_1-comprehension, which is a Pi^1_3-statement (preprint available as arXiv:1704.01662).
Friday, October 6, 2017, in S2|15-201, at 13:30|
Prof. Dr. Martin Ziegler, KAIST School of Computing
Formal Verification in Imperative Multivalued Programming over Continuous Data Types
(joint work with Gyesik Lee, Norbert Müller, Eike Neumann, Sewon Park, and Norbert Preining)
Inspired and guided by the iRRAM C++ library (Müller 2001), we formally specify a programming language for the paradigm of EXACT REAL COMPUTATION: reliably operating on encapsulated CONTINUOUS data types such as (not necessarily algebraic) real numbers --- imperatively and exactly (no rounding errors) with primitives computable in the sense of Recursive Analysis and a necessarily modified multivalued=non-extensional semantics of tests. We then propose a complete logical system over two types, integers and real numbers, for rigorous correctness proofs of such algorithms. We extend the rules of Hoare Logic to support the formal derivation of such proofs, and have them verified in the Coq Proof Assistant. Our approach is exemplified with three simple numerical example problems: integer rounding, solving systems of linear equations, and continuous root finding.
Summer term 2017
Wednesday, September 13, 2017, at 14:00 in S2|15-201|
Continuous enclosures of discontinuous problems
The main theorem of computable analysis asserts that any computable function is continuous. Many interesting problems encountered in practice turn out to be discotinuous, however. It hence is a natural question how much partial information may be obtained on the solutions of a discontinuous problem in a continuous or computable way. To formalise this idea, we propose the notion of continuous enclosures: continuous multi-valued functions which take values in certain semilattices which encode partial information on the solutions of the original problem. We give some existence results and provide some explicit examples.
Friday, July 21, 2017, at 13:30 in S2|15-201|
Julian Bitterlich, TU Darmstadt
Special classes of acyclic groups and their applications
I present some connections between results in monoid theory and in (finite) model theory. More specifically, we look at theorems about the profinite topology on free groups (M. Hall, Ribes and Zalesskii) and compare these to theorems concerning extension problems for partial automorphisms (Hrushovski, Herwig and Lascar). The two threads can be related through a suitable notion of acyclicity in groups, which provides yet another viewpoint on the topic.
Friday, July 7, 2017, at 13:30 in S2|15-201|
Felix Canavoi, TU Darmstadt
A Modal Characterisation Theorem for Common Knowledge Logic
We investigate epistemic modal logic with common knowledge modalities for groups of agents and obtain two van Benthem style model-theoretic characterisation theorems, a classical version and one in the sense of finite model theory. In order to do that we show that basic modal logic is expressively equivalent to the bisimulation invariant fragment of first-order logic over the non-elementary class of so-called (finite) common knowledge Kripke frames. The transitive nature of common knowledge modalities poses a new challenge that cannot be tackled by the usual locality based techniques. For (finite) common knowledge Kripke frames we construct (finite) bisimilar companions that are based on Cayley graphs of suitable groups with specific acyclicity properties. These Cayley graphs possess a very intricate yet highly regular structure that allows for a locality analysis on multiple scales that are induced by distance measures w.r.t. various coalitions of agents.
Friday, June 30, 2017, at 13:30 in S2|15-201|
Prof. Andrey Morozov, Sobolev Institute of Mathematics, Novosibirsk
Infinite time Blum-Shub-Smale machines for computability in analysis
(joint work with Peter Koepke)
We continue the study of the computational strength of infinite time Blum-Shub-Smale machines (ITBM) performing computations over the reals in ordinal time started by P.Koepke and B.Seyfferth. We give a characterization of ITBM-computable functions via iterated Turing jump and discuss the adequacy of this approach to our intuitive imaginations of computability used in analysis.
Friday, June 16, 2017, at 13:30 in S2|15-201|
Prof. Rodney G. Downey, Victoria University of Wellington
Notes on Computability in Mathematics
We look at some recent advances in the understanding of the computational content of mathematics. I will mainly concentrate on problems in and around abelian groups.
Tuesday, April 11, 2017, at 11:00 in S2|15-201|
Michal Konecny, Aston University
Representations for feasibly approximable functions
(joint work with Eike Neumann)
'Exact' continuous real functions can feature as first-class objects in computation in a similar way as so-called exact real numbers. While all natural representations of continuous functions used in computable analysis are computably equivalent, different admissible representations may fail to be equivalent under the polynomial-time reduction defined by Kawamura and Cook (2012). Building on work by Labhalla, Lombardi, and Moutai (2001) and Kawamura, Mueller, Roesnick, and Ziegler (2015), we review several common admissible representations of continuous real functions, study their polynomial-time reducibility lattice and benchmark their performance using AERN, a Haskell library for exact real computation. In particular, we show that rigorous approximation by piecewise polynomials is polynomial-time equivalent to rigorous approximation by rational functions. Each representation of continuous functions offers a trade-off between the ease of computing names of functions (ie writing) and the ease of extracting information about a function (ie reading). We formalise this concept by switching from representations to compositional evaluation strategies over term signatures. A signature includes a set of function operations, some of which just create functions, some read existing functions (eg computing the range) and some do both (eg pointwise addition). We reformulate some existing results about function representations as Pareto optimality with respect to certain signatures. We implemented evaluation strategies based on the chosen representations and we benchmark their performance on a small set of terms.