论文标题
直觉句子逻辑的可决定性，并通过依次的微积分身份
Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus
论文作者
论文摘要
本文的目的是双重的：首先，我们提出了一个直觉的非逻辑ISCI的依次的演算，该逻辑是基于Chlebowski和Leszczynska-jasion论文提出的演算，“对直觉逻辑进行了研究，以认同的逻辑进行了研究（Logic 48（48）的二级（48）（48）（4），P。48（4），P。通过获得的系统讨论ISCI可决定性的问题。提到的论文的原始演算没有为ISCI提供可决定性结果。为了获得此结果，有两个问题要解决：所谓的循环特征是直觉逻辑的特征以及由于身份定义规则的形式而导致的subformula属性。我们讨论了克服这些问题的可能路线：我们考虑了一个较弱的subformula属性，并由公式的复杂性守护，该公式可以包括在其中；我们还提出了一个证明搜索程序，以便在失败时，就会存在一种反模型（在ISCI的Kripke语义中）。
The aim of our paper is twofold: firstly we present a sequent calculus for an intuitionistic non-Fregean logic ISCI, which is based on the calculus presented in the paper by Chlebowski and Leszczynska-Jasion, 'An Investigation into Intuitionistic Logic with Identity' (Bulletin of the Section of Logic 48(4), p. 259-283, 2019) and, secondly, we discuss the problem of decidability of ISCI via the obtained system. The original calculus from the mentioned paper did not provide the decidability result for ISCI. There are two problems to be solved in order to obtain this result: the so called loops characteristic for intuitionistic logic and the lack of the subformula property due to the form of the identity-dedicated rules. We discuss possible routes to overcome these problems: we consider a weaker version of the subformula property, guarded by the complexity of formulas which can be included within it; we also present a proof-search procedure such that when it fails, then there exists a countermodel (in Kripke semantics for ISCI).
