首页/论文/0905.1555

arXiv 0905.15552009-05-11math.LO

经典命题自然演绎的可实现性语义

A semantics of realisability for the classical propositional natural deduction

Karim Nour, Khelifa Saber

备注：: Second Workshop on Computational Logic and Applications (CLA 2004), Lyon : France (2004)

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

本文引入了经典命题自然演绎的可实现性语义，并证明了一个正确性定理。这允许表征某些类型化术语的操作行为。

英文摘要：

In this paper, we introduce a semantics of realisability for the classical propositional natural deduction and we prove a correctness theorem. This allows to characterize the operational behaviour of some typed terms.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

全命题经典自然演绎强规范化定理的语义证明

A semantical proof of the strong normalization theorem for full propositional classical natural deduction

本文给出了全命题经典自然演绎的强正规化的一个简短的语义证明。这个证明是由J. - Y. Girard，并由M.帕里戈

2009-05-04math.LO

CZF的一阶逻辑是直觉一阶逻辑

The first-order logic of CZF is intuitionistic first-order logic

证明了CZF的一阶逻辑是直觉一阶逻辑。要做到这一点，我们引入了一个新的超限计算模型（集寄存器机），并结合由此产生的概念与贝丝语义的可实现性。同时，我们还证明了CZF的命题容许规则与直觉命题逻辑的命题容许规则完全相同。

2022-06-09math.LO

经典命题逻辑中的同构公式

Isomorphic Formulae in Classical Propositional Logic

公式之间的同构是相对于在经典命题逻辑和经典线性命题逻辑的乘法片段捕获的证明网的形式化相等的演绎的范畴来定义的。这种平等是由演绎的一般性所驱动的。刻画给出了对同构公式，从而导致决策程序，这种同构。

2010-10-04math.CTmath.LO

Coq语言中的命题演算

Propositional Calculus in Coq

我正式的经典命题逻辑在证明辅助Coq的重要定理。主要证明了（1）自然演绎演算的可靠性和完备性，（2）自然演绎演算与Hilbert系统和Hilbert演算的等价性，（3）Hilbert演算的割消元。

2015-03-31cs.LOmath.LO

从非传统观点看直觉主义势图

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$表示提出的符号将图的通常拓扑的开集、闭集和准开集与直觉命题逻辑联系起来，这对于从更几何的角度来处理这种逻辑表示中的新问题是有用的。

2017-05-26math.LO

依赖命题逻辑

Propositional Logics of Dependence

本文在命题层次上研究依赖逻辑。我们证明了几个有趣的命题依赖逻辑，包括命题依赖逻辑，命题直觉依赖逻辑以及命题查询逻辑，是表达完备的，并且具有析取或合取范式.我们提供了演绎系统，并证明了这些逻辑的完备性定理。

2016-03-07cs.LOmath.LO

更多相关论文收起更多论文

一阶逻辑的自然演绎演算

Natural Deduction Calculus for First-Order Logic

本文的目的是给出一个易于理解的逐步解释，让感兴趣的人充分认识到自然演绎的一阶逻辑的力量。自然演绎作为一种证明系统，可以用来证明命题逻辑中的各种陈述，但我们将看到它的扩展，以涵盖量词，这使它在解决更复杂的现实世界问题时比命题逻辑更强大。我们首先回顾了逻辑连接词和量词，以商定整篇论文将使用的符号，因为有些作者使用不同的符号来指代同一事物。此外，我们展示了最常用的推理规则。此外，我们给出了一阶逻辑自然演绎的可靠性和完备性。最后，我们解决了从简单到复杂的示例，为您提供了不同的情况，您可以在其中应用证明系统来解决可能遇到的问题。希望这篇文章能有助于使这个主题更容易理解。

2021-08-13cs.LOmath.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-25math.LO

自然演绎的自然性（II）。关于原子多态性的几点注记

The naturality of natural deduction (II). Some remarks on atomic polymorphism

