Intuitionistic First-Order Linear Logic and Hypergraph Languages

Non-commutative substructural logics have several points of contact with the theory of formal languages. On the one hand, such logics, for example, the Lambek calculus, are used as a mechanism for specifying formal languages ​​in categorical grammars. On the other hand, formal languages ​​arise as models of substructural logics; the main result in this direction, proved by M.R. Pentus, states that the Lambek calculus is correct and complete with respect to language semantics.
We will discuss similar relationships between first-order substructural logics and hypergraph languages. In the first part of the talk, we will propose a definition of hypergraph L-grammars based on an arbitrary first-order logic L (in sequential format). It generalizes the concept of MILL1 grammars, that is, categorical grammars based on the multiplicative intuitionistic first-order linear logic MILL1. The latter were considered in [Moot, 2014], [Slavnov, 2023]. We will show the connection between hypergraph MILL1 grammars, as well as grammars over the intuitionistic first-order linear logic ILL1, and generative hypergraph grammars. As a consequence, we will answer the open question from [Moot, 2014] about the class of languages ​​defined by string MILL1 grammars; in particular, we will show that this class contains an NP-complete language.
In the second part of the talk, we will define a language semantics for the logic MILL1, in which formulas are interpreted by hypergraph languages, and the multiplicative conjunction (tensor) of linear logic is interpreted by the parallel composition operation. This operation is well known in the theory of graph grammars in the context of HR-algebras [Courcelle, 1990]. We will establish a soundness and completeness theorem for the negative fragment of MILL1 (using an analogue of the construction in [Buszkowski, 1982]). The question of the completeness of the entire logic MILL1 with respect to hypergraph-language semantics remains open.
The talk is based on the preprint https://arxiv.org/abs/2502.05816.