证明论语义学（二）

1.2 推理主义、直觉主义、反实在论

证明论语义学本质上是推理性的，因为它是推理活动，表现在证明中。因此，它属于推理主义（由 Brandom 创造的术语，参见其 1994 年；2000 年），根据该理论，推理和推理规则确定了表达式的意义，与指称主义相反，根据该理论，指称是主要的意义。推理主义和语义学的“意义即使用”观点是证明论语义学的广泛哲学框架。这种普遍的哲学和语义观点与源自数学哲学（尤其是数学直觉主义）的建设性观点相融合。大多数形式的证明论语义学在精神上都是直觉主义的，这尤其意味着经典逻辑的原理（例如排中律或双重否定律）被拒绝或至少被认为是有问题的。这部分是由于证明论语义学的主要工具自然演绎演算偏向于直觉逻辑，因为其消去规则的直接表述是直觉主义的。在那里，经典逻辑只能通过某种间接证明规则获得，这至少在一定程度上破坏了推理原理的对称性（参见第 3.5 节）。如果采用自然演绎的立场，那么直觉逻辑就是一个自然逻辑系统。逻辑符号的 BHK（Brouwer-Heyting-Kolmogorov）解释也起着重要作用。这种解释不是语义学的独特方法，而是包含各种通常以非正式而非正式描述的形式出现的思想。尤为重要的是其对蕴涵的功能观点，根据该观点，�→� 的证明是一个构造函数，当将其应用于 A 的证明时，将得出 B 的证明。这种功能视角是许多证明论语义学概念的基础，特别是 Lorenzen、Prawitz 和 Martin Löf 的概念（参见第 2.1.1、2.2.2、2.2.3 节）。

根据 Dummett (1975) 的说法，直觉主义的逻辑立场与反现实主义的哲学立场相对应。现实主义的认识独立于现实的观点是所有句子都是真或假的观点的形而上学对应物，与我们认识它的方式无关。证明论语义学的主要部分遵循 Dummett 及其与反现实主义的联系。

1.3 Gentzen 式证明理论：归约、规范化、切割消除

Gentzen 的自然演绎演算及其由 Prawitz 的呈现是大多数证明论语义学方法的背景。自然演绎基于至少三个核心思想：

假设的解除：假设可以在推导过程中“解除”或“消除”，因此自然演绎的核心概念是依赖于假设的推导。

分离：每个原始规则模式只包含一个逻辑常数。

引入和消除：逻辑常数的规则是成对出现的。引入规则允许人们推断出一个以所讨论的常数作为其主要运算符的公式，消除规则允许从这样的公式中得出后果。

在 Gentzen 的一阶逻辑自然演绎系统中，推导以树形形式编写，并基于众所周知的规则。例如，蕴涵具有以下引入和消除规则

[�]��→�→I�→���→E

其中括号表示排除假设 A 出现的可能性。推导的开放假设是最终公式所依赖的假设。如果推导没有开放假设，则称为封闭的，否则称为开放的。如果我们处理量词，我们还必须考虑开放的单个变量（有时称为“参数”）。对于证明论语义学来说至关重要的元逻辑特征，由 Prawitz (1965) 首次系统地研究并发表，包括：

归约：对于由引入和随后的消除组成的每个绕道，都有一个归约步骤来消除此绕道。

规范化：通过连续应用归约，可以将推导转换为不包含绕道的范式。

对于蕴涵，消除绕道的标准归约步骤如下：

[�]⋮��→�|��归约至|�⋮�

规范化的一个简单但非常重要的推论如下：直觉逻辑中的每个封闭式推导都可以在最后一步使用引入规则归约成推导。我们还说直觉自然演绎满足“引入形式属性”。在证明论语义学中，这一结果在“基本假设”标题下占有重要地位（Dummett，1991，第 254 页）。“基本假设”是对技术证明论结果进行哲学重新解释的典型例子。

进一步阅读：

有关证明论语义学的一般方向，请参阅 Kahle 和 Schroeder-Heister (2006) 编辑的 Synthese 特刊、Piecha 和 Schroeder-Heister (2016b) 编辑的读本、Francez (2015) 的教科书以及 Wansing (2000) 和 Schroeder-Heister (2016) 的调查。

有关证明理论的哲学立场和发展，请参阅希尔伯特纲领、证明理论的发展以及 Prawitz (1971) 的条目。

