Master Thesis Presentation - Wouter Leferink

Title: Tight Complexity for Modal Extensions of Lec with K, 4 and T

Abstract:

Substructural logics are defined by dropping some of the structural properties of intuitionistic logic such as commutativity (exchange), contraction, or weakening. Substructural logics with contraction and without weakening can have very high complexity: in particular, FLec, the Full Lambek calculus with exchange and contraction, is complete for the Ackermannian complexity class. Here, `Full' refers to the presence of additive (lattice) connectives; these are used to simulate zero tests in the lower bounding argument. Indeed, Schmitz (2016) showed that its multiplicative fragment Lec has much lower complexity: provability and deduction are 2EXPTIME-complete. In this paper, we investigate the effect of adding the standard modal rules K, 4, and T to this multiplicative setting.

We show that provability in Lec + K remains in 2EXPTIME by extending Schmitz’s expansive BVASS argument. We also obtain Ackermannian lower bounds for Lec + K deducibility and Lec + 4 provability, by constructing reductions from expansive counter machines; the main point here is that the modal rules can be used to simulate zero tests. The reduction to Lec + 4 provability also yields the same lower bound for cut-free Lec + 4 + K. We also show that all of these results hold even in the presence of the T rule. Combined with known results, this yields a tight classification: Lec + K (+ T) provability is 2EXPTIME-complete, Lec + K (+ T) deducibility is Ackermannian-complete, and provability and deducibility in Lec + 4 (+ T) and cut-free Lec + 4 + K (+ T) are Ackermannian-complete.

Supervisors: Revantha Ramanayake, Ivan Bliznets