Speaker
Borja Sierra Miranda
University of Bern
Talks at this conference:
Friday, 15:40, J336 
Coalgebra for nonwellfounded proof theory 
Authors: Borja Sierra Miranda, Thomas Studer and Lukas Zenger Nonwellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely wellfounded frame conditions like \(\textsf{GL}\) (GödelLöb logic also known as provability logic) or \(\textsf{Grz}\) (Grzegorczyk logic). We provide a uniform method to define proof translations for such systems, guaranteeing that the condition on infinite paths is preserved. In addition, as particular instances of our method, we establish cutelimination for nonwellfounded systems of the logics \(\textsf{Grz}\) and \(\textsf{wGrz}\) (weak Grzegorczyk logic). Our proof relies only on the categorical definition of corecursion via coalgebras, while an earlier proof by Savateev and Shamkanov uses ultrametric spaces and a corresponding fixed point theorem. Bibliography
