证证逻辑（三）

3.2 弱完备性和强完备性

如果公式 X 在该模型的所有可能世界中都为真，则该公式在特定 JCS 模型中有效。JCS 的公理化已在第 2.2 节和第 2.3 节中给出。完备性定理现在具有预期的形式。

定理 2：当且仅当 X 在所有 JCS 模型中都有效时，公式 X 在 JCS 中可证明。

如上所述，完备性定理有时被称为弱完备性。令人惊讶的是，它的证明比模态逻辑 K 的完备性证明要容易得多。关于这一点的评论如下。另一方面，它非常通用，适用于所有常数规范。

在 (Fitting 2005) 中，还引入了更强版本的语义。如果模型 M=⟨G,R,E,V⟩ 满足以下条件，则称其具有完全解释性。对于每个 Γ∈G，如果对于所有 Δ∈G 且 ΓRΔ ，M,Δ⊩X，则对于某个证明项 t，M,Γ⊩t:X。注意，对于所有 Δ∈G 且 ΓRΔ ，M,Δ⊩X 这个条件是 X 在 Hintikka/Kripke 意义上在 Γ 处可信的通常条件。因此，完全解释性实际上是指，如果一个公式在可能世界中是可信的，那么它就存在一个证明。

并非所有弱模型都满足完全解释性条件。满足的模型称为强模型。如果常数规范 CS 足够丰富，使得内化定理成立，那么对于满足 CS 的强模型，我们就具有完备性。事实上，从适当的意义上讲，强模型的完整性等同于能够证明内部化。强模型的完备性证明与使用模态逻辑 K 的规范模型的完备性证明非常相似。反过来，强模型可以用来给出实现定理的语义证明（参见第 4 节）。

3.3 单主体族

到目前为止，我们讨论了 K 的对应物 J 的一种证立逻辑的可能世界语义。现在，我们将范围扩大到涵盖其他常见模态逻辑的证立类似物。

只需将可达关系 R 的自反性添加到第 3.1 节中模型的条件中，即可获得 t:X→X 对每个 t 和 X 的有效性，从而获得 JT 的语义，JT 是模态逻辑 T（最弱的知识逻辑）的证立逻辑类似物。事实上，如果 M,Γ⊩t:X，则特别地，X 在每个可从 Γ 到达的状态下都为真。由于可达关系要求自反性，因此 M,Γ⊩X。弱完备性定理和强完备性定理可以使用与 J 情况相同的机制来证明，并且连接 JT 和 T 的实现定理的语义证明也是可行的。这同样适用于下文讨论的逻辑。

对于 K4 的证明类似物，在术语语言中添加了一个额外的一元运算符“!”，参见 2.5 节。回想一下，这个运算符将证明映射到证明，其思想是，如果 t 是 X 的证明，那么 !t 也应该是 t:X 的证明。从语义上讲，这为模型 M=⟨G,R,E,V⟩ 添加了如下条件。

首先，R 当然应该是传递的，但不一定是自反的。其次，需要对证据函数进行单调性条件：

如果 ΓRΔ 且 Γ∈E(t,X) 则 Δ∈E(t,X)

最后，还需要一个证据函数条件。

E（t，X）⊆E（！t，t:X)

这些条件共同蕴涵了 t:X→!t:t:X 的有效性，并产生了 J4（K4 的证立类似物）的语义，并通过实现定理将它们连接起来。添加反身性将产生一种逻辑，由于历史原因，它被称为 LP。

我们已经讨论了作为 LP 子逻辑的证立逻辑，对应于模态逻辑 S4 的子逻辑。超越 LP 的第一个例子是第 2.7 节中讨论的那些，涉及一个负自省算子“?”。包含此算子的证立逻辑模型添加了三个条件。首先，R 是对称的。其次，添加了一个后来被称为强证据的条件：对于所有 Γ∈E(t,X)，M,Γ⊩t:X。最后，对证据函数有一个条件：

