证证逻辑（二）_数学联邦政治世界观

2.2 基本证立逻辑 J0

证立项由证立变量 x、y、z、… 和证立常量 a、b、c、…（索引 i = 1、2、3、…，在安全的情况下可省略）通过运算“⋅”和“+”构建而成。下文讨论的更复杂的逻辑也允许对证立进行额外的运算。常量表示系统不分析的原子证立；变量表示未指定的证立。基本证立逻辑 J0 由以下公理化实现。

经典逻辑

经典命题公理和肯定前件规则

应用公理

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

求和公理

s:F→[s + t]:F， s:F→[t + s]:F。

J0 是针对绝对怀疑主体的一般（不一定是事实性的）证立逻辑，对于该主体，没有任何公式能够被证明是正当的，即 J0 无法针对任何 t 和 F 推导出 t:F。然而，这样的主体能够得出如下形式的相对证立结论：

如果 x:A,y:B,…,z:C 成立，则 t:F。

凭借这种能力，J0 能够用其语言充分模拟许多其他证立逻辑系统。

2.3 逻辑意识与常数规范

逻辑意识原则指出，逻辑公理是依职权（ex officio）得到证实的：主体接受逻辑公理作为已证实的公理（包括与证实相关的公理）。正如刚才所述，在某些认知情境中，逻辑意识可能过于强势。然而，证实逻辑提供了灵活的常数规范机制，可以表示不同程度的逻辑意识。

当然，假设和已证实的假设之间是有区别的。在论证逻辑中，常量用于表示假设的论证，前提是假设无需进一步分析。假设需要假定公理A对于认知者而言是合理的。只需对某个证据常数e1（索引为1）假设e1:A即可。此外，如果还需要假定这个新原理e1:A也是合理的，则可以对常数e2（索引为2）假设e2:(e1:A)。依此类推。记录索引并非必需，但记录索引很容易，并且有助于决策过程（Kuznets 2008）。对于给定逻辑，所有此类假设的集合称为常数规范。正式定义如下：

对于给定的辩护逻辑 L，常数规范 CS 是一组形式为

en:en−1:…:e1:A(n≥1) 的公式，

其中 A 是 L 的公理，e1,e2,…,en 是索引为 1, 2, …, n 的相似常数。假设 CS 包含所有中间规范，即，只要 en:en−1:…:e1:A 在 CS 中，则 en−1:…:e1:A 也在 CS 中。

文献中对常数规范提出了许多特殊条件。以下是最常见的。

空

CS=∅。这对应于一个绝对怀疑论主体。这相当于使用逻辑 J0。

有限

CS 是一组有限的公式。这是一个完全典型的情况，因为辩护逻辑中的任何特定推导都只涉及一组有限的常数。

公理化适用

每个公理，包括那些通过常数规范本身新获得的公理，都有其正当性。在正式的设定中，对于每个公理 A，存在一个常数 e1，使得 e1:A 在 CS 中，并且如果 en:en−1:…:e1:A∈CS，则对于每个 n≥1，en+1:en:en−1:…:e1:A∈CS。为了确保本节末尾讨论的内化特性，公理上合适的常数规范是必要的。

总计

对于每个公理 A 和任何常数 e1,e2,…,en，

en:en−1:…:e1:A∈CS。

名称 TCS 保留用于（对于给定逻辑的）总常数规范。当然，总常数规范在公理上是合适的。

我们现在可以指定：

给定常数规范的证明逻辑：

设 CS 为常数规范。JCS 是逻辑 J0 + CS；公理是 J0 的公理以及 CS 的成员，唯一的推理规则是肯定前件。注意 J0 是 J∅。

证明逻辑：

J 是逻辑 J0 + 公理内化规则。新规则规定：

对于每个公理 A 和任何常数 e1,e2,…,en，推断 en:en−1:…:e1:A。

后者体现了对J的不受限制的逻辑意识的理念。类似的规则出现在《证明逻辑LP》中，并且也已在Goldman的著作（Goldman 1967）中得到预见。逻辑意识，用公理上合适的常数规范来表达，是模态逻辑中必然性规则的明确体现：⊢F⇒⊢◻F，但仅限于公理。注意，J与JTCS重合。

论证逻辑系统的关键特征是它们能够将其自身的推导内化为其语言中可证明的论证断言。这一特性在（Gödel 1938）中得到了预见。

定理1：对于每个公理上合适的常数规范CS，JCS享有内化：

