Cover Systems for the Modalities of Linear Logic

TL;DR

This paper introduces modal FL-cover systems that combine semantics from Beth-Kripke-Joyal and Girard's interpretation to model Ono's modal FL-algebras, providing a new semantic framework for linear logic modalities.

Contribution

It defines modal FL-cover systems and proves their correspondence with modal FL-algebras, bridging algebraic and semantic perspectives in linear logic.

Findings

Modal FL-cover systems can represent any modal FL-algebra.

The semantics integrate Beth-Kripke-Joyal and Girard's interpretations.

Provides a new semantic foundation for linear logic modalities.

Abstract

Ono's modal FL-algebras are models of an extension of Full Lambek logic that has the modalities ! and ? of linear logic. Here we define a notion of modal FL-cover system that combines aspects of Beth-Kripke-Joyal semantics with Girard's interpretation of the ! modality, and has structured subsets that interpret propositions. We show that any modal FL-algebra can be represented as an algebra of propositions of some modal FL-cover system.