¯

E(t,X)

⊆E(?t,¬t:X)

如果将此机制添加到J4的机制中，我们得到逻辑J45，它是K45的证明对应物。其公理健全性和完备性可以得到证明。类似地，相关逻辑JD45和JT45可以语义地表述。(Rubtsova 2006)中给出了一个考虑算子?的实现定理。

转向2.8节中介绍的Geach逻辑，也可以为J4.2指定一个语义模型。假设G=⟨G,R,E,V⟩是一个LP模型。我们添加以下要求：首先，框架必须收敛，就像S4.2一样。其次，与?一样，E必须是一个强证据函数。第三，E(f(t,u),¬t:X)∪E(g(t,u),¬u:¬X)=G。完备性和可靠性结果按通常方式得出。

类似地，该族中每个由Geach方案公理化的模态逻辑都有一个相应的证明，并具有拟合语义和一个将证明对应项与相应的模态逻辑连接起来的实现定理。具体而言，这告诉我们证明逻辑族是无限的，而且肯定比最初设想的要广泛得多。此外，一些以前未考虑过的、不属于这一家族的模态逻辑，也有相应的证明方法。所有这些后果的研究仍在进行中。

3.4 单一世界证明模型

单一世界证明模型的发展远早于我们一直在讨论的更一般的可能世界证明模型（Mkrtychev 1997）。今天，它们可以简单地被认为是恰好具有单一世界的可能世界证明模型。J 的完备性证明以及上面提到的其他证明逻辑可以很容易地修改，以建立单一世界证明模型的完备性，尽管这当然不是最初的论证。单一世界证明模型的完备性告诉我们，关于证明模型可能世界结构的信息可以通过可采纳证据函数完全编码，至少对于迄今为止讨论的逻辑而言是如此。 Mkrtychev 使用单一世界论证模型来建立 LP 的可判定性，其他人则将其作为基础性应用，用于设定论证逻辑的复杂性界限，以及展示信念论证逻辑的保守性结果 (Kuznets 2000, Kuznets 2008, Milnikel 2007, Milnikel 2009)。复杂性结果进一步被用于解决逻辑全知问题 (Artemov and Kuznets 2014)。

3.5 本体论透明语义

上文 3.1-3 中描述的论证逻辑的形式语义。4 在给定世界Γ处定义真值的方式与在意识模型中相同：t:F 在Γ处成立，当且仅当

F 在所有可从Γ到达的世界成立，并且

根据给定的证据函数，t是F的可采纳证据。

此外，还有一种不同的语义学，即所谓的模块化语义学，它致力于使论证的本体论地位更加透明。在模块化语义学中，命题获得通常的经典真值，而论证在句法上被解释为公式集。我们保留了命题公式Fm的经典解释∗，在单个世界的情况下，它可以简化为

∗:Fm↦ {0,1}

即，每个公式的真值均为0（假）或1（真），并满足通常的布尔条件：⊩A→B 当且仅当⊮A或⊩B，等等。主要问题是如何解释论证术语。对于公式 X 和 Y 的集合，我们定义

X⋅Y={F∣G→F∈X，且 G∈Y，其中 G 为某个 G}。

通俗地说，X⋅Y 是对 X 和 Y 的所有成员（按此顺序）应用一次肯定前件式的结果。证立项 Tm 被解释为公式集的子集：

∗:Tm↦2Fm

使得

(s⋅t)∗⊇s∗⋅t∗ 且 (s+t)∗⊇s∗∪t∗。

这些条件对应于基本证立逻辑 J；其他系统要求 ∗ 具有额外的闭包性质。需要注意的是，模块化模型中的命题在语义上被解释为真值，而证立在句法上被解释为公式集。这是一个主要的超内涵特征：模块化模型可以将不同的公式 F 和 G 视为相等，即 F∗=G∗，但仍然能够区分辩护断言 t:F 和 t:G，例如当 F∈t∗ 但 G∉t∗ 时，得出 ⊩t:F 和 ⊮t:G。在一般可能世界设定中，公式在经典意义上被解释为可能世界集合 W 的子集，

