理由逻辑（四）

5.1混合明确和隐性知识

由于理由逻辑提供了明确的理由，而传统的知识逻辑提供了一个隐式知识操作员，因此自然要考虑将两者结合在一个系统中。显式和隐式知识的最常见的联合逻辑是\ Mathsf {S4LP}（Artemov and Nogina 2005）。 \ mathsf {s4lp}的语言就像\ Mathsf {lp}的语言，但是添加了隐式知识操作员，编写了\ Mathbf {K}或\ box。 Axiomatics就像\ Mathsf {lp}一样，与隐式运算符的\ Mathsf {s4}结合使用，以及连接的axiom，t：x \ rightArrow \ box x，任何具有显式合理的事物都是可知的。

从语义上讲，\ mathsf {lp}可能的世界理由模型不需要修改，因为它们已经具有Hintikka/Kripke模型的所有机械。一个人以通常的方式对\ box运算符进行建模，仅利用可访问性关系，然后使用可访问性和证据功能进行第3.1节中所述的理由术语进行建模。由于\ box x在一个世界上的常规条件是t：x真实条件的两个条款之一，因此这立即产生t：x \ rightarrow \ box x的有效性，声音很容易跟随。公理的完整性也很简单。

在\ mathsf {s4lp}中，隐式和明确的知识都表示，但是在可能的世界合理模型语义中，单个可访问性关系都适合两者。这不是这样做的唯一方法。更一般而言，明确的知识可访问性关系可能是对隐性知识的适当扩展。这代表了显式知识的愿景，因为它比隐性知识具有更严格的标准。当这些认识论概念遵守不同的逻辑定律时，例如\ mathsf {s5}，使用不同的可访问性关系以进行显式和隐式知识，以实现隐式知识，而\ mathsf {lp}以进行显式。在文献中通常将多个可访问性关系的情况称为Artemov拟合模型，但在这里将被称为多代理可能的世界模型。 （参见第5.2节）。

奇怪的是，虽然逻辑\ Mathsf {S4LP}似乎很自然，但实现定理是有问题的：如果有人坚持认为所谓的正常实现，就无法证明这种定理（Kuznets 2010）。

通过尊重认知结构的明确论证来实现 \mathsf{S4LP} 中的隐含知识模式仍然是该领域的主要挑战。

隐性知识和显性知识之间的相互作用有时可能相当微妙。作为一个例子，考虑以下消极内省的混合原则（同样 \Box 应该被理解为隐式认知运算符），

\tag{6} \neg t : X \rightarrow \Box \neg t : X。

从可证明性的角度来看，这是消极内省的正确形式。事实上，让 \Box F 被解释为 F 是可证明的，并且 t : F 因为 t 是给定形式理论 T 中 F 的证明，例如，在皮亚诺算术 \mathsf{PA} 中。然后（6）陈述了一个可证明的原理。事实上，如果t不是F的证明，那么，由于这个陈述是可判定的，它可以在T内部成立，因此在T中这个句子是可证明的。另一方面，“t 的证明 p 不是 F 的证明”取决于 t 和 F 两者，p = p ( t , F) 并且不能仅在给定 t 的情况下进行计算。在这方面，\Box 不能被任何特定的仅依赖于 t 的证明项替换，并且 (6) 不能以完全明确的论证风格格式呈现。

显性/隐性知识系统的第一个例子出现在可证明性逻辑领域。在（Sidon 1997，Yavorskaya (Sidon) 2001）中，引入了逻辑 \mathsf{LPP}，它将可证明性逻辑 \mathsf{GL} 与证明逻辑 \mathsf{LP} 结合起来，但要确保所得系统具有理想的逻辑属性，添加了来自 \mathsf{GL} 和 \mathsf{LP} 原始语言之外的一些附加操作。在（Nogina 2006，Nogina 2007）中，以\mathsf{GL}和\mathsf{LP}的原始语言的总和，提供了用于证明和可证明性的完整逻辑系统\mathsf{GLA}。 \mathsf{LPP} 和 \mathsf{GLA} 都相对于算术模型类以及相对于可能的世界论证模型类而言享有完整性。

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

