Linear Logic and the Hilbert Scheme
William Troiani, Daniel Murfet
TL;DR
The paper develops a geometric model for shallow MELL by encoding proofs as closed subschemes $\mathbb{X}(\pi)$ inside ambient projective-scheme products $\mathbb{S}(\pi)$, thereby connecting proof structure to algebraic geometry. The exponential modality is realized via the Hilbert scheme, so that “equations between equations” naturally arise from the exponential rules; invariance under cut-elimination is established through explicit isomorphisms between schemes associated to related proofs. The work provides concrete illustrations (e.g., Church numerals) and shows how diagonals and Segre embeddings capture the logical rules geometrically, offering a bridge between proof theory and scheme theory. It also sketches a path to extend the model to all of MELL via the general Hilbert functor and highlights potential ties to elimination theory and other algebraic-geometric proof-models.
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.