Logic@GU

A 2½-day workshop dedicated to current and future trends in cyclic and illfounded forms of provability and justification. The event is sponsored by the Knut and Alice Wallenberg Foundation via the research project Taming Jörmungandr: The Logical Foundations of Circularity, the Swedish Research Council through the research project Proofs with Cycles and Computation, and the Department of Philosophy, Linguistics and Theory of Science at the University of Gothenburg.

Speakers

• Henning Basold (Leiden University)
• Anupam Das (University of Birmingham)
• Sebastian Enqvist (Stockholm University)
• Zeinab Galal (RIMS, Kyoto)
• Iris van der Giessen (University of Amsterdam)
• Marianna Girlando (University of Amsterdam)
• Helle Hvid Hansen (University of Groningen)
• Stefan Hetzl (TU Wien)
• Alex Leitsch (TU Wien)
• Reuben Rowe (Royal Holloway)
• Alexis Saurin (IRIF)
• Takeshi Tsukada (Chiba University)

Location

The workshop will be held at the Faculty of Humanities of the University of Gothenburg, address Renströmsgatan 6, Gothenburg. It is adjacent to the Korsvägen transport hub and within walking distance from the city centre.

Registration

Attendence is free but registration is required. The deadline for registration has passed. In case of questions, contact Gianluca Curzi.

Schedule

The workshop starts at 9am on Wednesday, 24 September and closes at 12.30 on of Friday, 26 September 2025. All talks will be in room J439 in the Humanisten building of Gothenburg University.

Wednesday, 24 September

• 9.00 Registration
• 9.30 Alexis Saurin – Title TBA
• 10.30 Break
• 11.00 Alex Leitsch – Proof Schemata and Herbrand systems

  Abstract A proof schema is an expression (recursively) representing an infinite sequence of proofs. Proof schemata depend on parameters (variables over natural numbers) and evaluate to proofs when the parameters are replaced by numerals. These schemata provide a formalism to express induction without induction rules. The main application of proof schemata lies in the (automated) analysis of mathematical proofs using induction. While Herbrand’s theorem fails in presence of induction it can be realized in proof schemata. Instead of a single Herbrand sequent (we work in sequent calculus) we obtain an infinite sequence of Herbrand sequents. A Herbrand system is the corresponding (recursively defined) infinite sequence of Herbrand substitutions defining the Herbrand sequents. As, in general, the computation of a Herbrand sequent requires cut-elimination, a cut-elimination method for schemata is needed. Schematic CERES (Cut-elimination by RESolution) is such a method which will be presented in brief. By their potential in extracting relevant information from mathematical proofs, Herbrand systems provide a powerful tool in automated proof analysis.

• 12.00 Lunch
• 13.30 Marianna Girlando – Propositional Dynamic Logic to Transitive Closure Logic: Cyclic Proofs via Hypersequents

  Abstract Propositional Dynamic Logic (PDL) is a modal logic for reasoning about the iterative execution of programs. Via the standard translation, PDL can be embedded into Transitive Closure Logic (TCL), an extension of first-order logic with a recursive operator expressing the transitive closure of binary relations. Cyclic proof systems based on Gentzen-style sequents have been developed for both PDL and TCL in the literature, but cyclic proofs for PDL do not directly translate into cyclic proofs for TCL. Therefore, the standard translation does not lift to the level of Gentzen-style cyclic proofs. Motivated by this observation, we introduce a hypersequent-style cyclic proof system for TCL, which enriches Gentzen-style sequents with additional structural connectives. We prove that this system is sound and that it simulates cyclic proofs for PDL, thereby establishing cut-free completeness for a fragment of TCL.

  This talk is based on joint work with Anupam Das, published in the Journal of Automated Reasoning: https://link.springer.com/article/10.1007/s10817-023-09675-1. A preprint is available here: https://arxiv.org/abs/2205.08616

• 14.30 Iris van der Giessen – Uniform interpolation for intuitionistic Gödel-Löb logic

  Abstract In this talk I would like to present ongoing joint work with Guillermo Menéndez Turata and Borja Sierra Miranda. The research is concerned with proving the uniform interpolation for Gödel-Löb logics using cyclic proofs. From a cyclic sequent system a so-called pre-interpolant template is extracted which is a tree with cycles. Based on this template fixpoint equations are obtained and solved in the Gödel-Löb logic obtaining uniform interpolants. The method works to reprove the uniform interpolation property for Gödel-Löb logic GL. Most interestingly, it provides a first proof of the uniform interpolation property for intuitionistic Gödel-Löb logic iGL.

