One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity | Zendy

Paweł Płaczek | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

One-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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research