理由逻辑（一）

1. 为什么要论证逻辑？

1.1 认知传统

1.2 数理逻辑传统

1.3 超内涵性

2. 论证逻辑的基本组成部分

2.1 证明逻辑的语言

2.2 基本调整逻辑J0

2.3 逻辑意识和恒定规范

2.4 扩展基本调整逻辑

2.5 事实

2.6 积极自省

2.7 消极内省

2.8 Geach 逻辑及更多

3. 语义

3.1 J 的单主体可能的世界合理性模型

3.2 弱完备性和强完备性

3.3 单代理家族

3.4 单一世界理由模型

3.5 本体透明语义

3.6 与意识模型的联系

4. 实现定理

5. 概括

5.1 混合显性知识和隐性知识

5.2 多智能体可能的世界合理性模型

6. 罗素的例子：诱导事实

7. 理由的自我指涉

8. 论证逻辑中的量词

9. 历史注释

参考书目

学术工具

其他互联网资源

相关条目

1. 为什么要论证逻辑？

论证逻辑是认知逻辑，它允许知识和信念模态被“展开”为论证术语：而不是◻X，我们写成t：X，并将其读作“X由理由t证明是合理的”。人们可能会认为传统的模态运算符是隐式模态，而论证术语是它们的显式阐述，它用更细粒度的认知机制补充了模态逻辑。理由术语族具有结构和操作。操作的选择会产生不同的论证逻辑。对于所有常见的认知逻辑，它们的模态可以完全展开为明确的论证形式。在这方面，论证逻辑揭示并使用了传统认知模态逻辑的显式但隐藏的内容。

论证逻辑起源于一个成功项目的一部分，该项目为直觉逻辑提供了一种建设性的语义——论证术语抽象出了数学证明中除了最基本的特征之外的所有特征。证明也许是最纯粹形式的论证。随后论证逻辑被引入形式认识论。本文介绍了目前理解的论证逻辑的一般范围。它讨论了它们与传统模态逻辑的关系。除了技术机制之外，本文还探讨了明确论证术语的使用如何阐明许多传统哲学问题。整个学科仍在积极发展中。

证明逻辑的根源可以追溯到许多不同的来源，其中两个来源被详细讨论：认识论和数理逻辑。

1.1 认知传统

至少自 von Wright 和 Hintikka 以来，知识和信仰的属性一直是形式逻辑的主题（Hintikka 1962，von Wright 1951）。知识和信仰都以一种现在非常熟悉的方式被视为模态——认知逻辑。但在柏拉图关于知识的三个标准中，合理的、真实的、信念（Gettier 1963，Hendricks 2005），认知逻辑只适用于其中的两个。可能的世界和不可区分性塑造了信念——人们相信在所有情况下都认为可能的事情。事实性带来了真实性的成分——如果现实世界中的某件事不是这样的，那么它就无法被知道，只能被相信。但没有说明合理性条件。尽管如此，模态方法在丰富的数学理论和应用的发展方面取得了巨大的成功（Fagin、Halpern、Moses 和 Vardi 1995，van Ditmarsch、van der Hoek 和 Kooi 2007）。但这还不是全部。

从某种意义上说，知识逻辑的模态方法是围绕全称量词构建的：如果 X 在所有情况下都为真，则在某种情况下 X 是已知的，并且与该情况无法区分。另一方面，论证将存在量词引入其中：如果在某种情况下存在 X 的论证，则 X 在该情况下是已知的。这种普遍/存在二分法对于逻辑学家来说是熟悉的——在形式逻辑中，当且仅当 X 在所有逻辑模型中都为真时，才存在公式 X 的证明。人们认为模型本质上是非建设性的，而证明则是建设性的。像数学证明一样思考一般的论证是不会出错的。事实上，第一个论证逻辑被明确设计为捕获算术中的数学证明，这将在 1.2 节中进一步讨论。

在论证逻辑中，除了公式类别之外，还有第二类论证。理由是正式术语，由使用各种操作符号的常量和变量构建而成。常量代表普遍接受的真理（通常是公理）的理由。变量表示未指定的理由。不同的理由逻辑在允许哪些操作（以及其他方面）方面有所不同。如果 t 是论证项且 X 是公式，则 t:X 是公式，并且应理解为：

t 是 X 的理由。

所有论证逻辑都共有的一种运算是应用，其写法类似于乘法。这个想法是，如果 s 是 A→B 的理由，t 是 A 的理由，那么 [s⋅t] 是 B[1] 的理由。也就是说，通常假设以下内容的有效性：