• 15.30 Break
• 16.00 Helle Hvid Hansen – Craig Interpolation for PDL via Cyclic Tableaux

  Abstract The question of whether Propositional Dynamic Logic (PDL) has Craig interpolation was disputed for several years, with three proof attempts being published but later criticized or retracted. In this talk, I will present a proof based on the ideas of Borzechowski (1988). The proof uses a cyclic tableau system for PDL and an adaptation of Maehara’s method. In this approach, interpolants for cycles are obtained as the solutions to fixpoint equations, and the challenge is to ensure that these fixpoint equations have solutions in PDL. To achieve this, the construction of interpolants for clusters (strongly connected components) employs an auxiliary structure called a quasi-tableau.

  This is joint work with Malvin Gattinger, Revantha Ramanayake, Valentina Trucco Dalmas and Yde Venema.

Thursday 25 September

• 9.00 Takeshi Tsukada – Title TBA
• 10.00 Break
• 10.30 Reuben Rowe – Algorithms for Checking Infinite Descent

  Abstract The (PSPACE-complete) Infinite Descent property underpins the trace-based validation of cyclic derivations that capture inductive and coinductive reasoning, as well as the size-change approach to proving program termination. In the literature, we find a couple of different algorithms described for deciding Infinite Descent: a dynamic programming algorithm incorporating a fixed-point saturation (e.g. as suggested in the size-change termination paper by Lee, Jones, and Ben-Amram), and an encoding via containment of omega automata (e.g. in Brotherston’s thesis).

  In this talk I will describe work in which we have developed an alternative automata-theoretic encoding (with some connections to a construction described by Dax, Hoffman and Lange) and an optimisation of the dynamic programming algorithm that takes into account some specific symmetries present in the Infinite Descent problem. I will also describe some more efficient, but approximate (i.e. incomplete) approaches for checking Infinite Descent that we have developed. I will comment on the relative tradeoffs in the (runtime) complexity of the decision procedures, and report on an experimental evaluation of our implementations of these algorithms within the Cyclist theorem prover framework. Interestingly, we found the approximate methods to provide good coverage in practice.

• 11.30 Stefan Hetzl – Title TBA
• 12.30 Lunch
• 14.00 Anupam Das – Title TBA
• 15.00 Break 
• 15.30 Sebastian Enqvist – Computation by infinite descent made explicit

  Abstract I will present a non-wellfounded proof system for intuitionistic logic extended with ordinary inductive and co-inductive definitions, based on a syntax in which fixpoint formulas are annotated with explicit variables for ordinals. My main motivation for studying this system was to get a better understanding of the recently introduced validity criterion for non-wellfounded proofs in terms of so called “bouncing threads”. I will describe the computational content of this system via a notion of computability and show that every valid proof is computable. A consequence of this result is that every proof of a sequent of the appropriate form represents a unique function on natural numbers. Finally, we derive a categorical model from the proof system and show that least and greatest fixpoint formulas correspond to initial algebras and final coalgebras respectively.

Friday 26 September

• 9.30 Zeinab Galal – A categorical viewpoint on systems of fixpoint equations

  Abstract Fixpoints play an important role in both denotational semantics where they are used to represent recursively defined programs and data types as well as in operational semantics where many behavioral equivalences are obtained as fixpoints of some relation transformers.

  In the categorical theory of fixpoint operators, we usually consider one fixpoint operator at a time and little attention is given to the study of mixed fixpoint operators where we take a different fixpoint operator for each variable. Systems combining least and greatest fixpoints over lattices are an important example as they are the basis of many static analysis and model checking methods.

  I will present in this talk an axiomatization of mixed fixpoint operators first in the 1-categorical setting and then briefly mention how to extend to 2-categories in order to capture the examples of (parametrized) initial algebras and coalgebras of accessible functors, analytic and polynomial

• 10.30 Break
• 11.00 Hening Basold – Invariants in Cyclic Proofs

  Abstract In this talk, I will present general category theoretical approaches to recursive computations and proofs, which are ensured to be well-defined by local invariants. That is, it is not necessary to check programs and proofs as a whole to guarantee that they have productive operational semantics, rather the conditions are checked at each step of their composition. A well-known instance is guarded recursion in the so-called topos of trees and the resulting type systems with the so-called later modality. We will discuss how the approach of guarded recursion can be extended to other categories than that of sets and maps, which is where the topos of trees originates, and even to situations that are not Cartesian. This allows us to construct recursive proof systems for non-classical, modal and quantitative logic. However, from the coalgebraic perspective, we can only construct causal computations and proofs in the topos of trees, which means that each approximation step of a recursion only depends on previous steps. We will see in the talk how to move beyond this and devise a category theoretical approach to guarded recursion that captures uniform continuity. This enables a much broader class of recursive computations and proofs that are guaranteed to be well-defined by local invariants.

