证证逻辑（完结）

如果 M=⟨G,R1, …,Rn,R,E,V⟩ 是一个多主体可能世界论证模型，那么一个世界真值关系 M,Γ⊩X 的定义包含大多数常用子句。其中特别值得关注的是：

M,Γ⊩KiX 当且仅当，对于每个 Δ∈G 且 ΓRiΔ，我们有 M,Δ⊩X。

M,Γ⊩t:X 当且仅当 Γ∈E(t,X)，并且对于每个 Δ∈G 且 ΓRΔ，我们有 M,Δ⊩X。

条件 Ri⊆R 意味着对于每个主体 i，t:X→KiX 的有效性。如果只有一个主体，并且该主体的可达性关系是自反且传递的，这为 S4LP 提供了另一种语义。无论主体数量多少，每个主体都接受显式理由作为知识的建立。

Yavorskaya (Sidon) 2008 提出并研究了包含两个智能体的 LP 版本，但它可以推广到任意有限数量的智能体。在这种情况下，每个智能体都有自己的一组调整运算符、变量和常量，而不是像上面那样为每个人设置一组。此外，还可以允许代理之间进行一些有限的通信，使用一个允许一个代理验证另一个代理证明正确性的新算子。单世界和更通用的可能世界证明语义的版本都已为双代理逻辑创建。这涉及证据函数概念的直接扩展，并且对于可能世界证明模型，使用两个可达性关系。实现定理已得到句法证明，但语义证明可能也行得通。

具有显性和隐性知识的多代理模型（其中每个代理都有自己的一组证明算子）可用于对零知识证明进行认识论分析（Lehnherr、Ognjanovic 和 Studer，2022）。零知识证明是一种协议，通过该协议，一个代理（证明者）可以向另一个代理（验证者）证明证明者拥有某些知识（例如，知道密码），而无需透露任何超出拥有知识这一事实的信息（例如，无需透露密码）。以下公式可用于描述协议执行后的情况，其中项 s 证明了验证者通过协议获得的知识：

s:VKPF，

表示协议向验证者 V 提供证明 s，证明证明者 P 知道 F；以及

¬s:Vt:PF，对于任何项 t，

即，对于任何项 t，协议都无法证明验证者能够知道 t 能够证明证明者知道 F。也就是说，协议证明了证明者知道 F，但并未证明任何可能的证据来证明该知识。

已经有一些关于公共公告在多智能体论证逻辑中的作用的探索（Renne 2008，Renne 2009）。补充文件《更多技术问题》第5节中对基于证据的共同知识的概念进行了更详细的阐述。

除了多智能体认知逻辑之外，还有其他一些论证逻辑，它们具有两种类型的项。Kuznets、Marin 和 Strassburger (2021) 提出了一种显式的构造模态逻辑。在该逻辑中，◻-模态性通过类似LP中的证明项来实现。为了实现◊-模态性，引入了第二种项，称为见证项。在构造模态逻辑中，公式◊F表示F是一致的。在其实现s:F中，见证项s表示公式F的抽象见证模型。

另一个例子是二元道义逻辑（DDL），它可以由两种模态◻和◯公理化。公式◻F表示F已确定为真，条件◯(F/G)表示F在G给定的情况下是必然的。Faroldi、Rohani和Studer (2023)考虑了DDL的一个显式版本。同样，◻F通过像LP中的证明项来实现，而◯(F/G)则是通过使用一种表示道义理由的新类型的项来实现的。

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

有一种使用证立逻辑来分析同一事实的不同证立的技巧，尤其是在某些证立是事实性而某些不是的情况下。为了演示该技巧，请考虑一个著名的例子：

如果一个人相信已故首相的姓氏以“B”开头，那么他相信的是真的，因为已故首相是亨利·坎贝尔·班纳曼爵士[5]。但如果他相信贝尔福先生是已故首相[6]，他仍然会相信已故首相的姓氏以“B”开头，然而，这种信念虽然正确，但不会被认为构成知识。（Russell 1912）

正如第 1.1 节讨论的“红谷仓”例子一样，这里我们必须处理对一个真实陈述的两个论证，其中一个是正确的，另一个则不正确。设B是一个句子（命题原子），w是B的错误理由的指定证立变量，r是B的正确（因此是事实的）理由的指定证立变量。那么，罗素的例子引出了以下一组假设[7]：

R={w:B,r:B,r:B→B}

与直觉有些相反，我们可以从R逻辑上推导出w的事实性：

