Graphical Proof Theory I: Sequent Systems on Undirected Graphs

TL;DR

This paper develops sequent calculi for logical reasoning on graphs, extending classical logic to graph structures, proving key properties like cut-elimination, and establishing equivalences with existing graphical logics.

Contribution

It introduces a novel set of logical connectives for graphs, extends sequent calculus to these, and proves their properties and equivalences with known graph-based logics.

Findings

Sequent calculi for graphs are sound and complete.

Cut-elimination is established for the proposed systems.

One system is shown equivalent to the graphical logic GS.

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.