Open AccessOne-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
Author(s) -
Paweł Płaczek
Publication year - 2020
Publication title -
bulletin of the section of logic
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.225
H-Index - 13
eISSN - 2449-836X
pISSN - 0138-0680
DOI - 10.18778/0138-0680.2020.25
Subject(s) - sequent , sequent calculus , natural deduction , mathematics , associative property , cut elimination theorem , noncommutative geometry , bilinear interpolation , discrete mathematics , multiplicative function , pure mathematics , algebra over a field , arithmetic , proof calculus , mathematical proof , mathematical analysis , statistics , geometry
Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-sided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek, we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTime complexity of the multiplicative fragment of NBL.