∗:Fm↦ 2W，

而论证项在句法上被解释为每个世界中的公式集

∗:W×Tm↦ 2Fm。

关于模块化模型，论证逻辑系统已在 (Artemov 2012; Kuznets and Studer 2012) 中得到论证，其可靠性和完备性已得到证明。

3.6 与意识模型的联系

逻辑全知问题是指在认识论逻辑中，所有重言式都是已知的，并且知识在结果之下是封闭的，这是不合理的。Fagin 和 Halpern (1988) 提出了一种避免此类问题的简单机制。在通常的 Kripke 模型结构中添加一个意识函数 A，该函数指示代理在每个世界中感知到的公式。然后，如果满足以下条件，则认为一个公式在可能世界 Γ 处已知：1) 该公式在所有可从 Γ 到达的世界中都为真（知识的克里普克条件）；2) 主体在 Γ 处知道该公式。意识函数可以作为阻止任意公式集知识的实用工具。然而，作为逻辑结构，意识模型由于缺乏自然的闭包性质，可能会表现出异常行为。例如，主体可以知道 A∧B，但既不知道 A 也不知道 B，因此两者都不知道。

可能世界论证逻辑模型使用类似于意识模型的强制定义：对于任何给定的论证 t，论证断言 t:F 在世界 Γ 处成立，当且仅当 1) F 在所有可从 Γ 到达的世界 Δ 处都成立；2) t 是 F 在 Γ 处的可采信证据，Γ∈E(t,F)。主要区别在于论证逻辑模型中论证运算以及可采信证据函数 E 的相应闭包条件。因此，它可以被视为意识模型的动态版本，其必要的闭包性质已明确。Sedlár (2013) 探讨了这一思想，他运用LP语言，将其视为多主体模态逻辑，并将辩护项视为主体（更确切地说，是主体的行为）。这表明，辩护逻辑模型以自然的方式吸收了意识、群体主体和动态等常见的认知主题。

4. 实现定理

证据断言t:F的自然模态认知对应物是◻F，对于某个x，读作x:F。这一观察引出了遗忘投影的概念，它将每次出现的t:F替换为◻F，从而将辩护逻辑句子S转换为相应的模态逻辑句子So。遗忘投影以自然的方式从句子扩展到逻辑。

显然，不同的证立逻辑句子可能具有相同的遗忘投影，因此 So 会丢失 S 中包含的某些信息。然而，很容易观察到，遗忘投影总是将证立逻辑的有效公式（例如，J 的公理）映射到相应的认知逻辑（在本例中为 K）的有效公式。反之亦然：任何认知逻辑的有效公式都是某个证立逻辑有效公式的遗忘投影。这由对应定理 3 得出。

定理 3：Jo=K。

这种对应关系也适用于其他证立逻辑和认知系统对，例如 J4 和 K4，或 LP 和 S4，以及许多其他系统。对应定理以这种扩展形式表明，主要的模态逻辑，例如 K、T、K4、S4、K45、S5 以及其他一些系统，都有与之精确对应的证立逻辑。

对应定理的核心是以下实现定理。定理4：存在一个算法，对于每个可在K中导出的模态公式F，将证据项分配给F中每个模态性的出现，使得所得公式Fr可在J中导出。此外，该实现将证据变量分配给F中模态算子的否定出现，从而尊重认知模态性的存在性解读。

已知的恢复模态定理中证据项的实现算法在相应的模态逻辑中使用无截断推导。或者，实现定理可以通过Fitting方法或其适当修改在语义上建立。原则上，这些语义论证也产生了基于穷举搜索的实现程序。

