Coalgebraic Non-Wellfounded Proofs: Recursiveness and GTC

TL;DR

This paper introduces a coalgebraic framework for non-wellfounded proof systems, characterizing the global trace condition (GTC) through recursive coalgebras to ensure soundness in infinite derivation structures.

Contribution

It provides a categorical, coalgebraic characterization of the GTC, linking it to recursive coalgebras and establishing soundness for non-wellfounded proof systems.

Findings

Coalgebraic model captures derivation trees as coalgebras of polynomial functors.

GTC characterized as a condition on coalgebraic graphs of derivations.

Framework applied to modal mu-calculus, higher-order fixed-point logics, and mu-bicomplete categories.

Abstract

Non-wellfounded proof systems impose a global condition called the global trace condition (GTC) on a derivation tree to ensure soundness. Providing a categorical characterisation of the GTC that guarantees soundness remains challenging due to the global, non-compositional nature of these conditions and the infinitary structure of non-wellfounded proofs. We develop a coalgebraic framework for non-wellfounded proof systems where derivation trees are modelled as coalgebras of generalised polynomial functors on presheaves. Since the GTC is a constraint on infinite paths in derivation graphs, we employ graphs of coalgebras and formulate the GTC coalgebraically as a condition on these graphs. Soundness is then formulated as the existence of a unique coalgebra-to-algebra morphism from a coalgebra representing a derivation graph to an algebra specifying semantics. Within this framework, we characterise the GTC via recursive coalgebras: a coalgebra satisfies the GTC if and only if its image under a suitable adjoint is recursive. Under an appropriate assumption on the given semantic algebra, this yields soundness, that is, every proof admits a unique coalgebra-to-algebra morphism. We demonstrate our framework through a non-wellfounded proof system for the modal mu-calculus, one for higher-order fixed-point logics, and a non-wellfounded variant of Santocanale's circular proof system in mu-bicomplete categories.