A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments

TL;DR

This paper establishes a novel connection between the classification of maximal abelian sub-algebras (MASAs) and fragments of linear logic, using a modified hyperfinite geometry of interaction model.

Contribution

It introduces a new interpretation of linear logic fragments via MASAs within a von Neumann algebra framework, highlighting their fundamental role in geometry of interaction.

Findings

MASAs classify linear logic fragments

Modified hyperfinite geometry models proofs as operators

MASA properties influence logic expressivity

Abstract

We show a correspondence between a classification of maximal abelian sub-algebras (MASAs) proposed by Jacques Dixmier and fragments of linear logic. We expose for this purpose a modified construction of Girard's hyperfinite geometry of interaction which interprets proofs as operators in a von Neumann algebra. The expressivity of the logic soundly interpreted in this model is dependent on properties of a MASA which is a parameter of the interpretation. We also unveil the essential role played by MASAs in previous geometry of interaction constructions.