Paweł Płaczek

The Nonassociative Lambek Calculus (NL) represents a logic devoid of the structural rules of exchange, weakening, and contraction, and it does not presume the associativity of its connectives. Its finitary consequence relation is decidable in polynomial time. However, the addition of classical connectives conjunction and disjunction (FNL) makes the consequence relation undecidable. Interestingly, if these connectives are distributive, the consequence relation is decidable in exponential time. This paper provides the proof, that we can merge classical logic with NL (i.e. BFNL) and intuitionistic logic with NL (i.e. HFNL), and still consequence relations are decidable in exponential time.

Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-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.

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.