在以前的文件（这是一个起诉），我们研究了提取的证明理论性质的自然演绎推导从他们的非谓词翻译到系统F。我们的主要思想是引入一个扩展的方程理论系统F编纂在语法层面上的一些参数模型中发现的属性。在最近的一系列论文中，提出了一种不同的方法来提取自然演绎推导的证明论性质，方法是定义通常翻译的谓词变体，将直觉命题逻辑嵌入系统F的原子片段。在本文中，我们表明，这种方法找到了一个一般的解释，在我们的方程研究的二阶自然演绎，并提供了一个明确的语义理由参数。

2021-01-04cs.LOmath.LO

团队性质的命题逻辑

The Propositional Logic of Team Properties

University of Gothenburg（哥德堡大学）

针对团队语义逻辑缺乏可替换性的问题，提出团队性质逻辑（LTP），通过布尔代数的幂集代数给出语义，并建立了一个可靠且完备的标记自然演绎系统。

2026-07-01math.LO

认知二元逻辑-命题二元逻辑的自然统一形式理论

Cognitive Binary Logic - The Natural Unified Formal Theory of Propositional Binary Logic

本文提出了一种形式化理论，它将命题二元逻辑描述为一种语义封闭的形式语言，并允许在相同的（计算）形式语言中，使用相同的数据结构来表达和测试语法和语义上良好的公式、形式证明（在希尔伯特接受中的可论证性）、演绎（根岑的可论证性观点）、CNF化和解构。本文还指出，认知二元逻辑是一种自我描述的理论，它解构了说谎者悖论。

2011-06-12cs.LOmath.LO

命题叠加逻辑

Propositional superposition logic

我们扩展了经典命题逻辑（PL），增加了一个新的原始二元连接词$φ|ψ$，旨在表示句子$φ$和$ψ$的“叠加”，量子力学的相应概念激发的操作，但不打算捕捉后者的所有方面，因为它们出现在物理学中。为了解释新的连接，我们扩展了经典的布尔语义采用模型的形式$\langle M,f\rangle$，其中$M$是一个普通的二值分配的句子PL和$f$是一个选择功能的所有对经典的句子。在新的语义中，$φ|ψ$被严格地插在$φ\wedgeψ$和$φ\veeψ$之间。通过对选择函数施加若干约束，我们得到了相应的逻辑结果关系和重言式系统的概念，其中$|$满足一些自然代数性质，如结合性、逻辑等价下的闭性和对偶连接词上的分配性.因此，各种系统的命题叠加逻辑（PLS）出现的PL的扩展。这些系统的重言式的公理化和健全的所有这些。证明了这些系统中最弱系统的完备性。对于其他系统，完备性成立，当且仅当每一个相容的句子集合都可扩展为一个相容的完备的句子集合，这个条件的真值与演绎定理的有效性密切相关。

2023-03-27math.LO

自然演绎的自然性

The naturality of natural deduction

发展罗素的建议，Prawitz展示了如何使用命题直觉二阶逻辑$NI^2$中的蕴涵和二阶量词推导出通常的自然演绎推理规则。然而，众所周知的是，翻译并不保持由可定义连接词的置换转换和直接扩展所引起的派生词之间的同一性关系，至少当$NI^2$的方程理论被假设为仅由$β$和$η$方程组成时是这样。在$NI^2$范畴解释的基础上，我们引入了一类新的方程，它用范畴术语表示解释$NI^2$ -导子的变换所满足的自然性条件.我们表明，罗素-Prawitz翻译不保持身份的证明方面的丰富的系统突出的事实，即自然对应于一个广义的置换原则。我们表明，这些结果概括了一些迄今为止未被注意到的事实，即拉塞尔-普拉维茨翻译将支配析取（和其他可定义的联结词）的方程的特定实例类别映射到已经包含在$βη$方程理论中的方程上。$NI^2$。最后，我们将我们的方法与Ferreira和Ferreira提出的方法进行了比较，并表明自然性条件表明他们的方法可以推广到更广泛的一类公式。

2019-08-29math.LO