The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings)

TL;DR

This paper proves that in Multiplicative Exponential Linear Logic without weakenings, the semantic interpretation in a multiset relational model uniquely identifies proofs up to certain structural connections, establishing injectivity.

Contribution

It demonstrates that the multiset relational model provides an injective semantics for proofs in this fragment of linear logic, aligning syntactic and semantic equivalences.

Findings

Semantic and syntactic proof equivalences coincide

Interpretation in the model is injective for this logic fragment

Proofs are uniquely identified by their semantic interpretation

Abstract

We show that for Multiplicative Exponential Linear Logic (without weakenings) the syntactical equivalence relation on proofs induced by cut-elimination coincides with the semantic equivalence relation on proofs induced by the multiset based relational model: one says that the interpretation in the model (or the semantics) is injective. We actually prove a stronger result: two cut-free proofs of the full multiplicative and exponential fragment of linear logic whose interpretations coincide in the multiset based relational model are the same "up to the connections between the doors of exponential boxes".