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,The Review of Symbolic Logic,vol. 14 (2018), pp. 22–50.
- \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.
- 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.
- Borja Sierra Miranda, Thomas Studer and Lukas Zenger,_Coalgebraic transformations of non-wellfounded proofs_to appear in arXiv.