Proof theory for heterogeneous logic combining formulas and diagrams ---Proof normalization---
Proof theory for heterogeneous logic combining formulas and diagrams ---Proof normalization---
复制标题
结合公式和图的异构逻辑证明理论---证明归一化---
DOI：
10.1007/s00153-020-00759-y
复制
发表时间：
2021
影响因子：
0.3
通讯作者：
Ryo Takemura
中科院分区：
文献类型：
--
作者：
Jeremiah Alberg;Eve Grace;Christopher Kelly;Ryo Takemura;Ryo Takemura
我们扩展自然演绎一阶逻辑（FOL）通过引入图作为组件的正式证明。从FOL的观点出发，我们把一个图看作是某些FOL公式的演绎闭合取。在此观察的基础上，我们首先调查基本的异构逻辑（HL），其中异构推理规则定义在风格的合取引进和消除规则的FOL。通过检查什么是我们的异构证明的弯路，我们讨论了一个消除引入对规则构成了我们的HL，这是相反的，通常在FOL的redex的redex。根据Redex的概念，我们证明了HL的规范化定理，我们给出了异构证明结构的一个特征。我们的HL中的每一个正规证明都是由引入规则的应用和消除规则的应用组成的，这也与FOL中正规证明的通常形式相反。此后，我们扩展了基本的HL的一般消除规则的风格，包括更广泛的异构系统的异构规则。
We extend natural deduction for first-order logic (FOL) by introducing diagrams as components of formal proofs. From the viewpoint of FOL, we regard a diagram as a deductively closed conjunction of certain FOL formulas. On the basis of this observation, we first investigate basic heterogeneous logic (HL) wherein heterogeneous inference rules are defined in the styles of conjunction introduction and elimination rules of FOL. By examining what is a detour in our heterogeneous proofs, we discuss that an elimination-introduction pair of rules constitutes a redex in our HL, which is opposite the usual redex in FOL. In terms of the notion of a redex, we prove the normalization theorem for HL, and we give a characterization of the structure of heterogeneous proofs. Every normal proof in our HL consists of applications of introduction rules followed by applications of elimination rules, which is also opposite the usual form of normal proofs in FOL. Thereafter, we extend the basic HL by extending the heterogeneous rule in the style of general elimination rules to include a wider range of heterogeneous systems.