Graphical Proof Theory I: Sequent Systems on Undirected Graphs
Matteo Acclavio
TL;DR
The paper develops a graph-centered proof theory by introducing graphical connectives that encode graphs as first-class syntactic objects and by building sequent calculi ($\mathsf{MGL}$, $\mathsf{MGL}^{\circ}$, $\mathsf{GLK}$) that operate directly on these graph-encoded formulas. It leverages modular decomposition to extend the classical formula–graph correspondence from cographs to arbitrary graphs, showing that graph-encodings of a given graph are logically equivalent and that these calculi are conservative extensions of $\mathsf{MLL}$, $\mathsf{MLL}$ with mix, and $\mathsf{CPL}$. The authors prove cut-elimination for the proposed calculi and establish a soundness/completeness link between a specific calculus and the graphical deep-inference system $\mathsf{GS}$, thereby providing an analytic sequent framework for graph-based logics and paving the way for graph-centric proof theory with potential connections to pomset-like structures and broader applications. Overall, the work offers a principled method to reason about graphs via sequent calculi, ensuring normalization and structurally faithful representations of graphs.
Abstract
In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce a set of logical connectives allowing us to extend the correspondence between cographs and classical propositional formulas to any graph. We then provide sequent calculi operating on these formulas, we prove cut-elimination and that formula encoding the same graph are logically equivalent. We show that these systems provide conservative extensions of multiplicative linear logic (with and without mix) and classical propositional logic. We conclude by showing that one of these systems is equivalent to the graphical logic GS defined via a system of context-free graph rewiring rules, therefore providing an alternative proof of analyticity for this logic over graphs.