Seminars

Public defence of Orvar Lorimer Olsson’s Licentiate thesis.

Opponent Assistant Professor Fan Yang, Utrecht University
Examiner Professor Graham E Leigh, Göteborgs universitet

I will introduce the basic framework and look at some of the applications to 1philosophy and linguistics.

Dependence logic extends first-order logic with dependence atoms, which express that the value of a variable is functionally determined by other variables. Team semantics gives dependence logic a second-order flavour, and even quantifier-free dependence logic formulas can have an NP-complete model-checking problem. This motivates the study of syntactic conditions under which model checking becomes tractable.

The talk starts with a brief introduction to team semantics and dependence logic, and then focuses on coherence, a notion introduced by Jarmo Kontinen to capture when the satisfaction of a formula can be determined by satisfaction by its small subteams. We show that, for quantifier-free formulas, coherence is precisely equivalent to first-order rewritability. We also study the complexity of deciding coherence, obtaining strong undecidability results for dependence logic and a precise complexity classification for propositional dependence logic.

The talk is based on joint work with Timon Barlag, Nicolas Fröhlich, Miika Hannula, Phokion G. Kolaitis, Arne Meier, and Jouko Väänänen: https://arxiv.org/abs/2605.31269

The mu-calculus is obtained from basic modal logic by adding least and greatest fixpoint operators. By doing so a lot of expressive power is added to the logic. However, the semantics can only be evaluated over labelled transition systems. Coalgebraic modal logic generalizes the basic modal logic and lets us evaluate the semantics over different coalgebras, instead of only labelled transition systems. In the coalgebraic mu-calculus, the expressive power of the mu-calculus and the generality of coalgebraic modal logic are combined.

In this talk we will introduce the coalgebraic mu-calculus and how to handle proof systems for this family of logics.

The 13th Scandinavian Logic Society Symposium (SLSS 2026) and 6th Nordic Logic Summer School (NLSS 2026) take place this year in Copenhagen under the auspices of the Scandinavian Logic Society on the dates

• Nordic Logic Summer School: 17–20 August, 2026
• Scandinavian Logic Society Symposium: 21–23 August, 2026

The Call for Papers is reproduced below; see the conference website for further details and updates.

We formulate and discuss a general axiomatic theory of arbitrary objects. This theory is expressed in a simple first-order language without modal operators, and it is governed by classical logic. The theory AOT intends to be a fundamental and a fully general (and somewhat flexible) theory of arbitrary objects. Ideally, it intends to be a suitable formal framework for all legitimate applications of arbitrary object theory. According to the proposed theory, arbitrary objects are organised in correlated systems, where each such system of arbitrary objects is abstracted from a system of particular objects.

Faculty Opponent: Associate Professor Michal Skrzypczak, University of Warsaw, Poland

Examining committee: 

• Professor Martin Lange, University of Kassel, Germany
• Associate Professor lsabel Oitavem, NOVA University of Lisbon, Portugal
• Associate Professor Paulo Oliva, Queen Mary University of London, UK
• Professor Eleni Gregoromichelaki, Göteborgs universitet (substitute)

Abstract A fixed point of a function can be described as a special mathematical object, with several powerful applications. This thesis studies fixed points in the context of two distinct frameworks. Common to both research strands is a method for dealing with the iterative nature of fixed points. The first part of the thesis looks at the computation of least fixed points in terms of closure ordinals of formulas in the modal 𝜇-­calculus. Using annotated structures, a new framework is defined to describe how the iterations of a fixed point formula evolve in a transition system. Applying a pumping technique allows us to establish an upper bound for countable closure ordinals. The method is tailored to the lower levels of the alternation hierarchy, but the fragment covered is broad enough to allow for considerations on the effects of fixed point alternation. In the second part, fixed points are considered in the context of a cyclic proof system for intuitionistic arithmetic. Cyclic proofs internalise induction in their structure, suggesting a natural fitting with quantifiers defined in terms of fixed points. Using higher order recursion schemes generated from instances of cyclic proofs, we investigate the computational content implicit in the initial proof.

As originally showed by Barr, a topology on a set X can be equivalently described as a ‘convergence relation’ between elements of X and ultrafilters on X: in other words, a spatial locale can be recovered from its set of points once it is endowed with appropriate extra structure defined in terms of ultrafilters. In this talk, I will present a similar reconstruction result for (Grothendieck) toposes with enough points, a categorification of spatial locales: every such topos can be recovered up to equivalence from its category of points, provided that the latter is endowed with appropriate extra structure involving ultrafilters. In logical terms, this reads as a (strong) conceptual completeness theorem for geometric logic. Towards this goal, I will introduce ultraconvergence spaces, a profunctorial generalization of Makkai’s ultracategories inspired by Barr’s convergence relations. This talk is based on joint work with Quentin Aristote, Sam van Gool and Jérémie Marquès.

First-order modal logic (FOML) provides a natural logical language for reasoning about modal attitudes, while retaining the richness of quantification for referring to predicates over domains. However, FOML is notoriously bad computationally, as most of the useful fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic fragment) have been shown to be decidable under heavy restrictions on the syntax. In this talk, I survey our recent work on the newly discovered bundled fragments based on constructions bundling quantifiers and modalities together. The idea came from our earlier work on epistemic logics of know-how/why/what, and it led us to many expressive and decidable fragments of FOML without restricting the number of variables or the arity of the predicates. I will give an almost complete picture of the (un)decidability of all the basic bundled fragments of FOML over increasing and constant domain models. I conclude with some future directions.

The field of Belief Change studies how an agent updates its beliefs in the presence of new information. In this work, we consider the case where beliefs are represented as description logic concepts and the new information is in the format of pointed interpretations. We call this setting model change, and distinguish three main kinds of changes: eviction, which consists of only removing models; reception, which incorporates models; and revision, which combines removal with incorporation of models in a single operation. We introduce a formal notion of revision and argue that it does not reduce to a simple combination of eviction and reception, contrary to intuition. We provide positive and negative results on the compatibility of eviction and reception for EL and ALC description logic concepts and on the compatibility of revision for ALC concepts.

Craig interpolation is the property held of many logics that for any valid implication A -> B there exists a formula I using only vocabulary common to both A and B such that A -> I and I -> B are both valid. The property is named after William Craig who formulated and proved the result for classical first-order logic in 1957.

Proof-theoretic treatments of interpolation, by their nature, offer further insights into a logic, such as characterising the complexity of interpolants. I will showcase several remarkable consequences of interpolation in the context of modal logic with fixed points, ranging from characterisatisons of expressivity using fixed points to the solution of certain decidability problems.

The claim is that intensions (or meanings) can be modeled usefully by algorithms which compute truth values, proofs (in various systems), denotations and implementations of programs (in various programming languages), etc.. I will discuss the nature of these ‘algorithms’ and present some unpublished results by me and others on this topic. Most of what I will say is in the book [1] which contains many unpublished results by Lou van den Dries, Vaughn Pratt, Anush Tserunyan and others.

1. Yiannis Moschovakis. Abstract recursion and intrinsic complexity, Cambridge University Press, Volume 48 in the Lecture Notes in Logic, Association for Symbolic Logic, 2019. (See YM’s homepage).