s:(A→B)→(t:A→[s⋅t]:B)。

这是知识算子和模态算子的通常分布性的显式版本，跨含义：

◻(A→B)→(◻A→◻B)。

事实上，公式（2）背后隐藏着许多逻辑全知的问题。它断言代理人知道代理人知识所暗示的一切——知识在结果下是封闭的。虽然原则上可知、可知性在结果下是封闭的，但对于实际知识的任何合理版本来说，情况却并非如此。 (1) 和 (2) 之间的区别可以在讨论 Goldman 和 Kripke 的典型 Red Barn 例子时加以利用；这是故事的简化版本（Dretske 2005）。

假设我开车经过一个街区，在我不知道的情况下，那里散布着纸浆谷仓，我看到我前面的物体是一个谷仓。因为我有谷仓在我面前的知觉，所以我相信我面前的物体是谷仓。我们的直觉表明我不了解谷仓。但现在假设附近没有假的红色谷仓，而且我也注意到我前面的物体是红色的，所以我知道那里有一个红色谷仓。这种并置，作为一个红色谷仓，我知道，意味着有一个谷仓，而我不知道，“这是一种尴尬”。

在红谷仓示例的第一个形式化中，逻辑推导将以基本模态逻辑进行，其中◻被解释为“信念”模态。然后，根据问题的描述，◻的一些出现将被外部解释为“知识”。设 B 为句子“我面前的物体是谷仓”，令 R 为句子“我面前的物体是红色的”。

◻B，“我相信我面前的物体是一个谷仓”；

◻(B∧R)，“我相信我面前的物体是一个红色谷仓”。

在元层面上，2实际上是知识，而从问题描述来看，1并不是知识。

◻(B∧R→B)，逻辑公理的知识断言。

在这种形式化中，似乎违反了模态形式 (2) 的认知封闭：第 2 行，◻(B∧R) 和第 3 行，◻(B∧R→B) 是知识的情况，而 ◻B（行1）不是知识。这里的模态语言似乎并不能帮助解决这个问题。

接下来考虑论证逻辑中的红谷仓示例，其中 t:F 被解释为“我因理由 t 而相信 F”。令 u 为相信 B 的具体个人理由，而 v 为相信 B∧R 的具体个人理由。另外，设a为逻辑真值B∧R→B的证明。那么假设列表是：

u:B，“u是相信我面前的物体是谷仓的理由”；

v:(B∧R)，‘v是相信我面前的物体是红色谷仓的理由’；

a:(B∧R→B)。

在元层面上，问题描述指出 2 和 3 是知识的情况，而不仅仅是信念，而 1 是信念，但不是知识。正式推理如下：

a:(B∧R→B)→(v:(B∧R)→[a⋅v]:B)，由原理(1)；

v:(B∧R)→[a⋅v]:B，由 3 和 4，通过命题逻辑；

[a⋅v]:B，根据命题逻辑，从 2 到 5。

请注意，结论 6 是 [a⋅v]:B，而不是 u:B ；认知封闭成立。通过论证逻辑推理，得出的结论是 [a⋅v]:B 是一个知识案例，即“我因为 a⋅v 的原因知道 B”。 u:B 不是知识的情况这一事实并不会破坏封闭原则，因为后者声称专门针对 [a⋅v]:B 的知识。因此，在观察到红色外观后，我确实知道 B，但这个知识与 1 无关，这仍然是信念而不是知识。论证逻辑形式化公平地代表了情况。

跟踪理由以传统认知模态工具无法捕获的方式表示红谷仓示例的结构。论证逻辑形式化对这种情况下似乎发生的情况进行了建模；即使“谷仓”在感知上并不可知，逻辑蕴涵下的知识封闭仍然得以维持。[2]

1.2 数理逻辑传统

根据布劳威尔的说法，构造性（直觉主义）数学中的真理意味着证明的存在，参见。 （Troelstra 和 van Dalen 1988）。 1931-34 年，Heyting 和 Kolmogorov 对直觉逻辑的基于证明的语义进行了非正式描述（Kolmogorov 1932，Heyting 1934），现在被称为 Brouwer-Heyting-Kolmogorov (BHK) 语义。根据 BHK 条件，如果公式有证明，则该公式为“真”。此外，复合语句的证明通过以下方式连接到其组件的证明：

A∧B 的证明由命题 A 的证明和命题 B 的证明组成；

A∨B 的证明通过给出 A 的证明或 B 的证明来给出；

A→B 的证明是将 A 的证明转换为 B 的证明的构造；