\tag{7} x :( \Box F \rightarrow F ) \rightarrow l ( x ): F

然而，没有实现使(5)中的所有三个\Box显式化。事实上，可实现的可证明性原理集是 \mathsf{GL} 和 \mathsf{S4} 的交集（Goris 2007）。

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

在多智能体可能的世界合理性模型中，采用了多种可达性关系以及它们之间的联系（Artemov 2006）。这个想法是，有多个代理，每个代理都有一个隐式知识运算符，并且有每个代理都理解的理由术语。粗略地说，每个人都明白明确的原因；这些相当于基于证据的常识。

n-agent 可能的世界论证模型是一个结构 \langle \mathcal{G} , \mathcal{R}_{1}, …,\mathcal{R}_{n} , \mathcal{R} , \mathcal{ E} , \mathcal{V}\rangle 满足以下条件。 \mathcal{G} 是一组可能的世界。每个 \mathcal{R}_{1},...,\mathcal{R}_{n} 都是一个可访问关系，每个代理一个。根据需要，可以假定这些是自反的、传递的或对称的。它们用于对代理家族的隐式代理知识进行建模。可及性关系 \mathcal{R} 满足 \mathsf{LP} 条件、自反性和传递性。它用于显性知识的建模。 \mathcal{E} 是一个证据函数，满足与 3.3 节中 \mathsf{LP} 相同的条件。像往常一样， \mathcal{V} 将命题字母映射到世界集。有一个特殊的条件：对于每个 i = 1, …,n ， \mathcal{R}_{i} \subseteq \mathcal{R}。

如果 \mathcal{M} = \langle \mathcal{G} , \mathcal{R}_{1} , …,\mathcal{R}_{n} , \mathcal{R} , \mathcal{E} , \ mathcal{V}\rangle 是一个多主体可能世界论证模型，一个世界真相关系 \mathcal{M} 、 \Gamma \Vdash X 定义为大多数常用条款。特别感兴趣的是：

\mathcal{M} , \Gamma \Vdash K_{i}X 当且仅当，对于每个 \Delta \in \mathcal{G} 和 \Gamma \mathcal{R}_{i} \Delta，我们有 \ mathcal{M} , \Delta \Vdash X.

\mathcal{M} , \Gamma \Vdash t : X 当且仅当 \Gamma \in \mathcal{E} ( t , X) 且对于每个 \Delta \in \mathcal{G} 且 \Gamma \mathcal{ R} \Delta，我们有 \mathcal{M} 、 \Delta \Vdash X。

对于每个代理 i，条件 \mathcal{R}_{i} \subseteq \mathcal{R} 需要 t : X \rightarrow K_{i}X 的有效性。如果只有一个代理，并且该代理的可访问关系是自反和传递的，这为 \mathsf{S4LP} 提供了另一种语义。无论代理的数量有多少，每个代理都接受明确的理由作为建立知识。

具有两个智能体的 \mathsf{LP} 版本在（Yavorskaya (Sidon) 2008）中被引入和研究，尽管它可以推广到任何有限数量的智能体。在这种情况下，每个代理都有自己的一组理由运算符、变量和常量，而不是如上所述为每个人都有一组。此外，可以允许代理之间进行一些有限的通信，使用新的运算符，允许一个代理验证另一代理的理由的正确性。为双智能体逻辑创建了单一世界和更一般的可能世界论证语义的版本。这涉及到证据函数概念的直接扩展，以及使用两种可达性关系的可能的世界论证模型。实现定理已经在句法上得到了证明，尽管语义证明可能也有效。

