Research

Cyclic Nonassociative Bilinear Logic (CyNBL) is a compromise between Nonassociative Linear and Bilinear Logics, where the product is not commutative, but we have only one De Morgan negation.

1. For CyNBL we obtained unusual, one-sided sequent system in which the assumptions (nonlogical axioms) are not axioms but special versions of the cut rule. We essentially restrict the cut rule to avoid typical problems of this rule. Hence, we obtained a constructuve proof that CyNBL without additive constants is a strongly conservative extension of FNL.

   • Sequent Systems for Consequence Relations of Cyclic Linear Logics 2024
2. We can also prove that CyNBL is a strongly conservative extension of FNL by simpler algebraic methods, but the proof is not constructive. The novelty is application of quantales to the logic with nonassociatvie product.

   • Applying Quantales to Lambek Calculi with Cyclic Negation 2026
3. in progress

   Using the method of restricting the cut rule to the assumptions we also prove that CyNBL with additive constants is a strongly conservative extension of FNL, provided that FNL admits only one additive constant - the upper bound. When we admin the lower bound, the extension is not conservative (even weakly).

Full Nonassociative Lambek Calculus (FNL), i.e. Nonassociative Lambek Calculus with additive constants (lattice operators) has undecidable consequence relation, which makes it not very useful in formal linguistics. However, its nonconservative extension - Distributive Full Nonassociative Lambek Calculus (DFNL) in which lattice operators are distributive has decidable conseqence in exponential time. Version without multiplicative constant is even EXPTIME-complete.

1. One of the interesting way of thinking about Lambek Calculus is to treat the connectives as binary modalities. Hence, we can take a different approach - to think about extending some other logic with Lambek modalities instead of extending Lambek Calculus with new connectives and constants. In such a way we can obtain Boolean Full Nonassociative Lambek Calculus (BFNL) which is classical propositional logic extended with NL or, on the other hand, DFNL with a Boolean negation. For this logic we obtained a proof that similarly do DFNL its consequence relation is EXPTIME (without multiplicative unit even EXPTIME-complete).

   • Complexity of Nonassociative Lambek Calculus with Classical and Intuitionistic Logic 2026
   • Complexity of Nonassociative Lambek Calculus with classical logic 2024
2. As a natural continuation we can consider other extensions of DFNL. Heyting Full Nonassociative Lambek Calculus (HFNL) is intuitionistic logic extended with NL or DFNL with intuituonistic implication. For this logic the consequence relation is also EXPTIME.

   • Complexity of Nonassociative Lambek Calculus with Classical and Intuitionistic Logic 2026

Nonassociative Bilinear Logic is Girard's Mulitplicative-Additive Linear Logic without assumption of associativity or commutativity of the product (multiplicative conjunction). One of its significant features is a pair of involutive negations, which can be treated as left and right negation.

1. For this logic we obtained a one-sided (left-sided) sequent system, which is much easier to use in research than typical two-sided system (e.g. intuitionistic). This system admits cut elimination.

   • One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity 2021
2. Multiplicative part of this logic (without addtivie connectives and constants) is decidable in polynomial time (PTIME). This extends the previous result of Buszkowski, who proved this property for the version without additive constants.

   • One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity 2021
3. in progress

   Moreover, multiplicative part (either with or without multiplicative constants) has decidable consequence relation in PTIME. The logic with additive connectives has undecidable consequence relation, because it is a strongly conservative extension of FNL.