得出任何模态逻辑都有一个合理的论证逻辑对应物的结论是错误的。例如，形式可证性逻辑 GL (Boolos 1993) 包含 Löb 原理：

◻(◻F→F)→◻F，

该原理似乎没有一个在认识论上可接受的明确版本。例如，考虑 F 为命题常数 ⊥ 的情况，表示为假。如果定理 4 的类似物涵盖 Löb 原理，则存在证立项 s 和 t，使得 x:(s:⊥→⊥)→t:⊥。但这在事实证立中直观地为假。事实上，s:⊥→⊥ 是事实公理的一个实例。应用公理内化，可得到常数 c 为 c:(s:⊥→⊥)。c 的选择使得 c:(s:⊥→⊥)→t:⊥ 的前件直观地为真，而结论为假[4]。尤其是，Löb原理 (5) 对于证明诠释无效（参见 (Goris 2007) 中关于哪些GL原理可实现的完整说明）。

对应定理为认识模态逻辑提供了新的见解。最值得注意的是，它为主流模态逻辑提供了一种新的语义。除了传统的克里普克式“普遍”解读◻F（即F在所有可能情况下都成立）之外，现在◻F有了严格的“存在性”语义，可以理解为F存在一个见证（证明、辩护）。

辩护语义在模态逻辑中的作用类似于克莱恩可实现性在直觉主义逻辑中的作用。在这两种情况下，预期的语义都是存在性的：直觉主义逻辑的布劳威尔-海廷-柯尔莫哥洛夫诠释（Heyting 1934，Troelstra and van Dalen 1988，van Dalen 1986）和哥德尔对S4的可证明性解读（Gödel 1933，Gödel 1938）。在这两种情况下，都存在一种具有普遍特征的可能世界语义，这是一种非常有力且占主导地位的技术工具。然而，它并未探讨预期语义的存在性特征。克莱恩可实现性（Kleene 1945，Troelstra 1998）揭示了直觉逻辑和证明逻辑的计算语义，从而为直觉逻辑和模态逻辑提供了精确的BHK证明语义。

在认识论语境中，证立逻辑和对应定理为知识和信念的模态逻辑添加了一个新的“证立”成分。同样，这个新的成分实际上是一个古老而核心的概念，已被主流认识论者广泛讨论，但仍超出了经典认识论逻辑的范围。对应定理告诉我们，证立与Hintikka风格的系统兼容，因此可以安全地纳入认识模态逻辑的基础。

有关实现定理的更多信息，请参阅补充文件《更多技术问题》的第4节。

5.概括

到目前为止，本文仅考虑了单主体证立逻辑，类似于单主体知识逻辑。证立逻辑可以被认为是显性知识逻辑，与更传统的隐性知识逻辑相关。除了上述讨论的系统之外，文献中还研究了许多系统，这些系统涉及多个主体，或同时包含隐性和显性运算符，或两者兼具。

5.1 显性知识与隐性知识的混合

由于证立逻辑提供显性证立，而传统知识逻辑提供隐性知识运算符，因此很自然地会考虑将两者结合在一个系统中。最常见的显性知识和隐性知识的联合逻辑是 S4LP (Artemov and Nogina 2005)。S4LP 的语言与 LP 类似，但增加了一个隐性知识运算符，写作 K 或 ◻ 。其公理体系类似于LP的公理体系，结合了隐式算子的S4公理体系，并加上一个连接公理：t:X→◻X，任何具有明确论证的事物都是可知的。

从语义上讲，LP的可能世界论证模型无需修改，因为它们已经具备了Hintikka/Kripke模型的所有机制。一种是按照通常的方式建模◻算子，仅使用可及性关系；另一种是按照3.1节中描述的方式建模论证项，同时使用可及性和证据函数。由于◻X在世界中为真的通常条件是t:X为真的条件的两个子句之一，因此这立即得出t:X→◻X的有效性，并且可靠性也很容易得到。公理完备性也相当简单。

