Elimination and cut-elimination in multiplicative linear logic

TL;DR

This paper models proof structures in multiplicative linear logic using polynomial ideals and demonstrates how cut-elimination corresponds to Buchberger's algorithm for computing Gr"obner bases, linking logic and algebraic geometry.

Contribution

It introduces an algebraic framework for understanding cut-elimination in multiplicative linear logic through polynomial ideals and Gröbner basis computation.

Findings

Proof structures are associated with polynomial ideals representing logical content.

Cut-elimination corresponds to Buchberger's algorithm in elimination theory.

Provides an algebraic perspective on proof normalization in linear logic.

Abstract

We associate to every proof structure in multiplicative linear logic an ideal which represents the logical content of the proof as polynomial equations. We show how cut-elimination in multiplicative proof nets corresponds to instances of the Buchberger algorithm for computing Gr\"obner bases in elimination theory.