Proof nets for display logic

TL;DR

This paper extends proof nets for the Lambek calculus to incorporate display logic connectives, including Galois connections and Grishin interactions, and explores its generative capacity by embedding lexicalized grammars.

Contribution

It introduces a new proof net calculus for the Lambek calculus that naturally handles display logic connectives and demonstrates its expressive power through embedding linguistic grammars.

Findings

Extended proof nets handle display logic connectives effectively

Embedding of lexicalized tree adjoining grammars into Lambek-Grishin calculus

Enhanced understanding of the calculus's generative capacity

Abstract

This paper explores several extensions of proof nets for the Lambek calculus in order to handle the different connectives of display logic in a natural way. The new proof net calculus handles some recent additions to the Lambek vocabulary such as Galois connections and Grishin interactions. It concludes with an exploration of the generative capacity of the Lambek-Grishin calculus, presenting an embedding of lexicalized tree adjoining grammars into the Lambek-Grishin calculus.