有关直觉主义，请参阅直觉主义逻辑、数学哲学中的直觉主义和直觉主义逻辑的发展的条目。

有关反现实主义，请参阅对形而上学现实主义的挑战以及 Tennant (1987; 1997) 和 Tranchini (2010; 2012a) 的条目。

有关 Gentzen 式证明理论和自然演绎理论，请参阅逻辑中的自然演绎系统条目，以及 Gentzen (1934/35) 的原始陈述、Jaśkowski (1934) 的假设理论、Prawitz (1965) 的经典专著、Tennant (1978; 2017)、Troelstra 和 Schwichtenberg (2000)、Negri 和 von Plato (2001)、Mancosu、Galvan 和 Zach (2021) 以及互联网哲学百科全书中 Andrzej Indrzejczak 的自然演绎条目。

2. 证明论语义的一些版本

2.1 蕴涵语义：可接受性、可推导性、规则

蕴涵语义是证明论语义的核心。与经典真值条件语义学相反，蕴涵本身就是一个逻辑常数。它还有一个特点，就是与结果概念紧密相关。它可以被看作是在句子层面表达结果，这是由于肯定前件和希尔伯特式系统中所谓的演绎定理，即 Γ,�⊢� 和 Γ⊢�→� 的等价性。

对蕴涵 �→� 的一个非常自然的理解是将其解读为表达允许人们从 A 到 B 的推理规则。根据 �→� 许可从 A 到 B 的步骤正是肯定前件所说的。而演绎定理可以看作是建立规则的手段：证明可以从 A 推导出 B 证明了可以从 A 推导出 B 的规则。沿着这样的思路，基于规则的蕴涵语义构成了几种证明论语义学概念的基础，尤其是 Lorenzen、von Kutschera 和 Schroeder-Heister 提出的概念。

2.1.1 操作逻辑

Lorenzen 在其《操作逻辑和数学导论》（1955 年）中从无逻辑（原子）演算开始，这些演算对应于生产系统或语法。如果一条规则可以在不扩大其可导出原子集的情况下添加到系统中，则他称该规则在这样的系统中是可接受的。蕴涵箭头 → 被解释为表达可接受性。如果一个蕴涵 �→� 在作为规则阅读时是可接受的（相对于底层演算而言），则该蕴涵 �→� 被认为是有效的。对于迭代蕴涵（= 规则），Lorenzen 发展了一种更高层次的可接受性陈述理论。某些陈述，例如

�→� 或

((�→�),(�→�))→(�→�)

独立于底层演算而成立。它们被称为普遍可接受的 [“allgemeinzulässig”]），并构成一个正蕴涵逻辑系统。以相关的方式，全称量化定律 ∀ 可以使用具有示意变量的规则的可接受性陈述来证明。

对于逻辑常数 ∧、∨、∃ 和 ⊥ 的定律的证明，Lorenzen 使用反演原理（他创造的一个术语）。逆序原理以一种非常简单的形式表示，不考虑规则中的变量，即从 A 的每个定义条件中得到的一切都可以从 A 本身中得到。例如，在析取的情况下，让 A 和 B 各自成为 �∨� 的定义条件，如原始规则 �→�∨� 和 �→�∨� 所表示的那样。然后逆序原理表示，在假设 �→� 和 �→� 的情况下，�∨�→� 是可接受的，这证明了析取的消除规则的合理性。其余的连接词以类似的方式处理。在 ⊥ 的情况下，荒谬规则 ⊥→� 是从 ⊥ 没有定义条件这一事实得出的。

2.1.2 Gentzen 语义

von Kutschera (1968) 在所谓的“Gentzen 语义”中，像 Lorenzen 一样，给出了逻辑上复杂的蕴涵式语句 �1,…,��→� 的语义，该语义与使用原子语句进行推理的演算 K 有关。与 Lorenzen 的根本区别在于，�1,…,��→� 现在表达的是可导出性语句，而不是可接受性语句。

