arXiv math/05040652005-04-04math.LOmath.CT

逻辑没有逻辑

Logic Without Syntax

Dominic Hughes

摘要：

本文提出了一个抽象的，数学公式的经典命题逻辑。它一层一层地进行：（1）抽象的、无语法的命题;（2）抽象的、无语法的收缩弱化证明;（3）分布;（4）公理（p或非p）。抽象命题对应于范畴G（Rel^L）的对象，其中G是Hyland-Tan双胶合构造，Rel是集合和关系的标准集范畴，L是文字的集合。抽象证明是Gl（Rel^L）的一个紧正交子范畴的态射，其中我们定义Gl为G的一个松弛变体。证明了L上的自由二元积和范畴（收缩弱化逻辑）是Gl（Rel^L）的一个满子范畴，自由分配格范畴（收缩弱化分配逻辑）是Gl（Rel^L）的一个满子范畴.我们探讨一般的结构，增加公理，这是不是雷尔特定的或（p或不p）特定的。

英文摘要：

This paper presents an abstract, mathematical formulation of classical propositional logic. It proceeds layer by layer: (1) abstract, syntax-free propositions; (2) abstract, syntax-free contraction-weakening proofs; (3) distribution; (4) axioms (p OR NOT p). Abstract propositions correspond to objects of the category G(Rel^L) where G is the Hyland-Tan double glueing construction, Rel is the standard category of sets and relations, and L is a set of literals. Abstract proofs are morphisms of a tight orthogonality subcategory of Gl(Rel^L), where we define Gl as a lax variant of G. We prove that the free binary product-sum category (contraction-weakening logic) over L is a full subcategory of Gl(Rel^L), and the free distributive lattice category (contraction-weakening-distribution logic) is a full subcategory of Gl(Rel^L). We explore general constructions for adding axioms, which are not Rel-specific or (p OR NOT p)-specific.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

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

继续探索

相关论文

命题混合逻辑的语义与语义

Propositional Mixed Logic: Its Syntax and Semantics

在本文中，我们提出了一个命题逻辑（称为混合逻辑）包含不相交的副本的最小，直觉和经典逻辑。我们证明了这个逻辑的Kripke语义的完备性定理。建立了混合逻辑与极小逻辑、直觉逻辑和经典逻辑之间的关系。最后，我们提出了这个逻辑的微积分版本。

2009-05-04math.LO

正则演算I：图形正则逻辑

Regular Calculi I: Graphical Regular Logic

关系的人机工程学语法是什么？在这第一个文件在一系列的两个，回答这个问题，我们定义定期演算：一个适当结构的函子从一个类别表示语法的正规逻辑的类别偏序集，这需要每个对象的偏序集的关系，该类型。我们介绍了两个主要类别的例子，经常演算对应于经常理论，经常演算对应于经常类别。工作在经常演算，我们提出了一个图形框架，作为原始的各种移动的经常逻辑。正则演算的主要定理是正则范畴的语法语义$2$维附加。

2021-09-29math.CTmath.LO

因果关系--一个范畴的视角

Syntax and Consequence Relations -- A Categorical Perspective

在本文中，我们使用一个范畴和函子设置模型的语法和推理逻辑代数签名，扩展以前的工作代数化的逻辑。这项工作的主要特点是，结构性，或变量替换下的不变性，由函性建模，从而在一个更清晰的框架代数语义和代数化。它也提供了一个很好的概念性理解的各种现有的结果已经建立在文献中，并得出一些新的结果。

2021-09-21math.CTmath.LO

一种推理规则的元逻辑：

A Meta-Logic of Inference Rules: Syntax

这项工作的目的是尝试引入元语言，用于处理多结论推理规则，这些规则允许断言的命题和拒绝的命题。被拒绝的命题的存在，特别是反向替换规则的存在，要求对结构性的定义作某些改变。

2014-11-27cs.LOmath.LO

多伴随正规逻辑程序的语法与语义

Syntax and semantics of multi-adjoint normal logic programming

本文提出了多伴随正规逻辑程序，通过在底层格中引入否定算子扩展了原有框架，并给出了其语法语义及确保稳定模型存在性与唯一性的充分条件。

