On the logic of \(\beta\)-pregroups (Q2467221)

The paper presents \(\beta\){-pregroups}, i.e., pregroups with modality operators, in the form of a rewriting system, and proves that in a given derivation the non-expanding rules must always preceed non-contracting ones for the derivation to be minimal (normalization theorem). It then presents a sequent system and proves the cut-elimination theorem. For illustration, the paper shows how to use \(\beta\){-pregroups} for linguistic applications. Section 1, Introduction, defines the notions of partially ordered monoid and (proper) pregroup, and gives a theorem with some equalities and inequalities; then it defines types and quasi-pregroups, and states the Lambek switching lemma [\textit{J. Lambek}, ``Type grammar revisited'', Lect. Notes Comput. Sci. 1582, 1--27 (1999; Zbl 0934.03043)]. Section 2, Pregroups, with modalities, defines a pregroup with \(\beta\)-operator and a \(\beta\)-pregroup. It goes on to define rewriting rules that define the free \(\beta\)-pregroup generated by a poset \((P,\leq )\), and illustrates this with an example given by \textit{M. Fadda} [``Towards flexible pregroup grammars'', in: New perspectives in logic and formal linguistics. Roma: Bulzoni Editore, 95--112 (2002)]. From there the author proceeds to prove the following theorem [Normalization theorem for \(\beta\){-pregroups}]: Every minimal derivation is normal. Section 3, Axiom system for pregroups with modalities, presents the rewriting system of Section 2 as a Gentzen-style calculus of sequents and proves cut elimination for systems with modalities.