Type logics and pregroups (Q2467212)

The author first outlines several type logics related to the Lambek calculus L as well as their semantical frameworks by linguistic and algebraic means, among them the logic of pregroups, or Compact Bilinear Logic CBL, which is the primary subject of the paper. The main issue is a formalization of an extended sequent system of CBL enjoying the cut-elimination theorem and the normalization theorem (corresponding to the Lambek switching lemma for CBL), with which are obtained the P-TIME decidability (for CBL and the extension) and a faithful interpretation of CBL in L1 (L with the unitary constant 1). The author also surveys the results on pregroups he has established so far, and provides a general construction of (preordered) bilinear algebras and pregroups whose universe is an arbitrary monoid.