falsehood ⊥ 是一个没有证明的命题， ØA 是 A→⊥ 的简写。

柯尔莫哥洛夫明确表示，他的解释中的类似证明的对象（“问题解决方案”）来自经典数学（Kolmogorov 1932）。事实上，从基础的角度来看，将上述“证明”理解为这些条件应该指定的直觉系统中的证明并没有多大意义。

BHK 语义的基本价值在于，它非正式但明确地建议将论证（这里是数学证明）视为具有运算的对象。

在（Gödel 1933）中，哥德尔迈出了为直觉主义开发严格的基于证明的语义的第一步。哥德尔认为经典模态逻辑 S4 是描述可证明性属性的微积分：

经典命题逻辑的公理和规则；

◻(F→G)→(◻F→◻G);

◻F→F；

◻F→◻◻F;

必然性规则：如果⊢F，则⊢◻F。

基于布劳威尔对逻辑真值可证明性的理解，哥德尔定义了直觉语言中的命题公式 F 到经典模态逻辑语言的翻译 tr(F)：tr(F) 是通过在 F 的每个子公式前加上可证明性来得到的。方式◻。通俗地说，当确定公式的经典真值的通常过程应用于 tr(F) 时，它将测试 F 的每个子公式的可证明性（而不是真值），这与 Brouwer 的想法一致。根据哥德尔的结果和麦肯锡-塔斯基关于模态逻辑拓扑语义的工作，可以得出结论，翻译 tr(F) 提供了将直觉命题微积分 (IPC) 正确嵌入到 S4 中，即将直觉逻辑嵌入到经典逻辑中由可证明性算子扩展。

如果IPC证明了F，那么S4就证明了tr(F)。

尽管如此，哥德尔最初用经典可证明性来定义直觉逻辑的目标并未实现，因为 S4 与可证明性的通常数学概念的联系尚未建立。此外，哥德尔指出，将模态 ◻F 解释为 F 的直接想法在给定的形式系统 T 中是可证明的，这与哥德尔的第二个不完备性定理相矛盾。事实上，◻(◻F→F)可以在S4中通过必然性规则从公理◻F→F导出。另一方面，将模态◻解释为理论T和F中形式可证明性的谓词作为矛盾，将该公式转换为错误的陈述，即T的一致性在T中是内部可证明的。

(Gödel 1933)之后的情况可以用下图来描述，其中“X↪Y”应该被理解为“X被解释为Y”

IPC↪S4↪?↪经典证明

1938 年在维也纳的一次公开演讲中，哥德尔观察到，使用显式证明的格式：

t是F的证明。

可以帮助解释他的可证明性演算 S4 (Gödel 1938)。不幸的是，哥德尔的著作（Gödel 1938）直到 1995 年才出版，到那时，显式证明的哥德尔逻辑已经被重新发现，并公理化为证明逻辑 LP，并提供了将其与 S4 和经典证明连接起来的完备性定理（Artemov） 1995）。

证明逻辑 LP 成为论证逻辑家族中的第一个。 LP 中的证明术语只不过是被理解为经典证明的 BHK 术语。借助 LP，命题直觉逻辑获得了所需的严格 BHK 语义：

IPC↪S4↪LP↪经典证明

有关数理逻辑传统的进一步讨论，请参阅补充文件“更多技术问题”的第 1 节。

1.3 超内涵性

高内涵悖论由 Cresswell 于 1975 年提出。

众所周知，似乎有可能出现这样一种情况：有两个命题 p 和 q，它们在逻辑上是等价的，但人们可能相信其中一个而不相信另一个。如果我们将一个命题视为一组可能世界，那么两个逻辑上等价的命题将是相同的，因此如果“x相信”是一个真正的句子函子，那么开头句中描述的情况就不会出现。我称之为高内涵语境的悖论。超内涵语境就是不尊重逻辑对等的语境。

从克雷斯韦尔本人开始，已经提出了几种处理这个问题的方法。一般来说，这些涉及向熟悉的可能世界方法添加更多层，以便可以使用某种方式区分逻辑上等效的句子。克雷斯韦尔建议考虑句子的句法形式。实际上，论证逻辑通过其处理句子论证的机制考虑了句子形式。因此，论证逻辑解决了超内涵性的一些核心问题，作为奖励，我们自动拥有适当的证明理论、模型理论、复杂性估计和广泛的应用。

高内涵语境的一个很好的例子是数学家相互交谈时使用的非正式语言。通常，当数学家说他或她知道某事时，他们的理解是证明即将到来。但如下所示，这种知识本质上是超内涵的。

