A cyclic proof system for Guarded Kleene Algebra with Tests
Guarded Kleene Algebra with Tests (GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about imperative while programs. Following earlier work by Das and Pous on Kleene Algebra, we study GKAT from a proof-theoretical perspective. The deterministic nature of GKAT makes ordinary sequents sufficient for achieving regular completeness, unlike with Kleene Algebra, where hypersequents are required. Moreover, proof search is in Co-NP, as opposed to the PSPACE complexity of proof search for Kleene Algebra.

This talk is based on joined work with Dexter Kozen and Alexandra Silva.

The reset rule with ordinal variables and cuts
Dam, Gurov & Sprenger have developed proof systems for modal and first-order mu-calculi using explicit variables for ordinal approximants of fixpoints. The annotated systems of Jungteerapanich and Stirling are similar, but use a different correctness criterion involving the so called "reset rule". Moreover, the latter systems are cut-free by design. I will show by an example that, in fact, combining the cut rule with a Jungteerapanich-Stirling-style reset rule results in an unsound system. Luckily, there is a simple fix which becomes apparent when considering the straightforward semantics of explicit ordinal variables. The result is a system which combines the virtues of both types of proof system: the presence of the cut rule allows us to capture the full strength of the Dam-Sprenger system for first-order mu-calculus, while the reset rule is advantageous in that it simplifies proof checking and helps with proof search. A recent application is a sound and complete, finitary (cyclic) proof system for the two-way mu-calculus.

The talk will be based on joint work with Bahareh Afshari, Graham Leigh, Johannes Marti and Yde Venema.

A cyclic proof system for intuitionistic linear-time temporal logic
Intuitionistic linear-time temporal logic, iLTL, combines Pnueli’s linear-time temporal logic (LTL) and propositional intuitionistic logic. Models of iLTL are two-dimensional: every state has at least one temporal successor and zero or more intuitionistic ‘successors’. Monotonicity of the temporal successor function with respect to the intuitionistic order suffices to ensure that truth is preserved upwards intuitionistically. We provide a cut-free, finitary cyclic proof system for iLTL. The calculus uses labelled formulas in order to accommodate the interplay between the temporal and the intuitionistic dimensions.

Cut-elimination: old results and new questions
We review some results about cut-elimination in infinitary systems, i.e. systems with infinitely branching rules, for modal fixed point logics. Then, we discuss recent approaches to cut-elimination in ill-founded and cyclic systems.

The topological mu-calculus: completeness and the finite model property
In this talk I will discuss a new method of proving completeness for a large class of transitive modal fixed-point logics. I will also review topological completeness of these logics with respect to the derived set semantics.

This is joint work with Alexandru Baltag and David Fernandez Duque

Fixpoints in Modal Logic: Finite Convergence and Higher Order
Fixpoint iteration is the main tool for evaluating recursively defined properties in temporal specification languages like the modal mu-calculus Lmu. Finite convergence, i.e. the phenomenon of reaching a fixpoint after finitely many iterations only, is of particular interest for algorithmic properties of such logics. The iteration of fixpoints of Lmu formulas trivially converges finitely on finite structures, but also clearly on (infinite) structures whose bisimulation quotient is finite. We start by reviewing the converse and present a (word) structure W on which all mu-calculus fixpoints converge finitely, even though that structure does not have a finite bisimulation quotient. We then introduce Higher-Order Fixpoint Logic HFL, an extension of Lmu in which formulas denote (higher-order) functions on sets of states of a transition system, with a type order such that Lmu is exactly HFL0, the set of HFL formulas only using functions of order 0. HFL is interesting in this context because it is very easy to construct an HFL1 formula, i.e. using first-order functions, that does not converge finitely over W. Moreover, it introduces a hierarchy of classes of transition systems with finite convergence of (higher-order) fixpoints. It is not unreasonable to suspect this hierarchy to collapse at a low type level, but this is currently an open question. We will present some ideas on how to tackle this.

This is joint work with Florian Bruse and Marco Sälzer of the University of Kassel and Etienne Lozes of the Université Cote d'Azur.

An Abstract Look at the Fixed-Point Theorem for Provability Logic
I discuss some general perspectives on the well-known Fixed-Point Theorem for Provability Logic, taking my cues from an old abstract argument by Dick de Jongh. This will lead us into issues about recursion in several old and new modal logics.

Intuitionistic Gödel-Löb logic, à la Simpson
We derive an intuitionistic version of Gödel-Löb modal logic (GL) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, lIGL, by restricting a non-wellfounded labelled system for GL to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that GL's usual frame condition, termination, is not first-order definable. While existing intuitionistic versions of GL are typically defined over only the box (and not the diamond), our presentation includes both modalities.

Our main result is that lIGL coincides with a corresponding semantic condition in birelational semantics: the composition of the modal relation and the intuitionistic relation is conversely well-founded. We call the resulting logic IGL. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of IGL.

This talk is based on joint work with Iris van der Giessen and Sonia Marin: https://arxiv.org/abs/2309.00532.