一句话：通过扩展 Kripke 引理并内化收缩，证明所有具有无割超矢列演算的 FLec 公理扩张可判定。
本文研究交换 Full Lambek 演算加收缩 FLec 的公理扩张的可判定性。作者证明：只要该扩张具有无割超矢列演算，它就是可判定的，覆盖线性（模糊逻辑）以及有界宽度和弱排中律的子结构版本等公理。方法上扩展了 Kripke 的结构证明论与组合学论证：一是通过内化固定量的收缩，给出超矢列演算中保持高度的收缩可容许性，即超矢列的 Curry 引理；二是证明超矢列的扩展 Kripke 引理，其基础是 n 元组按分量偏序构成 ω²-良拟序。该结果将 Kripke 对 FLec 的判定性证明显著推广到一大类公理扩张。
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.
DOI 原文 ·
@inproceedings{paperbot5550,
title = {Extended Kripke lemma and decidability for hypersequent substructural logics},
author = {Revantha Ramanayake},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394802}
}