Coalgebraic proof translations for non-wellfounded proofs

TL;DR

This paper introduces a categorical method for translating non-wellfounded proofs, ensuring infinite path constraints are preserved, and proves cut-elimination for the Grz logic system using coalgebraic corecursion.

Contribution

It provides a uniform coalgebraic approach to proof translations in non-wellfounded proof systems, including a new proof of cut-elimination for Grz.

Findings

Proof translation preserves infinite path constraints.

Cut-elimination for Grz logic established via coalgebraic methods.

Method relies on categorical corecursion, simplifying previous approaches.

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.