• 12.00 Closing

Organisers

• Graham E Leigh
• Gianluca Curzi
• Bahareh Afshari
• Ivan Di Liberti
• Dominik Wehr
• Giacomo Barlucchi

In case of questions, contact Graham Leigh

There is a long tradition of distinguishing finistic methods of reasoning, for both philosophical and mathematical motivations. Typically, this is made precise by reducing arguments to some theory of arithmetic – usually Peano or Heyting Arithmetic, or weaker fragments thereof. However, working directly in such systems requires encoding all objects as numbers; it is easy to get the impression that such coding is an inherent and inevitable aspect of the topic.

On the contrary, most major foundational logics – in particular, ZF-style set theory and dependent type theories – admit finitistic variants, equivalent in strength to suitable systems of arithmetic. These allow us to work rigorously in a finististic foundation, while keeping the richly expressive language we’re used to from everyday mathematics.

I will survey various finitistic systems, and then focus in more detail on the categorical Arithmetic Universes of Joyal, and type theories for these, following Maietti.

Opponent: TBA

Abstract Description logics are designed to reason efficiently with ontologies in knowledge bases, which are widely used in several industries. Human errors commonly cause mistakes to occur in the axioms of these ontologies, which leads to the logics deducing false conclusions. Ontology engineers spend much time on finding these false axioms to repair the ontology. This process can be facilitated by presenting a justification of the false conclusion, i.e. a set of axioms that entail the conclusion. Typically, the number of justifications for a given conclusion is very large and it is not clear which one should be presented.

It is therefore useful to estimate the cognitively adequate complexity of description logic so that the simplest justification(s) can be identified and selected. This work focusses on the cognitive complexity of deciding the consistency of ABoxes in the description logic $\mathcal{ALE}$. Conceptual considerations entail that the complexity of the ABox consistency problem is expressed as a linear preorder on a large enough set of ABoxes. This linear preorder can be estimated by an ACT-R model called SHARP. The model is a tableau algorithm implemented in a cognitive architecture, thereby modelling a human brain executing the tableau algorithm, which forms an approximation of the cognitive complexity ordering.

A complexity ordering that is a linear preorder can be obtained from experimental data by aggregating the different individual orders from a sample into one so-called proto-order, in which the largest transitive subrelation is the desired linear pre-order. The predicted complexity ordering by SHARP agrees well with the empirical data.

To enable applications in ontology debugging, a surrogate model is needed that accurately approximates SHARP’s output with great computational efficiency. Such a surrogate model can be obtained by the Random Forest algorithm trained on an appropriate dataset generated by SHARP. The complexity ordering thus obtained agrees well with the one predicted by SHARP but can be estimated in a fraction of the time enabling it for practical applications.

Examination committee:

• TBC

Dependence and independence concepts are ubiquitous in natural science, social science, humanities as well as in everyday life. The sentences “I park on this side of the road depending only on the day of the week” and “the time of descent is independent of the weight of the object” are examples of this. The question arises, do these concepts possess enough exactness for us to investigate their logic? There is currently a whole literature on this topic. It is the purpose of this talk to give a non-technical overview of this area of logic.

The combination of Löwenheim-Skolem Theorem and Compactness Theorem limits the expressive power of a logic to that of first order logic. This maximality principle is the famous Lindström Theorem for first order logic. It reveals that first order logic is at an optimal point of balance: by adding expressive power to it one necessarily loses model-theoretic properties. Soon after Lindström’s result, the question was raised, whether there are other logics at a similar point of equilibrium. More precisely: are there strict strengthenings of first order logic satisfying a Lindström-type characterization? Despite the naturality of this question, it remained unanswered, until recently.

In 2012 Saharon Shelah offered a solution to this problem in the form of a new infinitary logic. It has a Lindström-type characterization in terms of model-theoretic properties combining weak forms of Compactness and a Löwenheim-Skolem type property. In all known cases, a proof of a Lindström-type characterization automatically gives a proof of Craig Interpolation. This is the case for Shelah’s logic, too. There is, however, one aspect where Shelah’s logic seems to be rather weak: the syntax. The logic is derived from a game, in the sense that a sentence is, by definition, a class of structures, closed under a certain Ehrenfeucht-Fraïssé type of a game. This results in the absence of a syntax defined in such a way that the set of all formulas could be obtained by closing the set of atomic formulas under negation, conjunction, quantifiers, and possibly other logical operations. The lack of syntax complicates further study of it and logics in its neighborhood. In the present talk, we address the general question of deriving a syntax from a game, and the more localized question of finding a syntax for Shelah’s logic. Partial answers are provided to both questions. This is joint work with Andres Villaveces and Siiri Kivimäki.