证证逻辑（一）
你可能会说：“我知道亚伯拉罕·林肯个子高。” 反过来，你可能会被问到你是如何知道的。你几乎肯定不会像 Hintikka 那样，从语义上回答说，亚伯拉罕·林肯在所有与你的知识相符的情境下都很高。相反，你更有可能说：“我在几本书中读到过亚伯拉罕·林肯的身高，也见过他和其他人在一起的照片。” 人们通过提供理由，即证证来证明知识。Hintikka 语义学将知识视为真信念。证证逻辑弥补了柏拉图将知识描述为已证证的真信念所缺失的第三个要素。
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 教学逻辑及其他
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 认识论传统
至少自冯·赖特和欣蒂卡（Hintikka，1962；冯·赖特，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 的典型红谷仓例子中加以利用；以下是该故事的简化版本，摘自 (Dretske 2005)。
假设我开车经过一个街区，在我不知情的情况下，纸糊的谷仓散落各处，我看到我面前的物体是一个谷仓。因为我有“谷仓在我面前”的感知，所以我相信我面前的物体是一个谷仓。我们的直觉告诉我，我不知道谷仓是什么。但现在假设附近没有假的红色谷仓，而且我也注意到我面前的物体是红色的，所以我知道那里有一个红色的谷仓。这种并置，我知道有一个红色谷仓，就意味着那里有一个我不知道的谷仓，这“令人尴尬”。
在红色谷仓示例的第一次形式化中，将使用基本模态逻辑进行逻辑推导，其中◻被解释为“信念”模态。然后，根据问题的描述，某些◻的出现将被外部解释为“知识”。令 B 为句子“我面前的物体是谷仓”，令 R 为句子“我面前的物体是红色的”。
◻B，“我相信我面前的物体是谷仓”；
◻(B∧R)，“我相信我面前的物体是红色的谷仓”。
在元层面上，2 实际上是知识，而根据问题描述，1 不是知识。
◻(B∧R→B)，逻辑公理的知识断言。
在这个形式化中，模态形式 (2) 的认知闭包似乎被违反了：第 2 行◻(B∧R) 和第 3 行◻(B∧R→B) 是知识的情况，而◻B（第 1 行）不是知识。这里的模态语言似乎无助于解决这个问题。
接下来考虑证成逻辑中的红谷仓示例，其中 t:F 被解释为“我相信 F，理由是 t”。设 u 为对信念 B 的具体个体证成，v 为对信念 B∧R 的具体个体证成。此外，设 a 为逻辑真值 B∧R→B 的证成。则假设列表如下：
u:B“u 是相信我面前的物体是谷仓的理由”；
v:(B∧R)，“v 是相信我面前的物体是红色谷仓的理由”；
a:(B∧R→B)。
在元层面上，问题描述指出 2 和 3 是知识，而非信念，而 1 是信念，但并非知识。形式推理如下：
根据原理 (1)，a:(B∧R→B)→(v:(B∧R)→[a⋅v]:B)；
根据命题逻辑，由 3 和 4 可知 v:(B∧R)→[a⋅v]:B；
根据命题逻辑，由 2 和 5 可知 [a⋅v]:B。
注意，结论 6 是 [a⋅v]:B，而不是 u:B；认知闭包成立。通过论证逻辑推理，可以得出结论：[a⋅v]:B 是知识的集合，即“我因为原因 a⋅v 知道 B”。u:B 不是知识集合这一事实并不破坏闭合原则，因为后者明确地声称对 [a⋅v]:B 有知识。因此，在观察到红色外观之后，我确实知道 B，但这种知识与 1 无关，后者仍然是信念集合而非知识集合。论证逻辑形式化清晰地描述了这种情况。
追踪论证以一种传统认知模态工具无法捕捉的方式表征了红色谷仓示例的结构。论证逻辑形式化模拟了在这种情况下似乎正在发生的事情；即使“谷仓”在感知上不为人所知，在逻辑蕴涵下知识的闭合性仍然得以维持。[2]
1.2 数理逻辑传统
根据布劳威尔的观点，在构造性（直觉主义）数学中，真意味着存在一个证明，参见（Troelstra and van Dalen 1988）。1931-1934年，海廷和柯尔莫哥洛夫对直觉主义逻辑中基于证明的语义进行了非正式描述（Kolmogorov 1932，Heyting 1934），现在被称为布劳威尔-海廷-柯尔莫哥洛夫（BHK）语义。根据BHK条件，如果一个公式有证明，则它为“真”。此外，复合语句的证明与其组成部分的证明以如下方式关联：
A∧B的证明由命题A的证明和命题B的证明组成；
A∨B的证明可以通过给出A的证明或B的证明来给出；
A→B的证明是将A的证明转化为B的证明的构造；
假⊥是没有证明的命题，¬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中每个子公式的可证明性（而非真值），这与布劳威尔的思想一致。根据哥德尔的研究结果以及麦肯锡-塔斯基关于模态逻辑拓扑语义的研究，可以得出，翻译tr(F)提供了直觉主义命题演算IPC在S4中的恰当嵌入，即将直觉主义逻辑嵌入到由可证明性算子扩展的经典逻辑中。
如果IPC证明了F，则S4证明了tr(F)。
然而，哥德尔最初用经典可证明性来定义直觉主义逻辑的目标并未实现，因为S4与通常的数学可证明性概念的联系尚未建立。此外，哥德尔指出，在给定形式系统 T 中，将模态 ◻F 解释为 F 的直接想法与哥德尔第二不完备定理相矛盾。事实上，◻(◻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.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 是可证的。在这方面，证立逻辑超越了 Cresswell 的预期：逻辑上等价的句子表现出不同但受构造性控制的认知行为。
2. 证立逻辑的基本组成部分
本节介绍最常见证立逻辑系统的语法和公理。
2.1 证立逻辑的语言
为了建立证立逻辑的形式化描述，必须做出一个基本的结构性假设：证立是具有结构和操作的抽象对象。形式化证明是证立的一个很好的例子，形式化证明长期以来一直是数理逻辑和计算机科学的研究对象（参见 1.2 节）。
证立逻辑是一个形式逻辑框架，它包含认知断言 t:F，代表“t 是 F 的证立”。证立逻辑并不直接分析t在t:F格式之外证立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 和 Fitting，2019）或 JNoC−（Faroldi、Ghari、Lehmann 和 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 的串联。
