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.

翻译：非良基证明系统通过在推导树上施加称为全局迹条件（GTC）的全局性质来确保可靠性。由于这些条件的全局非组合性以及非良基证明的无穷结构特性，为保障可靠性的GTC提供范畴论刻画仍然具有挑战性。我们为非良基证明系统建立了一个余代数框架，其中推导树被建模为预层上广义多项式函子的余代数。鉴于GTC是对推导图中无穷路径的约束，我们利用余代数图，将GTC以余代数形式表述为对这些图的条件。可靠性进而被表述为：存在从表示推导图的余代数到指定语义的代数之间的唯一余代数到代数态射。在此框架内，我们通过递归余代数刻画GTC：一个余代数满足GTC当且仅当其通过适当伴随函子的像具有递归性。在给定语义代数的适当假设下，这保证了可靠性，即每个证明都允许唯一的余代数到代数态射。我们通过模态μ演算的非良基证明系统、高阶不动点逻辑的非良基证明系统，以及μ双完备范畴中Santocanale循环证明系统的非良基变体来演示该框架。