arXiv math/03013172003-01-27math.LO

经典逻辑的局部性

Locality for Classical Logic

Kai Bruennler

摘要：

在本文中，我们将看到演绎系统的经典命题和谓词逻辑的演算结构。像随机系统一样，它们有一个可接受的截规则。此外，它们具有自顶向下的对称性和一些在微积分中不可用的导子的标准形式。同一性公理、切割、弱化和收缩都可以被简化为原子形式。这导致规则是局部的：它们不需要检查无限大小的表达式。

英文摘要：

In this paper we will see deductive systems for classical propositional and predicate logic in the calculus of structures. Like sequent systems, they have a cut rule which is admissible. In addition, they enjoy a top-down symmetry and some normal forms for derivations that are not available in the sequent calculus. Identity axiom, cut, weakening and also contraction can be reduced to atomic form. This leads to rules that are local: they do not require the inspection of expressions of unbounded size.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

基于Quillen模型结构的有限模型上逻辑局部性概念

Quillen Model Structures-Based Notions of Locality of Logics over Finite Models

局部性是逻辑的一个属性，基于Hanf定理和Gaifman定理，并且在有限模型论的上下文中被证明是非常有用的。本文针对量词秩为k的连续肯定句，给出了局部性的一个同伦变式，即k-逻辑等价下基于Quillen模型范畴的局部性框架。

2020-05-18math.CTmath.LO

剩余格结构中的局部性

Locality in Residuated-Lattice Structures

University of Queensland（昆士兰大学）

研究经典局部性定理（Hanf和Gaifman）在剩余格框架下的成立条件，发现局部性的理解方式与代数性质影响定理成立，通过序解释连接词恢复主要引理。

2026-06-18cs.LOmath.LO

加权结构上一阶逻辑的保秩Gaifman范式

A Rank-Preserving Gaifman Normal Form for First-Order Logic on Weighted Structures

Humboldt-Universität zu Berlin（柏林洪堡大学）；RWTH Aachen University（亚琛工业大学）

本文提出保秩Gaifman范式定理，适用于一阶逻辑及带模计数量词和加权结构逻辑ngFOW+，简化了无处稠密结构上近线性时间算法的元定理证明。

2026-09-30cs.LOmath.LO

经典逻辑在直觉主义逻辑中的复制

Copies of classical logic in intuitionistic logic

经典逻辑（非构造性数学的逻辑）比直觉主义逻辑（构造性数学的逻辑）更强。尽管如此，在直觉主义逻辑中仍然存在经典逻辑的副本。通常在文献中找到的所有副本都是相同的。这就提出了一个问题：副本是唯一的吗？我们通过提供三份不同的副本来否定回答。

2012-11-08math.LO

局部与全局 d-刚性在图的一阶逻辑中不可定义

Local and global $d$-rigidity are not definable in the first order logic of graphs

本文借助 Hanf 局部性和 k-电路图全局刚性结果，证明局部与全局 d-刚性无法在图的一阶逻辑中定义。

2025-11-07math.COmath.LO

二阶经典逻辑和直觉逻辑完备性定理的简化证明

Simple proof of the completeness theorem for second order classical and intuitionictic logic by reduction to first-order mono-sorted logic

本文提出了一种比通常方法更简单的方法，从一阶逻辑推导出二阶经典逻辑的完备性定理。我们也将我们的方法推广到二阶直觉主义逻辑的情形。

2009-05-06math.LO

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

经典逻辑否定片断的代数逻辑

Algebraic logic for the negation fragment of classical logic

本文的总体目标是在当代（抽象）代数逻辑的框架内研究经典逻辑的否定片段。更确切地说，我们将找到与代数逻辑中的逻辑规范相关的三类代数，也就是说，我们找到类$\mathrm{Alg}^*$、$\mathrm{Alg}$和经典逻辑的否定片段的内在多样性。为了实现这一点，首先，我们提出了一个希尔伯特式的公理化这个片段。然后，我们刻画了该逻辑的约简矩阵模型和全广义矩阵模型。此外，我们还对莱布尼茨和弗雷格层次中的否定片段进行了分类。

2023-03-13math.LO

逻辑统一的顺序演算

Sequent calculi for a unity of logic

我们提出了一个新的统一的逻辑，即，一个单一的微积分，体现了经典，直觉和线性逻辑。具体地说，我们定义了经典线性逻辑否定（CLL $^-$），它是一种新的逻辑，它是经典的、线性的，但摒弃了经典线性逻辑中的极性和严格的德摩根定律。然后，我们定义了非线性化和经典化的微积分，使得非线性化映射CLL $^-$（分别为）。直觉线性逻辑（ILL））到经典逻辑（CL）（分别直觉主义逻辑（IL）），和经典化地图IL（分别。ILL）至CL（分别为CLL $^-$）模保守扩张。通过这两个映射，只有ILL的保守扩张的微积分才能满足ILL，IL，CLL $^-$和CL。这一结果实现了一个简单的，高度系统化的逻辑统一，通过丢弃极性和严格的德摩根定律，其中（可以说）只有CLL，并包括统一的经典化和非线性化，其中交换。以前的方法不能满足这些要求。我们的统一也澄清了直觉性和经典性之间的二分法，以及逻辑的线性和非线性之间的二分法，它们是对称的。

