Linear Logic and the Hilbert Scheme

TL;DR

This paper develops a geometric model of shallow multiplicative exponential linear logic using the Hilbert scheme, linking proof theory with algebraic geometry through schemes representing logical proofs and their transformations.

Contribution

It introduces a novel interpretation of shallow MELL proofs as locally projective schemes, demonstrating invariance under cut-elimination and connecting proof transformations with geometric isomorphisms.

Findings

Model is invariant under cut-elimination.

Hilbert scheme captures geometric content of promoted formulas.

Provides detailed examples including Church numerals.

Abstract

We introduce a geometric model of shallow multiplicative exponential linear logic (MELL) using the Hilbert scheme. Building on previous work interpreting multiplicative linear logic proofs as systems of linear equations, we show that shallow MELL proofs can be modeled by locally projective schemes. The key insight is that while multiplicative linear logic proofs correspond to equations between formulas, the exponential fragment of shallow proofs corresponds to equations between these equations. We prove that the model is invariant under cut-elimination by constructing explicit isomorphisms between the schemes associated to proofs related by cut-reduction steps. A key technical tool is the interpretation of the exponential modality using the Hilbert scheme, which parameterizes closed subschemes of projective space. We demonstrate the model through detailed examples, including an analysis of Church numerals that reveals how the Hilbert scheme captures the geometric content of promoted formulas. This work establishes new connections between proof theory and algebraic geometry, suggesting broader relationships between computation and scheme theory.