在S4LP中，隐式和显式知识都表示为：但在可能世界论证模型语义中，单一可达性关系适用于两者。这并非唯一的实现方式。更一般地说，显性知识可达性关系可以是隐性知识可达性关系的恰当扩展。这体现了显性知识对于已知事物的标准比隐性知识更严格的观点。当这些认知概念遵循不同的逻辑规律时，对显性知识和隐性知识使用不同的可达性关系就变得必要了，例如，隐性知识遵循S5规律，而显性知识遵循LP规律。多重可达性关系的情况在文献中通常被称为Artemov-Fitting模型，但本文将称之为多智能体可能世界模型。（参见5.2节）。

奇怪的是，虽然S4LP逻辑看起来很自然，但实现定理对它来说却存在问题：如果坚持所谓的正常实现（Kuznets 2010），则无法证明这样的定理。通过尊重认知结构的显性论证来实现S4LP中的隐性知识模态仍然是该领域的一个重大挑战。

隐性知识和显性知识之间的相互作用有时可能相当微妙。例如，考虑以下负自省的混合原理（再次强调，◻应理解为一个隐性认知算子）：

¬t:X→◻¬t:X。

从可证明性的角度来看，这是负自省的正确形式。事实上，设◻F被解释为F是可证明的，t:F被解释为t是给定形式理论T中F的证明，例如在皮亚诺算术PA中。则(6)陈述了一个可证明的原理。事实上，如果t不是F的证明，那么由于该陈述是可判定的，它可以在T内部成立，因此在T中这个句子是可证明的。另一方面，“t不是F的证明”的证明p同时依赖于t和F，p=p(t,F)，并且不能仅根据t计算得出。因此，◻不能被任何仅依赖于t的特定证明项所取代，并且(6)不能以完全显式的证明式格式呈现。

显性/隐性知识系统的第一个例子出现在可证性逻辑领域。在(Sidon 1997, Yavorskaya (Sidon) 2001)中，引入了一种逻辑LPP，它将可证性逻辑GL与证明逻辑LP相结合，但为了确保生成的系统具有理想的逻辑特性，添加了一些来自GL和LP原始语言之外的额外操作。在(Nogina 2006, Nogina 2007)中，提出了一个用于证明和可证性的完整逻辑系统GLA，它是GL和LP原始语言的综合。 LPP 和 GLA 相对于算术模型类以及可能世界论证模型类而言都具有完备性。

另一个无法完全明确表达的可证性原理示例是 Löb 原理 (5)。对于 LPP 和 GLA 中的每一个，很容易找到一个证明项 l(x) 使得

x:(◻F→F)→l(x):F

成立。然而，没有任何实现能够使 (5) 中所有三个 ◻ 都明确。事实上，可实现的可证性原理集是 GL 和 S4 的交集 (Goris 2007)。

5.2 多智能体可能世界论证模型

在多智能体可能世界论证模型中，采用了多种可达性关系，它们之间存在连接 (Artemov 2006)。其思想是，存在多个智能体，每个智能体都具有一个隐式知识算子，并且存在每个智能体都能理解的论证项。粗略地讲，每个人都能理解明确的理由；这些理由相当于基于证据的常识。

一个包含 n 个代理的可能世界论证模型是一个满足以下条件的结构 ⟨G,R1, …,Rn,R,E,V⟩。G 是一个可能世界集合。R1,…,Rn 中的每一个都是一个可达性关系，每个代理对应一个。这些关系可以根据需要假设为自反性、传递性或对称性。它们用于为代理家族建模隐式代理知识。可达性关系 R 满足 LP 条件，即自反性和传递性。它用于显式知识的建模。E 是一个证据函数，满足与第 3.3 节中 LP 条件相同的条件。V 像往常一样将命题字母映射到世界集合。有一个特殊条件：对于每个 i = 1，…，n，Ri⊆R。