Description

• Title:
  Sequent Systems for Consequence Relations of Cyclic Linear Logics
• Creator:
  Płaczek, Paweł
• Contributor:
  WSB Merito University in Poznań, Faculty of Finance and Banking, Poznań, Poland;
  pawel.placzek@poznan.merito.pl
• Description:
  Linear Logic is a versatile framework with diverse applications in computer science and mathematics. One intriguing fragment of Linear Logic is Multiplicative-Additive Linear Logic (MALL), which forms the exponential-free component of the larger framework. Modifying MALL, researchers have explored weaker logics such as Noncommutative MALL (Bilinear Logic, BL) and Cyclic MALL (CyMALL) to investigate variations in commutativity. In this paper, we focus on Cyclic Nonassociative Bilinear Logic (CyNBL), a variant that combines noncommutativity and nonassociativity. We introduce a sequent system for CyNBL, which includes an auxiliary system for incorporating nonlogical axioms. Notably, we establish the cut elimination property for CyNBL. Moreover, we establish the strong conservativeness of CyNBL over Full Nonassociative Lambek Calculus (FNL) without additive constants. The paper highlights that all proofs are constructed using syntactic methods, ensuring their constructive nature. We provide insights into constructing cut-free proofs and establishing a logical relationship between CyNBL and FNL.
• Object availability:
  free access
• Rights: https://creativecommons.org/licenses/by-nc-nd/4.0
• Date:
  2024.06.24;
  2024.04.24
• Type:
  Article
• Language:
  English
• Format:
  application/pdf
• Publisher:
  Wydawnictwo Uniwersytetu Łódzkiego
• Relation:
  Bulletin of the Section of Logic;2;
  53
• Subject:
  linear logic;
  Lambek calculus;
  nonassociative logics;
  noncommutative logics;
  substructural logics;
  consequence relation;
  nonlogical axioms;
  conservativeness
• Identifier:
  0138-0680;
  http://hdl.handle.net/11089/52599 ;
  2449-836X;
  10.18778/0138-0680.2024.06
• Data provider:
  Repozytorium Uniwersytetu Łódzkiego
• Can I use it?:
  check license
• Type:
  image