2024-09-24cs.LOmath.LO

循环Henkin逻辑

Cyclic Henkin Logic

在本文中，我们研究了循环Henkin逻辑CHL，一个可以被描述为可证明性逻辑而不需要第三个Löb条件的逻辑，即可证明蕴含可证明可证明（aka原则4）。逻辑CHL确实具有完全模态化的不动点。我们使用循环语法实现这些不动点，这样我们就可以只使用通常的连接词。本文的主要部分致力于发展循环语法的逻辑。许多定理，如多重不动点定理，在这种情况下成为理所当然的事。我们认为，使用循环语法是感兴趣的，即使是经典的勒布逻辑的研究。我们表明，一个版本的de Jongh-Sambin算法可以看作是理论GL^ \circ，即之间的同义词的一半。CHL加上第三个Löb条件和普通Löb逻辑GL。我们的发展表明，一个合适的计算方案的算法是保护递归。我们展示了如何算术解释工作的循环语法。在附录中，我们给出了一些关于方程算术方面的进一步信息。

2021-01-27math.LO

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

论逻辑与集合论的融合

On the Syntax of Logic and Set Theory

我们介绍了一个扩展的命题演算，包括抽象的谓词和量词，采用一个单一的规则，以及一个新的理解模式和原则的外延性，这是取代伯奈斯假设的量词和理解模式的ZF和其他集合论。我们证明了它在任何有限布尔子集格中是相容的。我们调查的二律背反罗素，康托，Burali-Forti，和其他人，并讨论了系统的关系，其他集理论系统ZF，NBG和NF。我们讨论了公理化高阶量化和抽象的两种方法，然后非常简要地讨论了其中一种方法在逻辑之外的数学领域的应用。

2010-03-22math.LO

一阶逻辑对偶

First-Order Logical Duality

从逻辑的角度来看，斯通对偶布尔代数涉及理论在经典命题逻辑和他们的收集模型。理论可以被看作是布尔代数的表示，模型的集合可以被拓扑化，这样理论就可以从它的模型空间中恢复出来。这种情况可以被看作是一种形式上的二元性，它把句法和语义两个范畴联系起来，通过归巢中介成一个共同的二元对象，在这种情况下是2。在目前的工作中，我们推广整个安排从命题的一阶逻辑。用一阶逻辑中的布尔范畴代替布尔代数，用模型的拓扑群胚及其同构代替模型空间。由此产生的句法和语义范畴之间的对偶，首先以逆变附加词的形式表达，通过归巢到一个共同的对偶对象（现在是$\Sets$）中来建立，它一度被视为布尔范畴，一度被视为配备有内在拓扑的广群。我们的研究的总体框架是由拓扑斯理论提供的。直接证明的主要结果，但专家将认识到拓扑思想的背景。事实上，语法和语义之间的对偶性实际上是代数和几何之间的对偶性在隐藏在我们形式理论后面的几何态射的两个方向上的表现。在此过程中，我们通过一个简化的相干拓扑覆盖定理，从一个可判定的相干理论的模型广群中构造了它的分类拓扑。

2013-06-28math.CTmath.LO

递归逻辑框架

Recursive logic frames

我们定义了逻辑框架的概念，它通过增加语法和公理系统的概念来扩展抽象逻辑的概念。在递归逻辑框架中，语法和公理集被递归编码。一个递归逻辑框架称为递归（可数）紧的，如果每个递归（分别，可数）相容理论都有一个模型。我们证明，对于由基数量词构建的逻辑框架，“至少存在λ”，递归紧性总是意味着可数紧性。另一方面，我们证明了一个递归紧的扩张不一定是可数紧的。

2004-05-01math.LO

组合逻辑

Logic of Combinatory Logic

我们开发了一个经典的命题逻辑推理组合逻辑。我们定义了它的语法、公理系统和语义。以经典命题逻辑为基础，以类型化组合项为基本命题，给出了其语法和公理系统，并给出了其语义，该语义基于扩展了与原始组合子相对应的特殊元素的应用结构。无类型组合逻辑的方程理论和所提出的公理系统都被证明是正确和完整的。给出的语义。此外，我们证明了组合逻辑是可靠的和完备的w.r.t.给出的语义。

