一句话:证明半格相关逻辑 S 的判定问题不可判定,推翻其可判定猜想。
半格相关逻辑 S 由 Urquhart 于 1972/1973 年提出,其判定问题长期开放。尽管 Urquhart 1984 证明了许多相关逻辑不可判定,但这些技术未能处理 S,因而包括 Urquhart 2016 在内的专家猜测 S 可判定。本文通过将铺砖问题解释到 S 中,构造出从铺砖问题到 S 的归约,从而证明 S 的判定问题是不可判定的。这一结果否定了先前的可判定性猜想,表明 S 与许多相关逻辑一样不可判定,并为该类逻辑的判定性边界提供了新的反例。
Since the introduction of the semilattice relevant logic S by [Urquhart 1972, 1973], its decision problem has persisted as an open problem. [Urquhart 1984] showed that many relevant logics are undecidable, yet S eluded these techniques. Eventually, this led experts, including [Urquhart 2016], to conjecture that S is decidable. Contrary to this conjecture, by interpreting a tiling problem, we show that S is undecidable.