通过相继式演算判定带同一性的直觉主义命题逻辑的可判定性
计算机科学中的逻辑
2022-04-15 v1
摘要
本文的目的有二：首先我们给出一个直觉主义非弗雷格逻辑 ISCI 的相继式演算，其基于 Chlebowski 与 Leszczynska-Jasion 的论文《直觉主义带同一性逻辑的研究》（Bulletin of the Section of Logic 48(4), p. 259-283, 2019）中提出的演算；其次，我们借助所得系统讨论 ISCI 的可判定性问题。上述论文中的原初演算并未给出 ISCI 的可判定性结果。为获得该结果需解决两个问题：直觉主义逻辑特有的所谓循环，以及由同一性专用规则的形式导致的子公式性质缺失。我们讨论克服这些问题的可能路径：我们考虑一种由可纳入其中的公式复杂度所守卫的较弱子公式性质；我们也给出一个证明搜索过程，当其失败时，则存在一个反模型（在 ISCI 的 Kripke 语义中）。
引用
@article{arxiv.2204.06728,
title = {Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus},
author = {Agata Tomczyk and Dorota Leszczyńska-Jasion},
journal= {arXiv preprint arXiv:2204.06728},
year = {2022}
}
备注
In Proceedings NCL 2022, arXiv:2204.06359