直觉主义命题逻辑的相继式式表列
Sequent-style tableaux for intuitionistic propositional logic
浏览论文内容
中文总结 AI 辅助
本文提出用于直觉主义命题逻辑的块演算$\boldsymbol{B}_{ti}$，证明其为多后件相继式演算$\boldsymbol{G}_{ti}$的倒置形式，且相对于克里普克语义可靠完备，具有有限模型性质与析取性质的块理论证明。
中文摘要 AI 辅助
相继式式表列是一种反驳演算，其中反驳树的每个节点携带一个有限公式块，结构规则被吸收进数据结构和闭包准则中。在其最初的经典形式中，它们基于对合德·摩根否定以及互补对出现时的闭包。我们证明这两者都可以舍弃。将无符号公式替换为有符号公式，我们得到了用于直觉主义命题逻辑的块演算$\boldsymbol{B}_{ti}$，其中整个直觉主义特性由一条规则承载，即分解$\boldsymbol{F}(A \to B)$的规则，该规则在传递到子块时删除上下文的$\boldsymbol{F}$部分。由此得到的规则，就表示形式而言，是Fitting的有符号表列的规则；新的是块格式，其中结构规则被吸收而非可容许，以及由此产生的性质。我们确定了这条规则和另一条异常规则的语义原因：在该语言的有符号复合公式中，恰好那些由蕴涵支配的公式无法局部分解，这两种失效分别通过保留主公式和清除上下文得到修复。我们证明$\boldsymbol{B}_{ti}$是多后件相继式演算$\boldsymbol{G}_{ti}$的倒置形式，$\boldsymbol{G}_{ti}$容许结构规则，且$\boldsymbol{B}_{ti}$相对于克里普克语义是可靠且完备的，具有有限模型性质，以及关于析取性质的块理论证明。
英文摘要
Sequent-style tableaux are a refutation calculus in which each node of the refutation tree carries a finite block of formulae and the structural rules are absorbed into the data structure and the closure criterion. In their original, classical form they rest on an involutive De Morgan negation and on closure upon a complementary pair. We show that both may be dispensed with. Replacing unsigned formulae by signed ones, we obtain a block calculus $\mathbf{B}_{ti}$ for intuitionistic propositional logic in which the whole of intuitionism is carried by one rule, the rule decomposing $\mathsf{F}(A \to B)$, which deletes the $\mathsf{F}$-part of the context on passing to the child block. The rules so obtained are, up to the presentation, those of Fitting's signed tableaux; what is new is the block format, in which the structural rules are absorbed rather than admissible, and what follows from it. We identify the semantic reason for this rule and for the one other anomalous one: of the signed compounds of the language, exactly those governed by the implication fail to be locally decomposable, and the two failures are repaired, respectively, by retaining the principal formula and by purging the context. We prove that $\mathbf{B}_{ti}$ is the multiple-succedent sequent calculus $\mathbf{G}_{ti}$ read upside down, that $\mathbf{G}_{ti}$ admits the structural rules, and that $\mathbf{B}_{ti}$ is sound and complete for Kripke semantics, with the finite model property and a block-theoretic proof of the disjunction property.
