Interaction Graphs: Multiplicatives

TL;DR

This paper introduces a graph-theoretical framework for multiplicative linear logic proofs that provides a denotational semantics and a notion of truth, connecting to Girard's geometry of interaction through a combinatorial approach.

Contribution

It presents a novel graph-based representation of proofs in multiplicative linear logic that unifies semantics and truth notions, and relates to Girard's geometry of interaction.

Findings

Develops a graph-theoretical proof representation for MLL.

Derives a categorical semantics and a notion of truth from the framework.

Shows equivalence with Girard's geometry of interaction in a restricted setting.

Abstract

We introduce a graph-theoretical representation of proofs of multiplicative linear logic which yields both a denotational semantics and a notion of truth. For this, we use a locative approach (in the sense of ludics) related to game semantics and the Danos-Regnier interpretation of GoI operators as paths in proof nets. We show how we can retrieve from this locative framework both a categorical semantics for MLL with distinct units and a notion of truth. Moreover, we show how a restricted version of our model can be reformulated in the exact same terms as Girard's latest geometry of interaction. This shows that this restriction of our framework gives a combinatorial approach to J.-Y. Girard's geometry of interaction in the hyperfinite factor, while using only graph-theoretical notions.