Logical foundations for hybrid type-logical grammars

TL;DR

This paper establishes proof-theoretic foundations for hybrid type-logical grammars, combining Lambek and lambda grammars, by proving normalization, subformula property, and developing sequent and proof net calculi.

Contribution

It introduces the first proof-theoretic analysis of hybrid type-logical grammars, enabling future variants and extensions such as non-associative and multimodal systems.

Findings

Proved normalization and subformula property for the calculus

Developed sequent and proof net calculi for hybrid grammars

Facilitated future extensions including non-associative and multimodal versions

Abstract

This paper explores proof-theoretic aspects of hybrid type-logical grammars , a logic combining Lambek grammars with lambda grammars. We prove some basic properties of the calculus, such as normalisation and the subformula property and also present both a sequent and a proof net calculus for hybrid type-logical grammars. In addition to clarifying the logical foundations of hybrid type-logical grammars, the current study opens the way to variants and extensions of the original system, including but not limited to a non-associative version and a multimodal version incorporating structural rules and unary modes.