具有显式和隐式知识的多智能体模型（其中每个智能体都有自己的一组论证算子）可用于对零知识证明进行认知分析（Lehnherr、Ognjanovic 和 Studer 2022）。零知识证明是一种协议，通过该协议，一个代理（证明者）可以向另一个代理（验证者）证明证明者拥有一定的知识（例如，知道密码），而无需传达除拥有知识这一事实之外的任何信息（例如，不泄露密码）。下面的公式可以用来描述协议执行后的情况，其中项 s 证明了验证者从协议中获得的知识： s:_V K_P F，意味着协议向验证者 V 产生了一个证明 s证明者 P 知道 F；和 \lnot s:_V t:_P F \text{ 对于任何项 t,} 即，对于没有项 t，协议证明验证者可以知道 t 证明证明者对 F 的了解是合理的。也就是说，协议证明证明者知道 F，但它不能证明该知识的任何可能证据。

人们对公告在多主体论证逻辑中的作用进行了一些探索（Renne 2008，Renne 2009）。

补充文件“一些更多技术问题”的第 5 节中有更多关于基于证据的常识的概念。

除了多主体认知逻辑之外，还有其他具有两种类型术语的论证逻辑。 Kuznets、Marin 和 Strassburger (2021) 引入了构造模态逻辑的显式版本。在那里，\Box-modality 是通过 \mathsf{LP} 中的证明项来实现的。为了实现“钻石模态”，引入了第二种术语，称为见证人术语。在构造模态逻辑中，公式\Diamond F 表示F 是一致的。在其实现 s:F 中，见证项 s 代表公式 F 的抽象见证模型。

另一个例子是二元道义逻辑（DDL），它可以通过两种模态 \Box 和 \bigcirc 进行公理化。公式 \Box F 意味着 F 为真，条件 \bigcirc(F/G) 意味着给定 G 时 F 是强制性的。 Faroldi、Rohani 和 Studer (2023) 考虑 DDL 的显式版本。同样，\Box F 是通过 \mathsf{LP} 中的证明项来实现的，而 \bigcirc(F/G) 是通过使用代表道义原因的新型项来实现的。

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

有一种技术可以使用论证逻辑来分析同一事实的不同论证，特别是当某些论证是事实的而另一些则不是时。为了演示该技术，请考虑一个众所周知的示例：

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

正如第 1.1 节中讨论的红谷仓示例一样，这里必须处理真实陈述的两种理由，其中之一是正确的，而其中之一则不正确。设 B 是一个句子（命题原子），w 是 B 错误原因的指定论证变量，r 是 B 正确（因此是事实）原因的指定论证变量。然后，罗素的例子提示了以下一组假设[7 ]:

\mathcal{R} = \{w : B , r : B , r : B \rightarrow B\}

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

r : B（假设）

r : B \rightarrow B （假设）

B（来自 Modus Ponens 的 1 和 2）

B \rightarrow ( w : B \rightarrow B) （命题公理）

w : B \rightarrow B （来自 Modus Ponens 的 3 和 4）

然而，这一推导利用了 r 是 B 的事实证明来得出 w : B \rightarrow B 的事实，这构成了 w : B 的“诱导事实性”的情况。问题是，如何区分“真实” r : B 的事实性来自 w : B 的“诱导事实性”？这里需要某种证据跟踪，而论证逻辑是一个合适的工具。自然的方法是考虑没有 r : B 的假设集，即

\mathcal{S} = \{w: B, r :B \rightarrow B\}

并确定 w 的事实性，即 w : B \rightarrow B 不能从 \mathcal{S} 导出。这是一个可能的世界论证模型 \mathcal{M} = (\mathcal{G} , \mathcal{R} , \mathcal{E} , \mathcal{V}) 其中 \mathcal{S} 成立，但 w : B \rightarrow B 不：

\mathcal{G} = \{\mathbf{1}\},

\mathcal{R} = \varnothing ，

\mathcal{V} ( B) = \varnothing （因此不是 - \mathbf{1} \Vdash B），

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

\mathcal{E} ( r , B) = \varnothing 。