r:B（假设）

r:B→B（假设）

B（根据肯定前件推理，由1和2推导出）

B→(w:B→B)（命题公理）

w:B→B（根据肯定前件推理，由3和4推导出）

然而，这一推导利用了r是B的事实性证立这一事实，从而得出w:B→B，这构成了w:B的“诱导事实性”的情形。问题是，如何区分 r:B 的“真实”事实性与 w:B 的“诱导事实性”？这里需要某种证据追踪，而证成逻辑是一个合适的工具。自然的方法是考虑不包含 r:B 的假设集，即

S={w:B,r:B→B}

并确定 w 的事实性，即 w:B→B 不能从 S 推导出来。这里有一个可能世界证成模型 M = (G,R,E,V)，其中 S 成立，但 w:B→B 不成立：

G={1}，

R=∅ ，

V(B) = ∅（因此 not-1⊩B），

对于除 (r,B) 之外的所有 (t,F) 对，E(t,F) = {1}，并且

E(r,B) = ∅ 。

很容易看出，E 上的 Application 和 Sum 闭包条件成立。在 1 处，w:B 成立，即：

1⊩w:B

因为 w 是 B 在 1 处的可采纳证据，并且不存在从 1 可到达的可能世界。此外，

非-1⊩r:B

因为根据 E，r 在 1 处不是 B 的可采纳证据。因此：

1⊩r:B→B

另一方面，

非-1⊩w:B→B

因为 B 在 1 处不成立。

7.论证的自指性

实现算法有时会生成包含自指论证断言 c:A(c) 的常量规范，即论证（此处为 c）出现在所断言命题（此处为 A(c)）中的断言。

论证的自指性是一种新现象，在传统的模态语言中并不存在。除了作为有趣的认识论对象之外，这种自指断言由于其内在的恶性循环，从语义学的角度来看也提出了特殊的挑战。事实上，要评估 c，人们通常期望先评估 A，然后将 A 的论证对象赋值给 c。然而，由于 A 包含尚未评估的 c，这无法实现。模态逻辑是否可以在不使用自指论证的情况下实现，一直是该领域一个重要的悬而未决的问题。

Kuznets 在 Brezhnev and Kuznets 2006 中的主要成果指出，在 LP 中 S4 的实现中，证明的自指性是不可避免的。Kuznets 的以下定理给出了当前的状态：

定理 5：在模态逻辑 K 和 D 的实现中可以避免自指性。在模态逻辑 T、K4、D4 和 S4 的实现中，自指性无法避免。

该定理确立了 S4 的证明项系统必然是自指性的。这给可证性语义带来了一个严重的、尽管并非直接可见的限制。在哥德尔算术证明的语境中，这个问题可以通过一种通用方法来处理，即将算术语义分配给自指断言 c:A(c)，声明 c 是 A(c) 的证明。在《证明逻辑》LP中，它通过一个非平凡的不动点构造来处理。

自指性为摩尔悖论提供了一个有趣的视角。详情请参阅补充文件《更多技术问题》第6节。

余俊华（Yu 2014）解答了直觉逻辑IPC的BHK语义的自指性问题。他扩展了库兹涅茨的方法，建立了

定理6：直觉主义双重否定律¬¬(¬¬p→p)的每个LP实现都需要自指常数规范。

更一般地，余俊华证明了，任何经典重言式的双重否定（根据格利文科定理，它们都是IPC的定理）在LC中的实现都需要自指常数规范。 Yu在IPC的纯蕴涵片段中发现了另一个不可避免的自指称性的例子。这表明直觉逻辑的BHK语义（即使仅仅是直觉蕴涵）本质上是自指称的，需要不动点构造才能将其与PA或类似系统中的形式化证明联系起来。这或许可以部分解释为什么任何试图以不带自指称性的直接归纳方式构建可证明性BHK语义的尝试注定会失败。

8. 论证逻辑中的量词

虽然对命题论证逻辑的研究远未完成，但也有一些关于一阶版本的研究。模态逻辑的量化版本已经提供了超越标准一阶逻辑的复杂性。当涉及论证逻辑时，量化的运用范围更加广阔。经典的量化对象是“对象”，而模型则配备了量词所涵盖的域。从模态上来说，所有可能世界可能都有一个共同的域，或者每个世界可能都有各自的域。巴坎公式在这里的作用众所周知。定域和变域选项也适用于证明逻辑。此外，还有一种模态逻辑中没有类似物的可能性：可以对证明本身进行量化。

