Proofs as Coalgebras
Madeleine Gignoux

Abstract:
In this thesis we study ill-founded proof systems from a coalgebraic perspective. We present proofs as coalgebras, where correctness is enforced solely by path conditions on infinite branches, with no requirements of tree-like structure or rootedness. We apply this framework to the Gödel-Löb provability logic (GL) and the alternation-free μ-calculus (AFMC), and pursue three lines of investigation: finitization, interpolation, and formalization. For finitization, we establish exponential upper bounds on proof size in terms of closure size for both GL and AFMC. For interpolation, we obtain Lyndon interpolation for GL and syntactic Lyndon interpolation for AFMC; for the latter we additionally show that interpolant size is bounded exponentially by closure size. For formalization, we present a fully machine-verified proof of Craig interpolation for GL in Lean 4.