如果⊢F，则⊢p:F，其中某个论证项p。

证明：对推导长度进行归纳。假设 ⊢ F。如果 F 是 J0 的成员，或者是 CS 的成员，则存在一个常数 en（其中 n 可能是 1）使得 en:F 在 CS 中，因为 CS 在公理上是合适的。则 en:F 可导。如果 F 可由 X→F 和 X 通过肯定前件推理得到，则根据归纳假设，对于某些 s,t，⊢s:(X→F) 且 ⊢t:X。利用应用公理，⊢[s⋅t]:F。

有关论证逻辑中具体句法推导的示例，请参阅补充文件《更多技术问题》第 2 节。

2.4 扩展基本论证逻辑

基本论证逻辑 J0 及其具有常数规范 JCS 的扩展，是最小正态模态逻辑 K 的明确对应物。由于实现的概念是核心，因此将在第 4 节中给出对应物的正确定义，但在我们介绍的这个阶段，一些提示已经很明显了。例如，在1.1节中指出，(1)，s:(A→B)→(t:A→[s⋅t]:B)，是我们所熟悉的模态原理(2)◻(A→B)→(◻A→◻B)的显式版本。类似地，第一个证立逻辑LP是模态逻辑S4的显式对应物。事实证明，许多模态逻辑都有证立逻辑对应物——实际上，通常不止一个。接下来，我们将首先讨论一些非常熟悉的逻辑，直至S4和LP。到目前为止，我们最初的动机大部分都适用——我们拥有可以用算术解释的证立逻辑。然后，我们转向更广泛的模态逻辑家族，算术动机不再适用。模态逻辑中存在证立逻辑对应物的现象已被证明出乎意料地广泛。

在几乎所有情况下，都必须在 J0 的 + 和 ⋅ 上添加运算，并建立描述其预期行为的公理。例外的是事实性（下文将讨论），它不需要额外的运算，但需要额外的公理。常数规范始终涵盖扩大集合中的公理。我们继续使用 2.3 节中的术语；例如，如果一个常数规范满足那里所述的条件，则它公理化地适用，适用于所有公理，包括任何已添加到原始集合中的公理。2.3 节中的定理 1 继续适用于我们新的辩护逻辑，并具有相同的证明：如果我们有一个辩护逻辑 JLCS，其常数规范公理化地适用，则内化成立。

2.5 事实性

事实性表明，辩护足以使主体得出真值。这体现在以下内容中：

事实性公理 t:F→F。

事实性公理与认识论逻辑的真值公理◻F→F 有着类似的动机，后者被广泛接受为知识的基本属性。

基本证立逻辑系统不要求证立具有事实性，这使得它们能够表示部分证立和事实性证立。事实性公理出现在《证明逻辑LP》第1.2节中，作为数学证明的一个主要特征。事实上，在这种情况下，事实性显然有效：如果存在F的数学证明t，则F必定为真。

事实性公理适用于导致知识的证立。然而，正如Gettier的例子（Gettier 1963）所证明的那样，单凭事实性并不能保证知识的获得。

事实证立逻辑：

JT0=J0 + 事实性；

JT=J + 事实性。

对应于常数规范CS的系统JTCS的定义如第2.3节所示。

2.6 积极内省

知识的共同原则之一是识别知识和知道自己知道。在模态设置中，这对应于◻F→◻◻F。这一原则有一个充分明确的对应物：代理接受 t 作为 F 的充分证据，这一事实本身也构成了 t:F 的充分证据。这种“元证据”通常具有物理形式：证明论文中某个证明正确的审稿报告；给定 F 的形式化证明 t 作为输入的计算机验证输出；t 是 F 证明的形式化证明，等等。为此，可以在语言中添加一个正向自省运算“!”；然后假设给定 t，代理会生成 t:F 的正当性证明 !t，使得 t:F→!t:(t:F)。这种运算形式的正向自省最早出现在《证明逻辑 LP》中。

正向自省公理：t:F→!t:(t:F)。

然后我们定义：

J4:=J + 正向自省；

LP:=JT + 正向自省。[3]

逻辑 J40、J4CS、LP0 和 LPCS 以自然方式定义（参见 2.3 节）。

在正向自省公理存在的情况下，可以将公理内化规则的范围限制为内化非 e:A 形式的公理。LP 中就是这样做的：然后可以使用 !!e:(!e:(e:A)) 代替 e3:(e2:(e1:A)) 等来模拟公理内化。常数规范的概念也可以相应简化。这些修改很小，不会影响论证逻辑的主要定理和应用。