为了将其转化为命题逻辑逻辑常量的语义，von Kutschera 论证如下：当放弃二价性时，我们不能再使用经典的真值赋值来指派原子公式。相反，我们可以使用证明或反驳原子语句的演算。此外，由于演算不仅能生成证明或反驳，还能生成任意的可导性关系，因此我们的想法是直接从原子系统中的可导性开始，并用表征逻辑联结词的规则对其进行扩展。为此，von Kutschera 给出了一个序贯演算，其规则用于在后项和前提中引入 n 元命题联结词，从而得到一个广义命题联结词的序贯系统。然后，Von Kutschera 继续证明，如此定义的广义联结词都可以用直觉逻辑的标准联结词（合取、析取、蕴涵、荒谬）来表达。

进一步阅读：

有关 von Kutschera 风格的表达完整性扩展：Wansing (1993a)。

2.1.3 具有高级规则的自然演绎

在为任意逻辑常数开发推理规则的通用模式时，Schroeder-Heister (1984) 提出了一种语义要求，即逻辑复杂的公式表达规则系统的内容或共同内容。规则 R 要么是公式 A，要么具有形式 �1,…,��⇒�，其中 �1,…,�� 是规则。这些所谓的“高级规则”将规则可以履行假设公式的想法推广到它们可以履行假设规则（即用作假设的规则）的情况。对于标准连接词，这意味着 �∧� 表达对 (�,�) 的内容； �→� 表达规则 �⇒� 的内容； �∨� 表达了 A 和 B 的共同内容；而荒谬性 ⊥ 表达了空规则系统家族的共同内容。对于任意的 n 元命题联结词，这导致具有广义引入和消除规则的自然演绎系统。这些一般联结词被证明可以根据标准联结词来定义，这确立了标准直觉联结词的表达完整性。

2.2 基于引入规则的推导语义

2.2.1 反转原则与和谐

在《逻辑演绎研究》中，Gentzen 对自然演绎中引入和消除推理之间的语义关系做了一些（经常被引用的）纲领性评论。

引入代表了所涉及符号的“定义”，而消除归根结底只不过是这些定义的结果。这一事实可以表达如下：在消除一个符号时，我们只能“按照引入该符号所赋予的意义”使用我们正在处理的终止符号的公式。（Gentzen，1934/35，第 80 页）

当然，这并不意味着消除规则可以从引入规则中推导出来，事实上，它们不是。这只能意味着它们可以以某种方式被它们证明。

通过使这些想法更加精确，应该能够根据某些要求将 E 推理显示为其相应 I 推理的独特函数。（同上，第 81 页）

因此，Gentzen 计划背后的思想是，我们有引入规则形式的“定义”和某种语义推理，通过使用“某些要求”来验证消除规则。

Prawitz (1965) 采用了 Lorenzen 的术语，并将其基本思想（见第 2.1.1 节）调整到自然演绎的背景下，制定了一个“反转原则”，以使 Gentzen 的评论更加精确：

设 � 是消除规则的一个应用，其结果为 B。那么，满足推导 � 大前提的充分条件 […] 的演绎，当与 � 的小前提（如果有）的演绎相结合时，已经“包含”了 B 的演绎；因此，B 的演绎可以直接从给定的演绎中获得，而无需添加 �。（第 33 页）

这里的充分条件由相应的引入规则的前提给出。因此，反转原理认为，如果在最后一步使用引入规则得出了大前提，则可以不应用消除规则得出其结论，这意味着可以避免步骤的组合

⋮�I-推理{��}�E-推理

，其中 {��} 代表（可能为空的）小前提推论列表。

引入规则和消除规则之间的关系通常被描述为“和谐”（Dummett 1973，第 396-397 页），或受“和谐原则”的支配（Tennant，1978，第 74 页）。这个术语并不统一，有时甚至不完全清楚。它本质上表达了“反转”的含义。即使“和谐”是一个表示对称关系的术语，它也经常被理解为表达一种基于引入规则的概念，例如 Read (2010) 的“广义消去和谐”（尽管有时也包括基于消去的概念）。有时和谐被认为意味着连接词在给定其引入或消去规则的情况下在某种意义上最强或最弱。这一思想是 Tennant (1978) 和谐原则以及 Popper 和 Koslow 的结构特征的基础（见第 2.4 节）。倒置原则中表述的引入和消去规则之间的特定关系排除了所谓的推理定义，例如连接词 tonk，它将析取的引入规则与合取的消去规则相结合，并引发了关于推理定义格式的持续争论。和谐的形式化表征使用了将推理规则转化为二阶命题逻辑（Girard 的系统 F），并已成为内涵证明论语义学的中心主题（Tranchini，2023）。