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

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