A semantical proof of the strong normalization theorem for full propositional classical natural deduction
Karim Nour, Khelifa Saber
本文给出了全命题经典自然演绎的强正规化的一个简短的语义证明。这个证明是由J. - Y. Girard，并由M.帕里戈
We give in this paper a short semantical proof of the strong normalization for full propositional classical natural deduction. This proof is an adaptation of reducibility candidates introduced by J.-Y. Girard and simplified to the classical case by M. Parigot.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
A semantics of realisability for the classical propositional natural deduction
本文引入了经典命题自然演绎的可实现性语义，并证明了一个正确性定理。这允许表征某些类型化术语的操作行为。
Isomorphic Formulae in Classical Propositional Logic
公式之间的同构是相对于在经典命题逻辑和经典线性命题逻辑的乘法片段捕获的证明网的形式化相等的演绎的范畴来定义的。这种平等是由演绎的一般性所驱动的。刻画给出了对同构公式，从而导致决策程序，这种同构。
Propositional Calculus in Coq
我正式的经典命题逻辑在证明辅助Coq的重要定理。主要证明了（1）自然演绎演算的可靠性和完备性，（2）自然演绎演算与Hilbert系统和Hilbert演算的等价性，（3）Hilbert演算的割消元。
Intuitionistic Existential Graphs from a non traditional point of view
在这篇文章中，我们发展了Arnol Oostra [4]提出的直觉主义存在图的一个新版本。本文中提出的演绎规则与Yuri Poveda [5]的工作中描述的规则具有相同的含义，因为根据切割奇偶性的演绎被消除，并被递归规则的有限集所取代。这样，直觉命题逻辑的存在图系统$ Alfa_I $遵循Poveda [5]描述的系统$ Alfa_0 $的演绎规则的过程，并且等价于直觉命题演算。在这种表示中，$ Alfa_0 $系统得到了改进，引入了一系列以前没有考虑过的二次演绎规则，这些规则允许更好地管理演绎，最后，从Van Dalen [6]提出的思想出发，在演绎技术中引入了一种混合物，Gentzen系统的自然演绎与新的系统规则$ Alfa_0 $和$ Alfa_I $相结合。为$Alfa_I$表示提出的符号将图的通常拓扑的开集、闭集和准开集与直觉命题逻辑联系起来，这对于从更几何的角度来处理这种逻辑表示中的新问题是有用的。
Natural Deduction Calculus for First-Order Logic
本文的目的是给出一个易于理解的逐步解释，让感兴趣的人充分认识到自然演绎的一阶逻辑的力量。自然演绎作为一种证明系统，可以用来证明命题逻辑中的各种陈述，但我们将看到它的扩展，以涵盖量词，这使它在解决更复杂的现实世界问题时比命题逻辑更强大。我们首先回顾了逻辑连接词和量词，以商定整篇论文将使用的符号，因为有些作者使用不同的符号来指代同一事物。此外，我们展示了最常用的推理规则。此外，我们给出了一阶逻辑自然演绎的可靠性和完备性。最后，我们解决了从简单到复杂的示例，为您提供了不同的情况，您可以在其中应用证明系统来解决可能遇到的问题。希望这篇文章能有助于使这个主题更容易理解。
Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation
本文首先证明了直觉主义逻辑中几种经典逻辑公式（非数据第三定律、反证法、皮尔斯定律）之间的等价性。然后，它建立了正确的哥德尔-柯尔莫哥洛夫翻译，其限制的命题的情况下，是由于格利文科。这种转换将一阶逻辑的公式$F$映射为公式$F^{\lnot\lnot}$，使得$F$在经典逻辑中可证明当且仅当$F^{\lnot\lnot}$在直觉主义逻辑中可证明。所有的形式证明都是在自然演绎中提出的。这些问题是众所周知的证明理论事实，但在教科书中，它们往往被忽略或留给读者。由于组合困难的一些必要的正式证明，我们希望这份报告可能是有用的，特别是学生和同事从其他领域。
The naturality of natural deduction (II). Some remarks on atomic polymorphism
在以前的文件（这是一个起诉），我们研究了提取的证明理论性质的自然演绎推导从他们的非谓词翻译到系统F。我们的主要思想是引入一个扩展的方程理论系统F编纂在语法层面上的一些参数模型中发现的属性。在最近的一系列论文中，提出了一种不同的方法来提取自然演绎推导的证明论性质，方法是定义通常翻译的谓词变体，将直觉命题逻辑嵌入系统F的原子片段。在本文中，我们表明，这种方法找到了一个一般的解释，在我们的方程研究的二阶自然演绎，并提供了一个明确的语义理由参数。
Propositional Team Logics
我们考虑命题逻辑的团队语义，继续我们以前的工作（Yang & Väänänen 2016）。在团队语义学中，命题公式的真值被认为是一组估值，称为团队，而不是个人估值。这就有可能赋予依赖、独立和包容等概念以意义。我们定义了一个表达极大的命题组逻辑，称为全命题组逻辑。这需要超越经典命题逻辑的逻辑运算。我们展示了一个层次的逻辑之间的最小的，即经典命题逻辑，并充分命题队逻辑。我们用几种方式来描述这些不同的逻辑：首先是语法上的逻辑运算，然后是语义上的它们能够定义的团队集合。在一些重要的情况下，我们能够找到这些逻辑的完整公理化。
Cognitive Binary Logic - The Natural Unified Formal Theory of Propositional Binary Logic
本文提出了一种形式化理论，它将命题二元逻辑描述为一种语义封闭的形式语言，并允许在相同的（计算）形式语言中，使用相同的数据结构来表达和测试语法和语义上良好的公式、形式证明（在希尔伯特接受中的可论证性）、演绎（根岑的可论证性观点）、CNF化和解构。本文还指出，认知二元逻辑是一种自我描述的理论，它解构了说谎者悖论。
Yet Another Proof of Glivenko's Theorem
本文给出了Glivenko定理的另一种证明，即公式$ϕ$在经典命题逻辑中是可证的当且仅当$\neg\negϕ$在直觉命题逻辑中是可证的.我们在根岑的自然演绎系统中工作，关键引理表明，在任何证明中，只需要一次反证法的应用。
Propositional superposition logic
我们扩展了经典命题逻辑（PL），增加了一个新的原始二元连接词$φ|ψ$，旨在表示句子$φ$和$ψ$的“叠加”，量子力学的相应概念激发的操作，但不打算捕捉后者的所有方面，因为它们出现在物理学中。为了解释新的连接，我们扩展了经典的布尔语义采用模型的形式$\langle M,f\rangle$，其中$M$是一个普通的二值分配的句子PL和$f$是一个选择功能的所有对经典的句子。在新的语义中，$φ|ψ$被严格地插在$φ\wedgeψ$和$φ\veeψ$之间。通过对选择函数施加若干约束，我们得到了相应的逻辑结果关系和重言式系统的概念，其中$|$满足一些自然代数性质，如结合性、逻辑等价下的闭性和对偶连接词上的分配性.因此，各种系统的命题叠加逻辑（PLS）出现的PL的扩展。这些系统的重言式的公理化和健全的所有这些。证明了这些系统中最弱系统的完备性。对于其他系统，完备性成立，当且仅当每一个相容的句子集合都可扩展为一个相容的完备的句子集合，这个条件的真值与演绎定理的有效性密切相关。
The naturality of natural deduction
发展罗素的建议，Prawitz展示了如何使用命题直觉二阶逻辑$NI^2$中的蕴涵和二阶量词推导出通常的自然演绎推理规则。然而，众所周知的是，翻译并不保持由可定义连接词的置换转换和直接扩展所引起的派生词之间的同一性关系，至少当$NI^2$的方程理论被假设为仅由$β$和$η$方程组成时是这样。在$NI^2$范畴解释的基础上，我们引入了一类新的方程，它用范畴术语表示解释$NI^2$ -导子的变换所满足的自然性条件.我们表明，罗素-Prawitz翻译不保持身份的证明方面的丰富的系统突出的事实，即自然对应于一个广义的置换原则。我们表明，这些结果概括了一些迄今为止未被注意到的事实，即拉塞尔-普拉维茨翻译将支配析取（和其他可定义的联结词）的方程的特定实例类别映射到已经包含在$βη$方程理论中的方程上。$NI^2$。最后，我们将我们的方法与Ferreira和Ferreira提出的方法进行了比较，并表明自然性条件表明他们的方法可以推广到更广泛的一类公式。
Kalmár-style constructive completeness proofs for classical positive propositional calculi
本文通过改编 Kalmár 完备性证明方法，构造性地证明了多个经典正命题演算（含 Peirce 律）的完备性，并利用定义析取等技巧简化了相关演算的完备性推导。
A natural deduction system for orthomodular logic
本文提出正交模逻辑的自然演绎系统，证明其非线性非交换性，赋予矢列物理语义并将蕴涵解释为满足演绎定理的 Sasaki 箭头，进而扩展至两个可靠的谓词逻辑系统。
A propositional cirquent calculus for computability logic
本文提出CL18公理化系统，用于可计算性逻辑的基本命题片段，并证明其相对于该逻辑博弈语义的可靠性与完备性。
A completeness theorem in proof-theoretic semantics via set-theoretic semantics
本文以原子二阶直觉主义命题逻辑为系统，借助 Okada 与 Takemura 的带证明项相语义构造闭项论域模型，从而证明直觉主义逻辑相对于 Prawitz 证明论有效性的完备性。
Fundamental Propositional Logic with Preconditional: Strong Completeness, Finite Model Property, and Modal Translations
研究带前提条件的基本命题逻辑，通过给出后承关系表示结合基本逻辑与前提条件，研究其扩展$\mathsf{T}$和$\mathsf{F}$，证明强完备性与有限模型性质，适配模态嵌入到正交$\mathsf{S4}$和直觉主义$\mathsf{KTB}$，给出新条件从句及框架构造。
Wright's First-Order Logic of Strict Finitism
本文将 Yamada 对 Wright 严格有穷主义逻辑的经典命题重构扩展为一阶逻辑，给出可靠完备的 Kripke 式语义和自然演绎系统，并说明其与既有结果的关系。
Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculi
本文给出了Berardi和Barbanera [1]的命题逻辑公式的强正规化的一个算术证明，它可以看作是经典命题逻辑在自然演绎风格下的公式-类型转换.然后，我们给出了Curien和Herbelin [3]所提出的带否定项的隐式部分-在本文中，我们采用David和Nour [4]的方法来证明强正规化。在我们的证明的新颖性是放大序列的redexes的概念，这使我们直接证明的主要定理。
Uniform Interpolation
本文通过Pitts定理，利用对偶性语义证明直觉主义命题逻辑的统一插值性质，并推广到Esakia空间的开映射定理，探讨其在范畴逻辑、代数和模型论中的联系。
Wijesekera-style constructive modal logics
我们定义了一个命题构造性模态逻辑族，每个模态逻辑对应于一个不同的经典模态系统。逻辑定义在风格的Wijesekera的建设性模态逻辑，并证明理论和语义动机。一方面，它们对应于经典模态逻辑的标准演算的单一后继限制。另一方面，它们是通过将直觉Kripke模型的遗传性纳入模态公式的经典满足子句而获得的。我们表明，对于所考虑的经典逻辑，证明理论和语义方法返回相同的建设性系统。
A logic of judgmental existence and its relation to proof irrelevance
本文提出一个自然演绎系统处理“存在证明”的判断，内化为模态概念，关联截断与松弛模态，并给出 Curry-Howard 计算解释，证明系统具有强规范化等性质。
Embedding Modal Logics into Logics of Bunched Implications
本文给出S4嵌入BBI的全新句法证明，证明其在S4任意公理扩张下稳定，可扩展至BBI的多种语言扩张，还给出BBI演绎定理的首个完整证明。
Semantical Investigations on Non-classical Logics with Recovery Operators: Negation
本研究以拓扑布尔代数为基础，采用高阶逻辑元语言与Isabelle/HOL证明助手，为带恢复算子的非经典否定逻辑提供语义，构建拓扑对立立方并实现多阶量化的统一刻画，推动非经典逻辑的计算机辅助研究。
A Subatomic Proof System for Decision Trees
我们设计了一个证明系统的命题经典逻辑，集成了两种语言的布尔函数：标准的合取-析取-否定和二进制决策树。我们给出了两个这样做的理由。第一个是证明理论的自然性：该系统由最近引入的亚原子逻辑的单一，简单，线性方案产生的所有推理规则组成。由于这种规律性，通过自然的结构消除了切口。第二个原因是系统生成有效的证明。事实上，我们表明，由于Statman，这不能有更好的比指数切割免费证明在微积分的重言式的某一类，有多项式切割免费证明在我们的系统。我们通过使用与切消元相同的结构来实现这一点。总之，通过扩展命题逻辑的语言，我们使其证明理论更加规则，并生成更多的证明，其中一些是非常有效的。这种设计是通过将原子视为其真值的叠加而实现的，这些真值由自对偶、非交换连接词连接。然后，一个证明可以通过每个原子投影成两个证明，每个真值一个，而不需要切割。这些投射在语义上是自然的，是本文结构的核心。为了适应自对偶的非交换性，我们在深度推理中组合证明。
Proof theory for sequent-style tableaux: G0- and G3-style sequent calculi and full normalization
该研究基于经典命题逻辑的块演算与无切矢列式演算的对应关系，构建了G0T、G3T矢列式演算及NgT自然演绎系统，证明了系统等价性、切消定理与NgT的完全正规化定理。
Computable Quantification in Reflective Grounded Arithmetic
研究提出自反基础算术RGA，其真值基于计算，全称量化自反。允许递归定义并证明加法乘法全性，能表示递归可枚举集且一致。经机器验证有可靠性、一致性等多种性质，所得逻辑处于独特子结构角落。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。