Graphical Proof Theory I: Multiplicative Linear Logic Beyond Cographs
share
Cographs are a class of (undirected) graphs, characterized by the absence of induced subgraphs isomorphic to the four-vertices path, showing an intuitive one-to-one correspondence with classical propositional formulas. In this paper we study sequent calculi operating on graphs, as a generalization of sequent calculi operating on formulas, therefore on cographs. We mostly focus on sequent systems with multiplicative rules (in the sense of linear logic, that is, linear and context-free rules) extending multiplicative linear logic with connectives allowing us to represent modular decomposition of graphs by formulas, therefore obtaining a representation of a graph with linear size with respect to the number of its vertices. We show that these proof systems satisfy basic proof theoretical properties such as initial coherence, cut-elimination and analyticity of proof search. We prove that the system conservatively extend multiplicative linear logic with and without mix, and that the system extending the former derives the same graphs which are derivable in the deep inference system GS from the literature. We provide a syntax for proof nets for our systems by extending the syntax of Retoré's RB-structures to represent graphical connectives. A topological characterization of those structures encoding correct proofs is given, as well as a sequentialization procedure to construct a derivation from a correct structure. We conclude the paper by discussing how to extend those linear systems with the structural rules of weakening and contraction, providing a sequent system for an extension of classical propositional logic beyond cographs.
READ FULL TEXT