费马大定理 FLT 在逻辑上等价于 0=0，因为两者都是可证明的，因此表示相同的命题。然而，证明的上下文立即区分了它们：0=0 的证明 t 不一定是 FLT 的证明，反之亦然。

为了形式化数学语言，论证逻辑 LP 是一个自然的选择，因为 t:X 被设计为具有“t 是 X 的证明”的特征。

命题 X 和 Y 在 LP 中等价，X↔Y，这一事实并不能保证相应的论证断言的等价性，并且通常 t:X 和 t:Y 是不等价的，t:X↮t:Y。

进一步来说，LP 和一般的论证逻辑不仅足够细化以区分逻辑上等效句子的论证断言，而且还提供了一种灵活的机制来连接等效句子的论证，从而维护质量逻辑系统所需的构造性闭包属性。例如，令 X 和 Y 可证明等价，即存在 X↔Y 的证明 u，因此 u:(X↔Y) 在 LP 中是可证明的。还假设 v 是 X 的证明，因此 v:X。已经提到过，这并不意味着 v 是 Y 的证明——这是一个超内涵语境。然而，在正当性逻辑的框架内，基于 X 和 X↔Y 的证明，我们可以构造一个证明项 f(u,v) 来表示 Y 的证明，因此 f(u,v):Y 是可证明的。在这方面，论证逻辑超出了克雷斯韦尔的预期：逻辑上等效的句子表现出不同但建设性控制的认知行为。

2. 论证逻辑的基本组成部分

本节介绍最常见的论证逻辑系统的语法和公理化。

2.1 证明逻辑的语言

为了建立正当理由逻辑的正式解释，我们必须做出一个基本的结构假设：正当理由是具有结构和操作的抽象对象。形式证明提供了一个很好的论证例子，它长期以来一直是数理逻辑和计算机科学的研究对象（参见第 1.2 节）。

论证逻辑是一种形式逻辑框架，其中包含认知断言 t:F，代表“t 是 F 的论证”。论证逻辑并不直接分析 t 证明 F 超出格式 t:F 的含义，而是尝试以公理方式描述此关系。这类似于布尔逻辑处理其连接词（例如析取）的方式：它不分析公式 p∨q，而是假设有关该公式的某些逻辑公理和真值表。

做出了几个设计决策。论证逻辑从最简单的基础开始：经典布尔逻辑，并且有充分的理由。即使在最简单的层面上，理由也构成了足够严峻的挑战。 Russell、Goldman-Kripke、Gettier 等人的典型例子可以用布尔论证逻辑来处理。认知逻辑的核心由具有经典布尔基础的模态系统（K、T、K4、S4、K45、KD45、S5等）组成，并且每个模态系统都提供了相应的基于布尔逻辑的论证逻辑同伴。最后，并不总是假定理由的真实性。这使得捕捉认识论中涉及信仰而非知识问题的讨论的本质成为可能。

理由的基本操作是应用。应用运算采用理由 s 和 t 并生成理由 s⋅t，这样如果 s:(F→G) 和 t:F，则 [s⋅t]:G。象征性地，

s:(F→G)→(t:F→[s⋅t]:G)

这是组合逻辑和 λ 演算（Troelstra 和 Schwichtenberg 1996）、Brouwer-Heyting-Kolmogorov 语义（Troelstra 和 van Dalen 1988）、Kleene 可实现性（Kleene 1945）、证明逻辑 LP 等中假设的证明的基本属性。 。

论证的另一个常见操作是求和：引入它是为了明确模态逻辑推理（Artemov 1995）。然而，一些有意义的论证逻辑，如 J− (Artemov and Fitting 2019) 或 JNoC− (Faroldi, Ghari, Lehmann, and Studer 2024) 不使用运算和。通过总和，任何两个理由都可以安全地组合成范围更广的东西。如果 s:F，那么无论证据 t 是什么，组合证据 s + t 仍然是 F 的证明。更正确地，操作“+”采用证明 s 和 t 并产生 s + t，这是所有证明的证明按 s 或按 t。

s:F→[s+t]:F 和 t:F→[s+t]:F

作为动机，人们可能会认为 s 和 t 是一本百科全书的两卷，而 s + t 是这两卷的集合。想象一下其中一卷，比如 s，包含了命题 F 的充分理由，即 s:F 就是这种情况。那么较大的集合 s + t 也包含 F 的充分理由，[s + t]:F。在 LP 证明逻辑第 1.2 节中，“s+t”可以解释为证​​明 s 和 t 的串联。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。