Topological Observations on Multiplicative Additive Linear Logic

TL;DR

This paper explores the topological structure of strategies in game semantics for Multiplicative Additive Linear Logic, establishing a topological game model, and proving cut elimination, soundness, and completeness.

Contribution

It introduces a topological game model for MALL without propositional variables, demonstrating strategies form a sheaf and establishing cut elimination.

Findings

Proves cut elimination theorem for the topological game model.

Shows strategies form a sheaf in the topological setting.

Establishes soundness and completeness of the model.

Abstract

As an attempt to uncover the topological nature of composition of strategies in game semantics, we present a ``topological'' game for Multiplicative Additive Linear Logic without propositional variables, including cut moves. We recast the notion of (winning) strategy and the question of cut elimination in this context, and prove a cut elimination theorem. Finally, we prove soundness and completeness. The topology plays a crucial role, in particular through the fact that strategies form a sheaf.