2.7 负向自省

(Pacuit 2006, Rubtsova 2006) 考虑了负向自省运算“?”，它可以验证给定的论证断言是否为假。考虑这种操作的一个可能动机是，积极的内省操作“！”很可能被认为能够对论证断言 t:F 的有效性提供结论性的验证判断，因此当 t 不是 F 的论证时，这样的“！”应该得出¬t:F的结论。这通常是计算机证明验证器、形式理论中的证明检查器等的情况。然而，这种动机是微妙的：证明验证器和证明检查器的示例将t和F作为输入，而Pacuit-Rubtsova格式?t表明“？”的唯一输入是证明t，并且结果?t应该对所有t:F不成立的F一致地证明命题¬t:F。这种运算“？”在形式数学证明中不存在，因为?t应该是无穷多个命题¬t:F的单一证明，这是不可能的。从历史上看，“？”运算是第一个不符合原始框架的例子，在该框架中，证明是形式证明的抽象版本。

负自省公理 ¬t:F→?t:(¬t:F)

我们定义以下系统：

J45=J4 + 负自省；

JD45=J45 + ¬t:⊥；

JT45=J45 + Factivity

并自然地将这些定义扩展为 J45CS、JD45CS 和 JT45CS。

2.8 Geach 逻辑及其他

涉及 ? 的证明逻辑是超越 LP 子逻辑的第一个例子。最近发现，存在一个无限的模态逻辑家族，它们具有证明对应物，但与算术证明的联系较弱或缺失。我们将详细讨论一个案例，并概述其他案例。

Peter Geach 提出了公理方案 ◊◻X→◻◊X。当它被添加到公理S4中时，它产生了一个有趣的逻辑，称为S4.2。从语义上讲，Geach的方案将汇合强加于框架之上。也就是说，如果两个可能世界w1和w2可以从同一个世界w0访问，那么就存在一个共同的世界w4，可以从w1和w2访问。Geach 方案在 Lemmon 和 Scott (1977) 的著作中得到了推广，并引入了相应的符号：Gk,l,m,n 表示方案 ◊k◻lX→◻m◊nX，其中 k,l,m,n≥0。从语义上讲，这些方案对应于广义的汇流方案。有些人开始将这些方案称为 Geach 方案，我们也将沿用这种做法。更一般地，如果一个模态逻辑可以通过向 K 添加一组有限的 Geach 方案来实现公理化，我们就称它为 Geach 逻辑。原始 Geach 方案为 G1,1,1,1，但同时注意 ◻X→X 为 G0,1,0,0，◻X→◻◻X 为 G0,1,2,0，◊X→◻◊X 为 G1,0,1,1，而 X→◻◊X 为 G0,0,1,1，因此 Geach 逻辑包含了最常见的模态逻辑。Geach 逻辑构成了一个无限逻辑家族。

每个 Geach 逻辑都有一个相应的证明。考虑原始 Geach 逻辑，将公理方案 G1,1,1,1，◊◻X→◻◊X 添加到 S4 的系统——即上面提到的系统 S4.2。我们从LP开始，公理化地构建S4.2的对应论证。然后，我们添加两个函数符号f和g，每个函数符号都是两位数，并采用以下公理方案，将得到的论证逻辑称为J4.2。

¬f(t,u):¬t:X→g(t,u):¬u:¬X

该方案有一些非正式的动机。在LP中，由于公理方案t:X→X，对于任何t和u，我们都有(t:X∧u:¬X)→⊥的可证明性，从而也有¬t:X∨¬u:¬X的可证明性。在任何情况下，其中一个析取式必定成立。上述方案等价于f(t,u):¬t:X∨g(t,u):¬u:¬X，这非正式地表明，在任何情况下，我们都有方法计算出成立的析取式的论证。这是一个强假设，但至少在某些情况下并非难以置信。

一个实现定理将 S4.2 和 J4.2 联系起来，尽管目前尚不清楚这是否有一个构造性的证明。

再举一个例子，考虑 G1,2,2,1，◊◻◻X→◻◻◊X，或等价地，◻¬◻◻X∨◻◻¬◻X。它具有如下对应的证明公理方案，其中 f、g 和 h 是三元函数符号。

f(t,u,v):¬t:u:X∨g(t,u,v):h(t,u,v):¬v:¬X