2022-12-13cs.LOmath.LO

变元函数的一阶导数

The First-Order Syntax of Variadic Functions

本文将一阶逻辑推广到包含变元函数符号，并证明了一个替换引理。给出了两个应用：一个是受囿量词消去，另一个是某些Borel集的可定义性。

2019-11-16math.LO

经典逻辑与直觉主义逻辑之间的伽罗瓦联系。I：

A Galois connection between classical and intuitionistic logics. I: Syntax

在1985年对他的作品集的评论中，Kolmogorov评论说，他1932年的论文“是希望随着时间的推移，解决问题的逻辑[即，直觉主义逻辑]将成为逻辑学[标准]课程的永久部分。一个统一的逻辑装置是打算创建，这将处理两种类型的对象-命题和问题。“我们构造了这样一个形式系统，以及它的谓词版本QHC，它是直觉谓词演算QH和经典谓词演算QC的保守扩展。唯一的新连接词？还有！的QHC诱导伽罗瓦连接（即，QH和QC的Lindenbaum偏序集（即Lindenbaum代数的基础偏序集）之间的一对伴随函子。Kolmogorov的双重否定翻译的命题到问题延伸到一个撤回的QHC到QH;而哥德尔的可证明性翻译的问题到模态命题延伸到一个撤回的QHC到其QC+（？！）片段，用模态逻辑QS 4标识。QH+（！？）片段是一个直觉主义的模态逻辑，它的模态是谁的？在Aczel意义上是一个严格的松弛模态，因此类似于直觉类型理论中的squash/bracket操作。QHC的公理试图对直觉主义逻辑的两个最著名的内容解释给出一个更完整的形式化（相对于直觉主义逻辑的公理）：柯尔莫哥洛夫的问题解释（包含海廷和克赖塞尔的标准改进）和奥尔洛夫和海廷的证明解释（如哥德尔所澄清的）。虽然这两种解释经常被混为一谈，但从QHC公理的观点来看，它们都没有减少到另一个，尽管它们确实重叠。

2022-10-02math.LO

双范畴、双等价与双可解释性

Bicategories, Biequivalence, and Bi-Interpretability

本文通过构造相干理论双范畴与相干范畴双范畴之间的双等价，给出双可解释性的范畴刻画，并利用正合完备化得到两个理论双可解释的充要条件，推广到一阶逻辑常见片段。

2023-07-09math.CTmath.LO

一种学说的几何完备化

The Geometric Completion of a Doctrine

本文提出以Grothendieck拓扑为第二参数的学说几何完备化，证明其幂等且对可表示为连续平坦函子范畴的学说语义不变，并阐明其与其他学说完备化及语法范畴构造的关系。

2023-04-15math.CTmath.LO

无证证明

Proofs Without Syntax

“数学家不关心逻辑，就像逻辑学家不关心数学一样。奥古斯都·德·摩根1868年传统上，证明是句法的、归纳生成的对象。本文提出了一个抽象的数学公式的命题演算（命题逻辑），证明是组合（图论），而不是语法。它定义了一个命题P的组合证明为图同态h：C -> G（P），其中G（P）是与P相关联的图，C是着色图。主要定理是可靠性和完备性：P为真当且仅当存在组合证明h：C -> G（P）。

2006-07-18math.COmath.LO

无语法一阶证明

First-order proofs without syntax

传统上，证明是句法的、归纳生成的对象。本文重新制定了一阶逻辑（谓词演算）的证明，这是图论的，而不是语法。它定义了一个组合证明的公式$ϕ$作为一个松散的纤维化的图与$ϕ$。主要定理是可靠性和完备性：一个公式是有效的当且仅当它有一个组合证明。

2019-06-26math.COmath.LO

一种没有公理的语义情境（理论的非公理化）

A Semantic Situation without Syntax (Non- axiomatizibility of Theories)

