Coalgebraic proof translations for non-wellfounded proofs
Abstract
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 GL or Grz. In this paper, 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 instance of our method, we establish cut-elimination for a non-wellfounded system of the logic Grz. 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.
Cite
@article{arxiv.2506.01711,
title = {Coalgebraic proof translations for non-wellfounded proofs},
author = {Borja Sierra Miranda and Thomas Studer and Lukas Zenger},
journal= {arXiv preprint arXiv:2506.01711},
year = {2025}
}