Extended Kripke lemma and decidability for hypersequent substructural logics

Revantha Ramanayake*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)


We establish the decidability of every axiomatic extension of the commutative Full Lambek calculus with contraction FLec 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 FLec by combining structural proof theory and combinatorics. This work significantly extends both ingredients: height-preserving 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.
Original languageEnglish
Title of host publicationProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020)
PublisherACM Press Digital Library
Number of pages12
ISBN (Print)9781450371049
Publication statusPublished - 8-Jul-2020
Externally publishedYes

Cite this