矢列式式表列的证明理论：G0型与G3型矢列式演算及完全正规化
Proof theory for sequent-style tableaux: G0- and G3-style sequent calculi and full normalization
浏览论文内容
中文总结 AI 辅助
该研究基于经典命题逻辑的块演算与无切矢列式演算的对应关系，构建了G0T、G3T矢列式演算及NgT自然演绎系统，证明了系统等价性、切消定理与NgT的完全正规化定理。
中文摘要 AI 辅助
矢列式式表列是经典命题逻辑的单侧反驳演算，其反驳树的每个节点携带有限公式块，结构规则被吸收到数据结构和闭合准则中。基于该块演算与无切矢列式演算的对应关系，并遵循Kamide和Negri的研究纲领，我们将该演算重铸为带共享上下文的无结构规则G3型矢列式演算$\boldsymbol{\textsf{G3T}}$，并引入带独立上下文、显式弱化与收缩、广义初始矢列式及原始爆炸规则的G0型矢列式演算$\boldsymbol{\textsf{G0T}}$。我们证明了$\textsf{G0T}$与$\textsf{G3T}$等价的定理，并由此得到$\textsf{G0T}$的切消定理。随后，我们为同一逻辑引入带一般消去规则的自然演绎系统$\boldsymbol{\textsf{NgT}}$，并证明$\textsf{NgT}$的完全正规化定理。该证明通过$\textsf{G0T}$与$\textsf{NgT}$之间的双向翻译实现：正规推导对应无切推导，完全正规形式对应“每个消去规则的大前提均为假设”的规则体系。
英文摘要
Sequent-style tableaux are a one-sided refutation calculus for classical propositional logic, 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. Building on the correspondence between this block calculus and the cut-free sequent calculus, and following the programme of Kamide and Negri, we recast the calculus as a structural-rule-free G3-style sequent calculus $\mathbf{G}_t$ with shared contexts, and we introduce a G0-style sequent calculus $\mathbf{G}_0$ with independent contexts, explicit weakening and contraction, generalized initial sequents, and a primitive explosion rule. A theorem establishing the equivalence between $\mathbf{G}_0$ and $\mathbf{G}_t$ is proved, and the cut-elimination theorem for $\mathbf{G}_0$ is obtained as a consequence. We then introduce a natural deduction system $\mathbf{N}_g$ with general elimination rules matching the left rules of $\mathbf{G}_0$, and we prove a full normalization theorem for $\mathbf{N}_g$. The proof is achieved by means of bidirectional translations between $\mathbf{G}_0$ and $\mathbf{N}_g$: normal derivations correspond to cut-free derivations, and full normal form to the discipline in which every major premiss of an elimination rule is an assumption. We also determine the reach of the formula-succedent fragment, which is shown to have no theorems, so that the equivalence of the three systems is one of consequence and not of theoremhood, and we show that classical logic is recovered on the succedent side, and recovered exactly, by adjoining the rule of indirect proof.
