Linear Realisability over nets: multiplicatives (long version)

TL;DR

This paper introduces a new orthogonality-based realisability model for the multiplicative fragment of linear logic, including generalized axioms, with a novel approach to cut elimination, ensuring adequacy and completeness.

Contribution

It presents the first realisability model for MLL with generalized axioms and defines cut elimination in this context, advancing the theoretical understanding of linear logic.

Findings

Model is adequate for MLL and MLL*

Cut elimination is successfully defined for generalized axioms

Model is complete for both MLL and MLL*

Abstract

We provide a new realisability model based on orthogonality for the multiplicative fragment of linear logic, both in presence of generalised axioms (MLL*) and in the standard case (MLL). The novelty is the definition of cut elimination for generalised axioms. We prove that our model is adequate and complete both for MLL* and MLL.