Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi
任何一组真值函数连接词都有微积分规则，这些规则可以从连接词的真假值表中系统地生成。这样一个逻辑演算产生了一个多结论的自然演绎系统和帕里戈自由演绎的一个版本。排除规则是“一般性的”，但可以系统地简化。削减消除和正常化保持不变。限制到一个单一的公式，在随后产生这些系统的直观版本。这些规则还产生了广义lambda演算，为Curry-Howard同构中的自然演绎证明提供了证明条件。添加一个间接证明规则产生经典的单结论版本的这些系统。根岑的标准系统是作为特例出现的。
2021-05-31 math.LO
The naturality of natural deduction (II). Some remarks on atomic polymorphism
在以前的文件（这是一个起诉），我们研究了提取的证明理论性质的自然演绎推导从他们的非谓词翻译到系统F。我们的主要思想是引入一个扩展的方程理论系统F编纂在语法层面上的一些参数模型中发现的属性。在最近的一系列论文中，提出了一种不同的方法来提取自然演绎推导的证明论性质，方法是定义通常翻译的谓词变体，将直觉命题逻辑嵌入系统F的原子片段。在本文中，我们表明，这种方法找到了一个一般的解释，在我们的方程研究的二阶自然演绎，并提供了一个明确的语义理由参数。
2021-01-04 cs.LO math.LO
Natural Deduction for the Sheffer Stroke and Peirce's Arrow (And Any Other Truth-Functional Connective)
可用于任意有限值逻辑公理化的方法可以应用于经典逻辑的所有真值函数连接词，包括Sheffer笔划（NAND）和Peirce箭头（NOR），以获得合理和完整的内限规则。在自然演绎的标准体系中，对单一结论的限制要求引入额外的规则，以使所产生的体系完整;然而，这些规则仍然是简单的，直接对应于经典的荒谬规则。省略这些规则会导致系统的直觉版本的连接词的问题。
2017-10-25 math.LO
On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
常域逻辑是直觉主义逻辑，它用所谓的全移位公理（forall-shift axiom）进行了扩展，这是一个经典有效的命题，蕴涵了可判定公式上的排中律。令人惊讶的是，这种逻辑是建设性的，到目前为止，这已经证明了削减消除特设的结石。在这里，我们使用自然演绎和Curry-Howard对应的方法来提供一个简单的计算解释的逻辑。
2018-10-18 cs.LO math.LO
A Binary Quantifier for Definite Descriptions in Intuitionist Negative Free Logic: Natural Deduction and Normalisation
本文提出了一种用二元量词$ι$形式化定摹状词的方法，其中$ιx[F, G]$读作“The $F$ is $G$”.给出了直觉负自由逻辑系统中$ι$的引入和消去规则。给出了消除形式为$ιx[F, G]$的极大公式的步骤，并证明了系统中的推论可以被带入范式。
2021-08-04 cs.LO math.LO
Natural Deduction Calculus for First-Order Logic
本文的目的是给出一个易于理解的逐步解释，让感兴趣的人充分认识到自然演绎的一阶逻辑的力量。自然演绎作为一种证明系统，可以用来证明命题逻辑中的各种陈述，但我们将看到它的扩展，以涵盖量词，这使它在解决更复杂的现实世界问题时比命题逻辑更强大。我们首先回顾了逻辑连接词和量词，以商定整篇论文将使用的符号，因为有些作者使用不同的符号来指代同一事物。此外，我们展示了最常用的推理规则。此外，我们给出了一阶逻辑自然演绎的可靠性和完备性。最后，我们解决了从简单到复杂的示例，为您提供了不同的情况，您可以在其中应用证明系统来解决可能遇到的问题。希望这篇文章能有助于使这个主题更容易理解。
2021-08-13 cs.LO math.LO
Hyperformalism for Bunched Natural Deduction Systems
本文探讨了超形式主义在束自然演绎系统中的应用，展示了相关逻辑B如何体现这种形式，并扩展了超形式主义以包含证明本身。
2024-09-16 math.LO
Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation
本文首先证明了直觉主义逻辑中几种经典逻辑公式（非数据第三定律、反证法、皮尔斯定律）之间的等价性。然后，它建立了正确的哥德尔-柯尔莫哥洛夫翻译，其限制的命题的情况下，是由于格利文科。这种转换将一阶逻辑的公式$F$映射为公式$F^{\lnot\lnot}$，使得$F$在经典逻辑中可证明当且仅当$F^{\lnot\lnot}$在直觉主义逻辑中可证明。所有的形式证明都是在自然演绎中提出的。这些问题是众所周知的证明理论事实，但在教科书中，它们往往被忽略或留给读者。由于组合困难的一些必要的正式证明，我们希望这份报告可能是有用的，特别是学生和同事从其他领域。
2016-02-25 math.LO
On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic
直觉主义一阶逻辑用马尔可夫原理的一个限制形式扩展是构造性的，并承认Curry-Howard对应，如Herbelin所示。我们提供了一个更简单的证明结果，然后我们研究直觉一阶逻辑扩展的无限制马尔可夫原理。从经典自然演绎出发，对排中律进行了限制，得到了一个自然演绎系统和一个平行的Curry-Howard同构。我们证明存在量化公式的证明项减少到代表所有可能证人的单个项的列表。作为推论，我们得出该逻辑是Herbrand构造性的：每当它证明任何存在公式时，它也证明该公式的Herbrand析取。最后，使用刚刚介绍的技术，我们还提供了一个新的计算解释的算术与马尔可夫的原则。
2017-10-17 cs.LO math.LO
The naturality of natural deduction
发展罗素的建议，Prawitz展示了如何使用命题直觉二阶逻辑$NI^2$中的蕴涵和二阶量词推导出通常的自然演绎推理规则。然而，众所周知的是，翻译并不保持由可定义连接词的置换转换和直接扩展所引起的派生词之间的同一性关系，至少当$NI^2$的方程理论被假设为仅由$β$和$η$方程组成时是这样。在$NI^2$范畴解释的基础上，我们引入了一类新的方程，它用范畴术语表示解释$NI^2$ -导子的变换所满足的自然性条件.我们表明，罗素-Prawitz翻译不保持身份的证明方面的丰富的系统突出的事实，即自然对应于一个广义的置换原则。我们表明，这些结果概括了一些迄今为止未被注意到的事实，即拉塞尔-普拉维茨翻译将支配析取（和其他可定义的联结词）的方程的特定实例类别映射到已经包含在$βη$方程理论中的方程上。$NI^2$。最后，我们将我们的方法与Ferreira和Ferreira提出的方法进行了比较，并表明自然性条件表明他们的方法可以推广到更广泛的一类公式。
2019-08-29 math.LO
Cut--free sequent calculus and natural deduction for the tetravalent modal logic
{ \em四价模态逻辑}（$\cal TML$）是Font和Rius（\cite{FR2}）定义的两种逻辑之一（另一种是{ \em正常四价模态逻辑} ${\cal TML}^N$），与蒙泰罗的四价模态代数有关。这些逻辑是众所周知的{ \em-邓恩的四值逻辑}的扩展，它结合了多值字符（四价）与模态字符。事实上，$\cal TML$是关于四价模态代数保持真度的逻辑。正如丰特和里乌斯所观察到的，逻辑$\cal TML$和代数之间的联系不如${\cal TML}^N$那么好，但是作为补偿，它具有更好的证明理论行为，因为它具有强充分的根岑演算（参见\cite{FR2}）。本文证明了Font和Rius给出的非线性微积分不具有割消性质。然后，利用Avron，Ben-Naim和Konikowska提出的一般方法（\cite{Avron02}），我们给出了具有割消性质的$\cal TML$的一个代数演算.最后，受后者的启发，我们提出了一个{ \em自然演绎}系统，相对于四价模态逻辑是可靠的和完备的。
2021-01-24 math.LO
Counterfactuals and dependencies on causal teams: expressive power and deduction systems
我们分析了Barbero和Sandu（2018）中引入的观察语言，这些语言允许在统一的框架中讨论干预主义的反事实和函数依赖性。特别是，我们系统地研究了这些语言在因果团队语义的表达能力，我们为每种语言提供了完整的自然演绎演算。作为一个中间步骤的完整性，我们axiomatize语言的因果团队语义的广义版本，这原来是有趣的，也在自己的权利。
2020-04-02 math.LO
A natural deduction system for orthomodular logic
本文提出正交模逻辑的自然演绎系统，证明其非线性非交换性，赋予矢列物理语义并将蕴涵解释为满足演绎定理的 Sasaki 箭头，进而扩展至两个可靠的谓词逻辑系统。
2021-10-12 math-ph math.LO math.MP
Context, Judgement, Deduction
该研究提出判断理论及其演算作为演绎系统的通用研究框架，将依赖类型论、自然演绎纳入其中并展开分析，还拓展至拓扑斯等结构的内部逻辑，为相关领域提供了新的研究视角。
2024-11-01 cs.LO math.CT math.LO
Gödel's Notre Dame Course
这是一个同伴的一份文件的作者题为“哥德尔的自然演绎”，其中提出并作出评论的自然演绎系统哥德尔的未发表的说明，小学逻辑当然，他在圣母大学于1939年。在这篇较早的论文中，人们可以找到哥德尔在巴黎圣母院课程中的笔记的简要摘要。这篇论文本身是一篇论文的同伴，该论文研究了哥德尔的一些哲学观点与一般证明论之间的联系。为了正确地看待先前的论文，这里对这些有趣的笔记进行了更完整的总结，并对它们进行了评论。
2016-11-15 math.HO math.LO
Resource control and strong normalisation
我们介绍了\emph{resource control cube}，一个系统，由八个直观的lambda演算与资源的隐式或显式控制，无论是自然演绎或自然演算。本文介绍了Kesner和Renaud提出的与自然演绎对应的四种立方体演算，以及与λ演算对应的四种立方体演算。该演示文稿是参数化的一组资源（削弱或收缩），这使得一个统一的治疗的八个结石的立方体。简单类型的资源控制立方体一方面将Curry-Howard对应扩展为具有隐式或显式结构规则的直觉自然演绎和直觉推理逻辑，另一方面又与子结构逻辑相关。我们提出了一个通用的交叉型系统的资源控制立方体演算。我们的主要贡献是一个强大的归一化减少在这个立方体的特征。首先，我们证明了可类型性意味着强规范化的“自然演绎基地”的立方体，通过适应reductionmethod。然后，我们证明了可类型性意味着强规范化的“cubes基地”的立方体，通过使用一个组合良好的订单和一个合适的嵌入在“自然演绎基地”。最后，我们证明了强规范化意味着在立方体中使用头部主题扩展的可键入性。所有的证明都是通用的，并且可以通过实例化资源集来针对立方体的每个演算。
2013-05-17 cs.LO math.LO
Propositional Calculus in Coq
我正式的经典命题逻辑在证明辅助Coq的重要定理。主要证明了（1）自然演绎演算的可靠性和完备性，（2）自然演绎演算与Hilbert系统和Hilbert演算的等价性，（3）Hilbert演算的割消元。
2015-03-31 cs.LO math.LO
Gentzen-Mints-Zucker duality
Curry-Howard对应通常被描述为将证明（在直觉自然演绎中）与程序（在简单类型lambda演算中的术语）相关联。然而，这种叙述并不是完美的，因为割消的计算内容和lambda演算的逻辑起源。我们重新审视霍华德的工作，并解释它作为一个同构的一类证明在直观的λ演算和一类简单类型的lambda演算的条款。在我们讲述这个故事时，基本的二重性不是证明和程序之间的二重性，而是在一个共同的逻辑计算数学结构上的局部（λ演算）和全局（λ演算或自然演绎）观点之间的二重性。
2020-08-23 cs.LO math.LO
Strong normalization results by translation
我们证明了强规范化的充分经典的自然演绎（即与合取，析取和置换转换），通过使用翻译成简单类型的Muda-mu-演算。我们还将Mendler关于递归方程的结果推广到这个系统。
2009-05-18 cs.LO math.LO
Cognitive Binary Logic - The Natural Unified Formal Theory of Propositional Binary Logic
本文提出了一种形式化理论，它将命题二元逻辑描述为一种语义封闭的形式语言，并允许在相同的（计算）形式语言中，使用相同的数据结构来表达和测试语法和语义上良好的公式、形式证明（在希尔伯特接受中的可论证性）、演绎（根岑的可论证性观点）、CNF化和解构。本文还指出，认知二元逻辑是一种自我描述的理论，它解构了说谎者悖论。
2011-06-12 cs.LO math.LO
Intuitionistic Existential Instantiation and Epsilon Symbol
本文给出了一个具有存在\实例化规则的直觉谓词逻辑的自然演绎系统，它使用了Hilbert的$\e$ -符号.它相对于直觉谓词逻辑是保守的。我们提供了一个合适的Kripke语义的完整性证明，勾勒出一个正规化证明的方法，调查相关的工作和状态一些开放的问题。我们的系统扩展了直觉系统，由于A. Dragalin和Sh.前原
2012-08-03 cs.LO math.LO