2021-01-06math.LO

经典组合逻辑

Classical Combinatory Logic

组合逻辑表明，约束变量可以在不损失表达性的情况下被消除。它在数学基础和函数式编程语言的实现中都有应用。原来的组合演算对应于最小的蕴涵逻辑写在一个系统“`一拉希尔伯特”。本文提出了一种对应于命题经典逻辑的组合逻辑。该系统等同于Barbanera和Berardi的系统$λ^{Sym}_{Prop}$。

2009-05-07math.LO

经典命题逻辑与直觉命题逻辑中变量的可判定性

Classical propositional logic and decidability of variables in intuitionistic propositional logic

我们改进了这个问题的答案：当一个公式中的命题变元在经典命题逻辑中是可证明的时候，在直觉主义命题逻辑中，什么样的被排除的中间集足以证明这个公式。

2014-08-06cs.LOmath.LO

相对于经典逻辑最自然的悖论定义逻辑

The most natural paradefinite logic relative to classical logic

University of Amsterdam（阿姆斯特丹大学）

本文提出，相对于经典逻辑，Belnap-Dunn逻辑通过添加否定和蕴含连接词来形成最自然的悖论定义逻辑。

2026-02-11cs.LOmath.LO

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

Isomorphic Formulae in Classical Propositional Logic

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

2010-10-04math.CTmath.LO

从经典逻辑视角看一种次协调逻辑

A classical-logic view on a paraconsistent logic

本文研究次协调一阶逻辑 LPQ$^{\supset,\mathsf{F}}$，提出其自然演绎证明系统，通过嵌入一阶经典逻辑提供模型论与逻辑论证，并探讨其可判定性及逻辑性质，揭示其与经典逻辑的紧密联系。

2025-09-16cs.LOmath.LO

经典逻辑的Kripke模型

Kripke Models for Classical Logic

我们引入了经典逻辑的Kripke模型的概念，并构造性地证明了它的可靠性和无割完备性。我们讨论的概念和它的潜在应用的新颖性。

2010-06-07cs.LOmath.LO

经典逻辑作为带对偶性的直觉主义逻辑

Classical Logic as Intuitionistic Logic with Duality

University of Southampton（南安普顿大学）；University College London（伦敦大学学院）

本文通过将原子命题替换为字面量并引入原始对偶性，提出一种基于证明论语义的经典逻辑替代方案，表明经典逻辑可视为直觉主义逻辑加上对偶性原则。

2026-10-06cs.LOmath.LO

非经典逻辑中的插值

Interpolation in Non-Classical Logics

Institute of Computer Science of the Czech Academy of Sciences（捷克科学院计算机科学研究所）

本文探讨了非经典逻辑中插值性质的差异，分析了多种逻辑系统中的插值特性及重要实例。

2025-12-01cs.LOmath.LO

在经典高阶逻辑中嵌入和自动化条件逻辑

Embedding and Automating Conditional Logics in Classical Higher-Order Logic

University of Torino（都灵大学）；Freie Universität Berlin（柏林自由大学）；King’s College London（伦敦国王学院）；University of Luxembourg（卢森堡大学）

提出了一种将条件逻辑完全嵌入到经典高阶逻辑中的方法。这种嵌入使得现成的高阶自动定理证明器和模型查找器能够应用于条件逻辑中的推理和关于条件逻辑的推理。

2011-08-17cs.AIcs.LOmath.LO

作为经典逻辑的量子逻辑

Quantum Logic as Classical Logic

我们提出了一个语义表示的标准量子逻辑QL在一个经典的，正常的模态逻辑，这通过一个格嵌入正交模格到布尔代数与一个模态算子。因此，我们的经典逻辑是量子逻辑QL的一个完善。换句话说，我们驳斥了伯克霍夫和冯·诺依曼的经典论点，即量子力学的逻辑（形式特征）将是非经典的，以及普特南的论点，即量子逻辑（他的同类）将是一般命题推理的正确逻辑。量子力学的命题逻辑是模态的，但却是经典的，命题推理的正确逻辑不需要具有外向的量子特征。一个正常的必然模态足以捕捉量子实验中观察的主观性，这要归功于它未能在经典析取上分布。我们结果的关键是把量子否定转化为可观测性的经典否定。

2017-02-07cs.LOmath-phmath.LO