Archive of events from 2026

Codd’s Theorem, a fundamental result of database theory, asserts that relational algebra and relational calculus have the same expressive power on relational databases. We explore Codd’s Theorem for databases over semirings and establish two different versions of this result for such databases: the first version involves the five basic operations of relational algebra, while in the second version the division operation is added to the five basic operations of relational algebra. In both versions, the difference operation of relations is given semantics using semirings with monus, while on the side of relational calculus a limited form of negation is used. The reason for considering these two different versions of Codd’s theorem is that, unlike the case of ordinary relational databases, the division operation need not be expressible in terms of the five basic operations of relational algebra for databases over an arbitrary positive semiring; in fact, we show that this inexpressibility result holds even for bag databases.

The Logic Group at the University of Gothenburg hosts its annual World Logic Day Pub Quiz. For more information on this other World Logic Day events around the world, see http://wld.cipsh.international/wld2026.html.

Throughout proof theory, proofs are often taken to be well-founded (often finite) trees of inferences. Theories of inductive definitions, among other theories, bump up against the limitations of this perspective, and a variety of formalisms have been used to push beyond this – Girard’s beta-proofs, non-well-founded proofs, proofs-as-functions. We briefly describe some features of these approaches, the way these perspectives are essentially equivalent, and the way well-foundedness reasserts itself as a core property of proofs.

In 1981 Kaufmann proved the set-theoretic analogue of a result due to Paris and Kirby in the context of arithmetic that connects fragments of the collection scheme to the existence of proper partially elementary end extensions. In particular, he shows that a countable resolvable model of a weak set theory has a proper \(\Sigma_{n+1}\)-elementary end extension if and only if it satisfies collection for all \(\Pi_n\)-formulae. In the same paper Kaufmann asks if every \(L_\alpha\) (the \(\alpha\)-th level of Goedel’s constructible hierarchy) that has a proper \(\Sigma_2\)-elementary end extension necessarily has one that satisfies bounded collection. Clote (1983) asks a generalised version of Kaufmann’s question for models of fragments of PA: Does every countable model of \(B\Sigma_{n+2}\) have a proper \(\Sigma_{n+2}\) elementary end extension that satisfies \(B\Sigma_{n+1}\)? Sun Mengzhou has recently (2025) shown that Clote’s question has a positive answer. In this talk I will describe recent work showing that, in contrast, the set-theoretic analogue of Clote’s question (the generalisation of Kaufmann’s original question) has a negative answer

Team semantics is a semantic framework originally introduced by Hodges (1997) for the study of dependence and independence concepts, and later systematically developed by Väänänen (2007). It is also independently adopted in inquisitive logic by Ciardelli and Roelofsen (2011). In team semantics, formulas are evaluated with respect to sets of evaluation points, called teams, rather than single evaluation points as in standard semantics.

Logics based on team semantics are typically extensions of classical logic and thus inherit classical implication over classical formulas. However, the earliest versions of team-based logic, such as independence-friendly logic and dependence logic, do not include a conditional connective for arbitrary formulas. An adequate conditional, known as intuitionistic implication, was proposed for dependence logic by Abramsky and Väänänen (2009). This connective is also part of the syntax of inquisitive logic. Intuitionistic implication behaves well in these downward closed logics, in the sene that it preserves downward closure and satisfies both Modus Ponens and the Deduction Theorem.

In recent years, many variants of dependence logic with different closure properties have been introduced, including union closed and convex logics. In these settings, the intuitionistic implication no longer behaves well, as it either fails to preserve the relevant closure property or fails to satisfy the Deduction Theorem. In this talk, we show that this failure is unavoidable: these logics cannot be enriched with any conditional connective that simultaneously preserves the closure property and satisfies both Modus Ponens and the Deduction Theorem.

This is joint work with Fausto Barbero.

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).

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 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.

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.

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.

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.

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.

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.