很容易看出，满足 \mathcal{E} 上的闭包条件 Application 和 Sum 。在 \mathbf{1} 处，w : B 成立，即

\mathbf{1} \Vdash w : B

因为 w 是 B 在 \mathbf{1} 处的可接受证据，并且从 \mathbf{1} 不存在可访问的可能世界。此外，

\text{非-}\mathbf{1} \Vdash r : B

因为，根据 \mathcal{E} ， r 不是 B 在 \mathbf{1} 处的可接受的证据。因此：

\mathbf{1} \Vdash r : B \rightarrow B

另一方面，

\text{非-}\mathbf{1} \Vdash w : B \rightarrow B

因为 B 在 \mathbf{1} 处不成立。

7. 理由的自我指涉

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

理由的自我指涉是传统情态语言中不存在的新现象。除了是有趣的认知对象之外，这种自我指涉断言还因为内在的恶性循环而从语义角度提供了特殊的挑战。事实上，要评估 c，人们会期望首先评估 A，然后将 A 的理由对象分配给 c。然而，这是无法完成的，因为 A 包含尚未评估的 c。模态逻辑是否可以在不使用自我指涉论证的情况下实现的问题是该领域的一个主要悬而未决的问题。

库兹涅茨在（Brezhnev and Kuznets 2006）中的主要结果表明，在 \mathsf{LP} 中实现 \mathsf{S4} 时，论证的自我指涉是不可避免的。库兹涅茨提出的以下定理给出了当前的情况：

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

该定理确立了 \mathsf{S4} 的证明项系统必然是自指的。这对可证明性语义造成了严重的（尽管不是直接可见的）限制。在哥德尔算术证明的背景下，这个问题是通过将算术语义分配给自指断言 c 的通用方法来解决的：A ( c) 声明 c 是 A ( c) 的证明。在证明逻辑 \mathsf{LP} 中，它是通过一个不平凡的定点构造来处理的。

自我参照为摩尔悖论提供了一个有趣的视角。有关详细信息，请参阅补充文件“更多技术问题”的第 6 节。

直觉逻辑\mathsf{IPC}的BHK语义的自指问题已经由Junhua Yu回答（Yu 2014）。扩展库兹涅茨的方法，他建立了

定理 6：双重否定直觉法则 \neg\neg(\neg\neg p \rightarrow p) 的每个 \mathsf{LP} 实现都需要自指常数规范。

更一般地说，Yu 证明了经典同义反复的任何双重否定（根据 Glivenko 定理，它们都是 \mathsf{IPC} 的定理）需要自指常数规范才能在 \mathsf{LC} 中实现。另一个不可避免的自我指涉的例子是 Yu 在 \mathsf{IPC} 的纯粹蕴涵片段中发现的。这表明直觉逻辑（甚至只是直觉蕴涵）的 BHK 语义本质上是自指的，需要一个定点构造将其与 PA 或类似系统中的形式证明连接起来。这可能部分解释了为什么任何在没有自我指涉的情况下以直接归纳方式构建可证明性 BHK 语义的尝试注定会失败。

8. 论证逻辑中的量词

虽然对命题论证逻辑的研究还远未完成，但也对一阶版本进行了一些工作。模态逻辑的量化版本已经提供了超出标准一阶逻辑的复杂性。当涉及论证逻辑时，量化可以发挥更广阔的作用。传统上，人们对“对象”进行量化，并且模型配备了一个量词范围的域。从模态上讲，一个人可能有一个对所有可能的世界通用的单一域，或者一个人可能对每个世界有单独的域。巴坎公式的作用在这里是众所周知的。恒定域和变化域选项也可用于调整逻辑。此外，还有一种模态逻辑没有类似的可能性：人们可能会量化论证本身。

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

定理 7：证明的一阶逻辑不是递归可枚举的（Artemov 和 Yavorskaya (Sidon) 2001）。带有量词的证明逻辑是不可递归枚举的（Yavorsky 2001）。

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