f、g 和 h 的直观解释不如 G1,1,1,1 那样清晰，但形式上表现良好。

尽管 Geach 逻辑家族是无限的，但这些逻辑并未涵盖所有具有证明对应项的逻辑。例如，使用公理方案 ◻(◻X→X) 的正则模态逻辑（有时也称为移位自反性）不是 Geach 逻辑，但它确实具有证明对应项。在构建证立项的机制中添加一个一位函数符号 k，并采用证立公理方案 k(t):(t:X→X)。实现定理成立；这在 Fitting (2014b) 中得到证明。我们推测所有用萨尔奎斯特公式公理化的逻辑都会有证立对应物，但这目前仍是一个猜想。

3. 语义

证立逻辑的现有标准语义源自 (Fitting 2005)——所使用的模型在文献中通常被称为 Fitting 模型，但本文将被称为可能世界证立模型。可能世界证立模型是由 Hintikka 和 Kripke 提出的我们熟悉的知识和信念逻辑的可能世界语义与 Mkrtychev 在 (Mkrtychev 1997) 中引入的针对证立项的特定机制（参见第 3.4 节）的混合体。

3.1 J 的单智能体可能世界证成模型

确切地说，需要定义 JCS 的语义，其中 CS 是任意常量规范。形式上，JCS 的可能世界证成逻辑模型是一个结构 M=⟨G,R,E,V⟩。其中，⟨G,R⟩ 是一个标准的 K 框架，其中 G 是可能世界集合，R 是该集合上的二元关系。V 是从命题变量到 G 子集的映射，指定可能世界中的原子真值。

新概念是 E，一个证据函数，源自 (Mkrtychev 1997)。它将论证项和公式映射到世界集合。直观的想法是，如果可能世界 Γ 在 E(t,X) 中，那么 t 就是在世界 Γ 处对 X 相关的或可采纳的证据。不应将相关证据视为结论性的。相反，应将其视为可以在法庭上采纳的证据：这份证词、这份文件是陪审团应该审查的，是相关的，但其真值判定状态尚待考量。证据函数必须满足某些条件，但这些条件稍后再讨论。

给定一个JCS可能世界论证模型M=⟨G,R,E,V⟩，公式X在可能世界Γ的真值记为M,Γ⊩X，并要求满足以下标准条件：

对于每个Γ∈G：

M,Γ⊩P当且仅当Γ∈V(P)，其中P为命题字母；

不存在M,Γ⊩⊥；

M,Γ⊩X→Y当且仅当M,Γ⊩X或M,Γ⊩Y不存在。

这些只是表明原子真值是任意指定的，而命题联结词在每个世界中都具有真值函数性。关键点在于下一点。

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

该条件分为两部分。第一部分要求对于每个 Δ∈G，M,Δ⊩X，使得 ΓRΔ，这是我们熟悉的 Hintikka/Kripke 条件，即 X 在 Γ 处是可信的或可相信的。第二部分要求 Γ∈E(t,X)，并附加了 t 应该是 X 在 Γ 处的相关证据。然后，非正式地讲，如果 X 在某个可能世界中，按照通常的认识论逻辑，是可相信的，那么 t:X 在那个可能世界中为真。并且 t 是该世界中 X 的相关证据。

重要的是要认识到，在这种语义下，人们可能因为某个特定原因而不相信某个世界中的某件事，要么是因为它根本不可信，要么是因为它可信但理由不充分。

仍然必须对证据函数施加一些条件，并且还必须考虑常数规范。假设给定 s 和 t 作为论证。可以用两种不同的方式将它们组合起来：同时使用两者的信息；或者只使用其中一个的信息，但首先选择哪一个。每种方式都会产生一个关于论证项 ⋅ 和 + 的基本运算，这在第 2.2 节中以公理化的方式引入。

假设 s 是蕴涵式的相关证据，t 是前件的相关证据。那么 s 和 t 一起提供了后件的相关证据。假设证据函数满足以下条件：

E(s,X→Y)∩E(t,X)⊆E(s⋅t,Y)

添加此条件后，

s:(X→Y)→(t:X→[s⋅t]:Y)

的有效性得到保证。

如果s和t都是证据项，则可以说某事由s或t之一证明，而无需具体指明是哪一个，这仍然是证据。对证据函数施加以下要求：

E(s,X)∪E(t,X)⊆E(s+t,X)

不出所料，

s:X→[s+t]:X

和