本文首先介绍了一个版本的意外绞刑悖论，试图为悖论开辟一条新的途径，为类似于说谎者悖论的悖论提供一种新的解释。同时，我们也将证明我们有一个语义情境，没有任何句法逻辑系统可以支持它。最后，我们提出了一个公理化命题。基于这个主张，拥有一个公理系统的可计算性理论是不可能的。事实上，同样的论证表明，许多其他理论是不可公理化的。(Dare《物理学与数学通论》（General Theories of Physics and Mathematics）

2015-06-26math.LO

意识逻辑：作为句法和语义模型中间地带的Kripke格

Awareness Logic: Kripke Lattices as a Middle Ground between Syntactic and Semantic Models

Center for Information and Bubble Studies, University of Copenhagen（哥本哈根大学信息与泡沫研究中心）

关于认知建模的文献包括无语法和基于语法的框架。Heifetz，Meier \& Schipper（HMS）提出了一个无语法的意识格模型。虽然他们的格方法是优雅和直观的，但它排除了依赖形式语言来归纳格的简单选择，并且没有明确区分不确定性和无意识。与此相反，最突出的基于语法的解决方案，Fagin-Halpern（FH）模型，解释了这种区别，并提供了一个简单的意识表示，但缺乏格结构的直观性。在这里，我们结合这两种方法，通过提供一个格的Kripke模型，诱导原子子集包含，其中不确定性和无意识是分开的。我们证明了我们的模型等价于HMS和FH模型，通过定义它们之间的转换，保留了显式知识的语言公式的满意度，并通过我们和HMS的结果获得完整性。最后，我们证明了Kripke格模型可以被证明等价于FH模型（当意识是命题确定的），也相对于语言的一般意识的逻辑，FH模型最初提出。

2021-06-24cs.AIcs.LOcs.MA

作为组合学的逻辑与计算

Logic and computation as combinatorics

本研究提出基于动态有限图的无句法有限组合框架，统一重构逻辑与计算核心概念，解决直觉主义线性逻辑完全完备性三十年悬题，还衍生出Hopf代数拓展代数应用。

2023-06-13cs.LOmath.COmath.LO

不一致性演算I：句子逻辑

A Calculus of Inconsistency I: Sentential Logic

我们描述了一个图论语法的自指公式以及四值逻辑，包括矛盾和独立的公式。然后，我们探讨在我们的理论中广义真假值表可以实现的程度，并继续描述微积分的模型论，其中允许模型包括矛盾（如“说谎者”）和公式，这些公式作为其结构的一个组成部分。这为我们构建包含矛盾的集合论模型的续集奠定了基础。

2004-09-02math.LO

把主体放回领域：一个两分类项模态逻辑

Putting the Agents back in the Domain: A Two-Sorted Term-Modal Logic

在本文件中，语法和语义将普通的n-代理QML与常数域，非刚性常数，刚性变量，包括两个功能，关系和平等的扩展。此外，代理的数量将被指定公理，从而确保最大的灵活性wrt。代理集合的基数。域，变量和常量将被划分为代理部分和对象部分，语法将被扩展为包括其中模态运算符的索引被量化为语言的wff的字符串。这将增强关于代理人的认知状态的表达能力。这样一个术语模态版本的逻辑K被证明是健全的和完整的WRT。类（适当的）帧，和一个术语版本的S4被证明是健全的和完整的wrt。（适当的）框架类，其中的关系是传递的。应该注意的是，完备性是通过规范模型的框架来展示的，因此允许对K和S4的术语版本之外的其他逻辑进行不复杂的推广。

2018-11-05cs.LOcs.MAmath.LO

无反射拉伸等式的三次插值

Cubical Syntax for Reflection-Free Extensional Equality

我们贡献XTT，观察类型论的立体重建，扩展马丁-洛夫的内涵类型论与依赖的平等类型，享有功能扩展性和判断版本的唯一性的身份类型原则（UIP）：任何两个元素相同的平等类型是判断平等的。此外，我们推测，类型关系可以决定在一个实用的方式。在本文中，我们建立了一个代数规范性定理，使用一个新的立方扩展（独立提出的Awodey）的逻辑家庭或范畴胶合参数的启发Coquand和Shulman：每一个封闭的布尔类型的元素是可导等于要么“真”或“假”。

2019-06-06cs.LOmath.LO