Spring Semester FS2026

Unless stated otherwise, all talks will take place in room ExWi 228 of the Exakte Wissenschaft Building (ExWi) at the University of Bern.

Schedule

Abstracts

Esakia duality provides a categorical dual equivalence between Heyting algebras, the algebraic semantics of intuitionistic logic, and certain descriptive intuitionistic Kripke frames. Dualities for modal extensions of intuitionistic logic are often derived by extending Esakia duality with additional structure, such as an additional relation. However, this strategy does not work for the constructive modal logic CK. The intuitive reason is that the birelational semantics for CK makes crucial use of the fact that the intuitionistic accessibility relation is a preorder, while Esakia duality requires a partial order. In this talk I will discuss this phenomenon and show how we can still obtain a duality for CK.

Intuitionistic tense logic, introducecd by Ewald(1986), provides a framework by extending intuitionistic logic with two pairs of adjoint temporal modalities. While Figallo and Pelaitay have previously established its algebraic semantics and discrete duality, its proof- theoretic properties require further investigation. In this talk, we present a formal proof of cut elimination for IKt using a specialized sequent calculus. The technical core of the proof focuses on a strategy for splitting the contraction and cut rules. This result confirms the consistency of the system and provides a basis for further study of its decidability.

In this talk, we investigate the pointed modal logic of reals. We first establish its relational (Kripke) semantics with bounded valuations in the Abelian l-group of real numbers with the distinguished negative constant -1. To study this logic algebraically, we introduce the variety of pointed modal Abelian l-groups, in particular we focus on the strongly pointed members thereof. Constructing complex algebras and canonical frames, we establish a Truth Lemma connecting the relational and algebraic frameworks.

Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. We adapt the technique to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM. To do this, we design a novel multi-succedent sequent calculus for this logic which terminates, eliminates cut, and provides a decidability argument for KM. Then, we adapt Pitts' technique to our calculus to construct uniform interpolants for KM, while highlighting the hurdles we overcame. Finally, by (re)proving the algebraisability of KM, we deduce the coherence of the class of KM-algebras. All our results are fully mechanised in the Rocq proof assistant, ensuring correctness and enabling effective computation of interpolants.

Common knowledge plays a central role in modeling coordination in multi-agent systems, yet classical results show that even arbitrarily small temporal uncertainty prevents it from ever being attained in practical systems. This has motivated a range of approximations to common knowledge, including ε-common knowledge and eventual common knowledge, which relax the requirement that all levels of mutual knowledge hold simultaneously. These notions aim to retain the logical structure of common knowledge while making it compatible with temporal imprecision. In this talk, we will focus on the logic of eventual common knowledge.