Extended Kripke lemma and decidability for hypersequent substructural logics

We establish the decidability of every axiomatic extension of the commutative Full Lambek calculus with contraction FL ec that has a cut-free hypersequent calculus. The axioms include familiar properties such as linearity (fuzzy logics) and the substructural versions of bounded width and weak excluded middle. Kripke famously proved the decidability of FL ec by combining structural proof theory and combinatorics. This work significantly extends both ingredients: heightpreserving admissibility of contraction by internalising a fixed amount of contraction (a Curry's lemma for hypersequent calculi) and an extended Kripke lemma for hypersequents that relies on the componentwise partial order on n-tuples being an ω 2 -well-quasi-order.