2025/06/02 by Borja Sierra Miranda, Miranda, Borja Sierra, Thomas Studer +3 · 3 citations
Computer Science · #FOS: Mathematics #Logic (math.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2506.01711
openalex publication_date 2025/06/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30
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.