On the role of connectivity in Linear Logic proofs

TL;DR

This paper explores a geometric property of linear logic proof-structures that extends correctness criteria, enabling better characterization and sequentialization in specific fragments of linear logic.

Contribution

It introduces a geometric condition that makes a necessary property sufficient for correctness in certain linear logic fragments, aiding proof characterization.

Findings

The property is necessary but not sufficient in general multiplicative exponential linear logic.

A geometric condition makes the property sufficient in specific fragments.

In intuitionistic linear logic, the property characterizes rule permutation equivalence.

Abstract

We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic to recover a sequent calculus proof from a proof-structure. We present a geometric condition on untyped proof-structures allowing us to turn this necessary property into a sufficient one: we can thus isolate fragments of linear logic for which this property is indeed a correctness criterion. In a suitable fragment of multiplicative linear logic with units, the criterion yields a characterization of the equivalence induced by permutations of rules in sequent calculus. In intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and it is sufficient for sequentialization in the axiom-free setting.