# Coalgebra for non-wellfounded proof theory

## Borja Sierra Miranda

**Authors:** Borja Sierra Miranda, Thomas Studer and Lukas Zenger

Non-wellfounded 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 well-founded frame conditions like \(\textsf{GL}\) (Gödel-Lö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 cut-elimination for non-wellfounded 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

- Yury Savateev and Daniyar Shamkanov,
*Non-Well-Founded Proofs Proofs for the Grzegorczyk Modal Logic*,,vol. 14 (2018), pp. 22–50.*The Review of Symbolic Logic* - \bysame,
*Cut Elimination for the Weak Modal Grzegorczyk Logic via Non-well-Founded Proofs*,(Rosalie Iemhoff, Michael Moortgat and Ruy de Queiroz, editors),vol. 11541,Springer, Berlin, Heidelberg,2019,pp. 569–-583.*Logic, Language, Information, and Computation. WoLLIC 2019. Lecture Notes in Computer Science* - Borja Sierra Miranda,
*Cyclic Proofs for iGL via Corecursion*,to appear inOpen Publishing Association,2024.*Electronic Proceedings in Theoretical Computer Science, Workshop on Fixed Points in Computer Science* - Borja Sierra Miranda, Thomas Studer and Lukas Zenger,_Coalgebraic transformations of non-wellfounded proofs_to appear in arXiv.