Proof nets for the Lambek-Grishin calculus

TL;DR

This paper explores proof nets for the Lambek-Grishin calculus, a logical framework combining non-commutative conjunctions and disjunctions with their residuals, and examines their relation to sequent calculus forms.

Contribution

It introduces proof nets for the Lambek-Grishin calculus and analyzes their correspondence with both unfocused and focused sequent calculus versions.

Findings

Proof nets effectively represent Lambek-Grishin calculus proofs.

Clear correspondence established between proof nets and sequent calculus forms.

Enhances understanding of the calculus's proof-theoretic structure.

Abstract

Grishin's generalization of Lambek's Syntactic Calculus combines a non-commutative multiplicative conjunction and its residuals (product, left and right division) with a dual family: multiplicative disjunction, right and left difference. Interaction between these two families takes the form of linear distributivity principles. We study proof nets for the Lambek-Grishin calculus and the correspondence between these nets and unfocused and focused versions of its sequent calculus.