Workshop on Fixed Points and Illfounded Proofs, 2728 April, 2023
Held on 2728 April, 2023 at the University of Gothenburg, this workshop brought together researchers working on various aspects of fixed point logics and illfounded proofs. The event was sponsored by the Knut and Alice Wallenberg Foundation via the research project Taming Jörmungandr: The Logical Foundations of Circularity and the Department of Philosophy, Linguistics and Theory of Science.
Location
The workshop will take place at the Humanities faculty building of the University of Gothenburg. It is located next to the Korsvägen transport hub and within walking distance from the city centre.
Schedule
See below for talk abstracts.
Thursday, April 27th
Time  Occasion  Location 

9:30  Welcome fika  J411 
10:00  Anupam Das Using metamathematics to calibrate illfounded reasoning 

11:00  Lide Grotenhuis Illfounded proofs for intuitionistic lineartime temporal logic 

11:40  Dominik Wehr Ordinal annotations for cyclic firstorder arithmetics 

12:20  Lunch  Cafeteria 
14:00  Guillermo Menéndez Turata  J444 
14:40  Giacomo Barlucchi On closure ordinals 

15:15  Fika 
Friday, April 28th
Time  Occasion  Location 

10:00  Sebastian Enqvist Herbrand meets cyclic proofs 
J442 
10:40  Johannes Kloibhofer Cut elimination in cyclic proofs for temporal logic 

11:20  Gianluca Curzi On the computational expressivity of (circular) proofs with fixed points 

12:20  Lunch  Cafeteria 
14:00  Licentiate defense of Dominik Wehr (opponent: Anupam Das) Representation matters in cyclic proof theory 
J439 
16:00  Reception with coffee and cake  FLoV 
19:00  Workshop dinner 
Workshop dinner
On Friday evening, there will be a workshop dinner at Floating Saigon resturant on Kungsportsplatsen at the city end of Avenyn. Dinner starts at 19.00.
Abstracts
Anupam Das: Using metamathematics to calibrate illfounded reasoning
I will discuss some recent results exploiting metamathematical methods to measure the expressivity of circular reasoning in a variety of settings. I will focus on the general structure of such arguments, and in particular emphasise the scope of the methodology.
Lide Grotenhuis: Illfounded proofs for intuitionistic lineartime temporal logic
Illfounded and cyclic proof calculi have shown to be particularly suitable for modal fixed point logics. The present work is motivated by the question whether such calculi can also be designed for intuitionistic versions of such logics. The main obstacle in applying the standard techniques is the twodimensional nature of the intuitionistic semantics: Kripke models for intuitionistic modal logic consist of both an intuitionistic and a modal relation, which are required to satisfy some confluence properties.
In this work we study intuitionistic versions of lineartime temporal logic by considering the language iLTL, which extends intuitionistic propositional logic with the temporal operators ‘next’ and ‘until’. We interpret this language in models satisfying forward confluence and models satisfying both forward and backward confluence. For each of the resulting logics, we present a cutfree complete, illfounded sequent calculus. Both calculi employ a simple form of nesting that enables formulas to be operated on at different temporal positions. This is joint work with Bahareh Afshari, Graham Leigh and Lukas Zenger.
Sebastian Enqvist: Herbrand meets cyclic proofs
Herbrand’s theorem provides a sort of computational content to classical logic. A standard way to prove it uses cut elimination in sequent calculus. In recent work by Afshari, Hetzl and Leigh, it was shown how to extract Herbrand disjunctions directly from sequent calculus proofs without eliminating cuts first. The idea is to associate a higherorder recursion scheme with a given proof, from which a set of witnessing terms can be extracted. In this talk I will present ongoing work, joint with Bahareh Afshari and Graham Leigh, in which we show how such “Herbrand schemes” can be adapted to provide a method for witness extraction from cyclic sequent calculus proofs in the setting of the classical theory of inductively defined predicates. Indeed, this is a quite natural step to take, as recursion schemes in general are cyclic structures.
Johannes Kloibhofer: Cut elimination in cyclic proofs for temporal logic
We present cut elimination for an annotated cyclic proof system for modal logic with the eventually operator. In this proof system the usual method of pushing cuts upwards does not necessarily yield a proof. We circumvent this problem by separating the critical case in the cut reductions, enabling us to directly obtain a cutfree cyclic proof without a detour via infinitary proofs. We expect that this method can be extended to more complicated logics and thereby serve as a starting point for developing cut elimination methods for cyclic proof systems.
(joint work in progress with Bahareh Afshari)
Gianluca Curzi: On the computational expressivity of (circular) proofs with fixed points
We study the computational expressivity of proof systems with fixed point operators, within the ‘proofsasprograms’ paradigm. We start with a calculus muLJ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, muLJ admits an extension to a ‘circular’ calculus CmuLJ in a standard way.
Our main result is that, perhaps surprisingly, both muLJ and CmuLJ represent the same firstorder functions: those provably total in Pi12CA0, a subsystem of secondorder arithmetic beyond the ‘big five’ of reverse mathematics and one of the strongest theories for which we have an ordinal analysis (due to Rathjen). This solves various questions in the literature on the computational strength of (circular) proof systems with fixed points.
For the lower bound we give a realisability interpretation from an extension of Peano Arithmetic by fixed points that has been shown to be arithmetically equivalent to Pi12CA0 (due to Möllerfeld). For the upper bound we give a novel totality argument for circular proofs with fixed points. In fact we must formalise this argument itself within Pi12CA0 in order to obtain the tight bounds we are after, requiring a choice of higher computability model distinct from usual type structures for secondorder systems (such as GirardReynolds’ F). Along the way we develop some novel reverse mathematics for the KnasterTarski fixed point theorem.