Extended Kripke lemma and decidability for hypersequent substructural logics

Revantha Ramanayake*

*Bijbehorende auteur voor dit werk

OnderzoeksoutputAcademicpeer review

3 Citaten (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.
Originele taal-2English
TitelProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020)
UitgeverijACM Press Digital Library
Aantal pagina's12
ISBN van geprinte versie9781450371049
StatusPublished - 8-jul-2020
Extern gepubliceerdJa

Citeer dit