关于量化证明逻辑可能性的初步结果非常不利。证明逻辑LP的算术可证明性语义自然地推广到具有常规量词的一阶版本，以及具有证明量词的版本。在这两种情况下，公理化问题都得到了否定的回答。

定理7：证明逻辑不是递归可枚举的 (Artemov and Yavorskaya (Sidon) 2001)。量词覆盖证明的证明逻辑不可递归枚举 (Yavorsky 2001)。

尽管算术语义学不可能实现，但在 (Fitting 2008) 中，针对量词覆盖证明的 LP 版本，给出了可能世界语义学和公理证明理论。并证明了其可靠性和完备性。此时，可能世界语义学与算术语义学分道扬镳，这可能会或可能不会引起人们的警惕。此外，还证明了 S4 通过将 ◻Z 翻译为“存在一个证明 x 使得 x:Z∗”，嵌入到量化逻辑中，其中 Z∗ 是 Z 的翻译。虽然这种逻辑有些复杂，但它已经找到了应用，例如在 (Dean and Kurokawa 2009b) 中，它被用于分析“知者悖论”，尽管在 (Arlo-Costa and Kishida 2009) 中，有人对这种分析提出了异议。

一阶证明逻辑（FOLP），带有针对单个变量的量词，已在 Artemov 和 Yavorskaya (Sidon) (2011) 中提出。在 FOLP 证明中，断言用形式为 t:XA 的公式表示，其中 X 是单个变量的有限集，这些变量被视为开放可替换的全局参数。X 中所有在 A 中自由出现的变量在 t:XA 中也是自由的。A 的所有其他自由变量都被视为局部变量，因此在 t:XA 中是受约束的。例如，如果 A(x,y) 是原子公式，则在 p:{x}A(x,y) 中，变量 x 是自由的，变量 y 是受约束的。同样，在 p:{x,y}A(x,y) 中，两个变量都是自由的，而在 p:∅A(x,y) 中，x 和 y 都不是自由的。

证明（论证）用不包含单个变量的证明项表示。除了 LP 运算之外，还有一系列针对证明项的运算，即 genx(t)，对应于对单个变量 x 的泛化。支配此运算的新公理是 t:XA→gen:x(t)X∀xA，其中 x∉X。完整的 FOLP 原理列表以及一阶 S4 的实现可在 Artemov 和 Yavorskaya (Sidon) (2011) 中找到。FOLP 的语义已在 Fitting (2014a) 中开发。

9. 历史注释

最初的证明逻辑系统，即证明逻辑 LP，于 1995 年由 (Artemov 1995) 引入（另见 (Artemov 2001)），其中首次建立了诸如内化、实现和算术完备性等基本性质。LP 为哥德尔的可证明性逻辑 S4 提供了预期的可证明性语义，从而为直觉主义命题逻辑提供了 Brouwer-Heyting-Kolmogorov 语义的形式化。认知语义和完备性（Fitting，2005）是首次为LP建立的。LP的符号模型和可判定性则归功于Mkrtychev（Mkrtychev，1997）。复杂度估计最早出现在（Brezhnev and Kuznets，2006，Kuznets 2000, Milnikel 2007)。所有可判定性和复杂性结果的全面概述可在 (Kuznets 2008) 中找到。系统 J、J4 和 JT 最初是在 (Brezhnev 2001) 中以不同名称和略微不同的设置下考虑的。JT45 独立出现在 (Pacuit 2006) 和 (Rubtsova 2006) 中，JD45 出现在 (Pacuit 2006) 中。单一结论证明的逻辑已在 (Krupski 1997) 中发现。(Artemov 2006) 提出了一种基于已证实知识的更通用的常识方法。(Renne 2008, Renne 2009) 研究了带有证实的证实逻辑和动态认知逻辑的博弈语义。 (Artemov and Kuznets 2009, Artemov and Kuznets 2014, Wang 2009) 探讨了证立逻辑与逻辑全知问题之间的联系。(Artemov 2008) 引入了证立逻辑这一名称，其中对克里普克、罗素和盖梯尔的例子进行了形式化；这种形式化已被用于解决悖论、验证、隐藏假设分析和消除冗余。(Dean and Kurokawa 2009a) 则将证立逻辑用于分析知者悖论和可知性悖论。

关于证立逻辑的首两部专著于 2019 年出版 (Artemov and Fitting 2019, Kuznets and Studer 2019)。