证明论语义学（四）

还有几种其他方法可以对逻辑常量进行统一的证明论表征，所有这些方法都至少涉及证明论语义学的问题。这些理论包括贝尔纳普的显示逻辑 (Belnap, 1982)、万辛的信息结构逻辑 (Wansing, 1993b)、通用校样编辑系统及其实现，如爱丁堡逻辑框架 (Harper、Honsell 和 Plotkin, 1987) 以及许多允许指定各种逻辑系统的后继者。自从线性逻辑和更一般的子结构逻辑兴起以来，出现了各种处理逻辑的方法，这些方法在结构规则的限制方面有所不同 (参见第 3.10 节)。最近，人们不再将某种特定的逻辑单独列为真正的逻辑，而是采取一种更加多元化的立场 (例如，参见 Beall 和 Restall, 2006)，这种立场关注的是不同逻辑的共同点，而不偏爱某种特定的逻辑，这可以看作是从语义论证向结构表征的转变。

进一步阅读：

有关波普尔的逻辑常数理论，请参阅 Binder 等人 (2022)、Piecha (2023)。

有关逻辑常数及其逻辑性，请参阅关于逻辑常数的条目。

有关线性和子结构逻辑，请参阅关于线性逻辑的条目和关于子结构逻辑的条目。

有关逻辑中的多元性，请参阅关于逻辑多元性的条目。

2.5 范畴论证明理论

关于范畴论与证明理论相关的文献很多，根据 Lawvere、Lambek 等人的开创性工作（请参阅 Lambek and Scott, 1986），范畴论本身可以看作是一种抽象证明理论。如果将类别中的箭头“→”视为从 A 得出 B 的一种抽象证明，那么我们就有了一种超越从 A 得出 B 的纯粹可推导性的表示（因为箭头有其个性），但不涉及该证明的特定句法结构。对于直觉系统，类别形式的证明论语义可能最接近经典情况下的形式语义。

类别证明论最发达的方法之一归功于 Došen。他不仅推进了类别方法在证明论中的应用（例如，Došen 和 Petrić，2004），而且还展示了如何将证明论方法用于类别论本身（Došen，2000）。对于类别逻辑与证明论语义的关系而言，最重要的是，在类别逻辑中，箭头总是与身份关系结合在一起，这在证明论中对应于证明的身份。这样，范畴论证明理论的思想和结果就属于所谓的内涵证明论语义学（见第 3.7 节），即研究证明本身是实体，而不仅仅是确定后果的工具（Došen，2006；2016）。

由于范畴意义上的箭头和演绎推理意义上的证明之间存在着密切的关系，因此几乎所有在演绎领域处理的概念都有范畴类似物，通常采用新颖的方法、思想和结果，以非常有效的方式补充演绎方法。范畴论证明论语义学是一个非常广泛的研究领域，与本条目采用的演绎视角并行 —— 演绎视角在哲学中更为常见。在直觉逻辑领域，范畴逻辑涵盖了非常先进的主题：超越标准量词逻辑的 Martin-Löf 传统依赖类型理论（见第 2.2.3 节），包括同伦类型理论。对于许多其他逻辑系统，已经开发了范畴语义学，包括经典逻辑和各种子结构逻辑，例如线性逻辑。

范畴证明论的一个在哲学上非常重要的一般特征是其固有的假设性。这是因为它从假设语句�→�（箭头）而不是范畴语句 A 开始（“范畴”与“假设”相对，而不是“范畴”，此处用于“属于范畴论”）。这样，它克服了标准范式，特别是基于有效性的证明论语义（参见第 3.6 节）。

进一步阅读：

有关一般范畴方法，请参阅范畴论条目和数学哲学中的结构主义条目。

有关范畴证明论语义学，请参阅 Pym、Ritter 和 Robinson（2023 年，其他互联网资源）。

2.6 原子系统

证明论语义学主要关注逻辑常数。即使人们同意这种倾向——定义反射理论（见第 2.3.2 节）是个例外——我们仍然必须确定原子句及其证明的地位。在模型论语义学中，逻辑复杂句子的真值是根据结构定义的，该结构称为该句子的“模型”。该结构决定了哪些原子句为真，哪些不为真。复杂句子是否为真取决于其原子成分。这在证明论语义学中非常类似。复杂句子的证明是否有效取决于所考虑系统的原子基础。在这里，原子基础通常被视为生成原子句的演算：原子基础中原子句的证明本身有效。与模型论中将逻辑真理定义为对所有结构都为真理的定义类似，在证明论语义学中，人们将逻辑上有效的证明定义为对所有原子基都有效的证明。

有多种原子系统可以被视为原子基的候选者。 (1) 最简单的是逻辑编程理论中使用的 Herbrand 模型，它只是原子句子的集合。从证明论的角度来看，这些将是仅由公理组成的演算，没有适当的推理规则。 (2) 在 Lorenzen（见第 2.1.1 节）和 Prawitz（见第 2.2.2 节）的著作中，原子系统被视为产生规则列表，即具有公理和规则的演算，形式为�1,…,��⇒�，允许人们从�1,…,��生成 B。 (3) 更复杂的系统可能包含允许人们解除假设的原子规则，这与蕴涵引入等逻辑规则非常类似。 (4) 概括这一思想，人们可以承认原子规则本身可以解除规则，即更高级别的规则（参见第 2.1.3 节）。 (5) 更先进的是包含定义反射规则的原子系统（参见第 2.3.2 节）。——可以想象构成原子系统的许多其他类型的原子规则。

对于证明论语义学，这里的关键点是某些形式结果取决于哪些类型的原子系统被接受。这尤其适用于语义完整性问题（参见第 2.8 节）。关于哪些原子系统作为证明论语义学的原子基础时会在逻辑层面导致哪些形式系统的研究才刚刚开始（参见 Sandqvist 2015b；Piecha 和 Schroeder-Heister，2016a；Stafford 2023，其他网络资源）。需要注意的是，这是证明论语义学的内涵特征：我们感兴趣的不仅仅是哪些原子是由各种形式的原子系统生成的，还在于这是如何生成的，即通过哪种类型的规则实现的。这是与模型论语义学的一个重要区别，模型论语义学在这方面是纯粹外延的。有关证明论语义学的更多内涵特征，请参见第 3.7 节。

2.7 基于句子的语义

人们可以直接定义句子的证明理论有效性，而不是定义句子证明的有效性。在定义逻辑复杂句子的有效性时，人们将放弃对这些句子证明的引用。这并不意味着人们放弃了证明理论方法，因为人们仍然会引用原子基础中的证明。证明出现在原子层面，但不出现在逻辑层面。从技术上讲，这种方法比基于证明有效性的方法（参见第 2.2.2 节）更简单，但仍然足以讨论语义完整性等基本主题（参见第 2.8 节）。事实上，从第 2.2.2 节意义上有效的句子 A 的证明，可以推断出 A 在基于句子的语义意义上的有效性；相反，从基于句子的语义中的 A 的有效性，可以构建 A 的（尽管是退化的）有效证明。从某种意义上说，基于句子的语义与 Martin-Löf 系统中固有的证明论语义相关（参见第 2.2.3 节），在基本逻辑（依赖类型不起任何作用）的情况下，可以丢弃判断 �:� 的证明信息 t，而采用简化判断 � true。

对于最小命题逻辑中以原子系统 S 作为其原子基础的句子有效性，一种可能的定义如下：

如果原子公式 A 在 S 中可导出，则它为 S 有效。

如果 A 和 B 都为 S 有效，则合取 �∧� 为 S 有效。

如果 A 或 B 为 S 有效，则析取 �∨� 为 S 有效。

如果对于 S 的每个扩展 �′，如果 A 如果 �′-有效则 B �′-有效，则蕴涵 �→� 是 S 有效的。

请注意，在假设有效性陈述中，参考了所考虑的原子基础的任意扩展。与证明有效性的正式定义一样，考虑基础扩展用于确保单调性并避免空洞的有效性。在文献中，根据 Sandqvist (2015a) 的说法，“基础扩展语义”一词通常以更具体的含义使用：即一种特殊形式的基于句子的语义，其中析取得到了一种异常的解释。

基于句子的语义的有效性取决于原子系统的选择。这种选择使基于句子的语义具有证明理论性。如第 2.6 节所示，原子系统的类型很重要，对于蕴涵和后果陈述考虑的扩展关系也很重要。

2.8 语义完整性

证明论语义学在精神上是直觉主义的，至少从其起源来看是如此。相应地，Prawitz (1971) 推测，那些由对任何原子基有效的证明所证明的结果陈述 Γ⊨� 正是直觉逻辑形式系统的可导出性陈述 Γ⊢�。在句子语义学的框架内，对于与语义完整性相关的有效性问题，该框架比有效证明的框架更容易处理，这个猜想被证明是错误的。Harrop 规则

¬�→(�∨�)(¬�→�)∨(¬�→�)

在直觉逻辑中不可导出（但仅可接受），可以在该框架中验证（Piecha 和 Schroeder-Heister，2019）。然而，当原子基的扩展结构被修改为超出集合论超集关系时，情况就会发生变化，克里普克的直觉逻辑完备性证明就适用于证明论框架（Goldfarb 2016；Stafford 和 Nascimento 2023）。避免不完备性的另一种方法是赋予析取非标准解释，例如要求 ∨-消除规则的小前提和结论始终可以被视为原子的（参见 Sandqvist，2015a）。

进一步阅读：

有关 Prawitz 的完备性猜想，请参阅“证明论有效性示例”补充。

有关 Harrop 规则在直觉逻辑的可接受性陈述中的作用，请参阅直觉逻辑条目。

3. 标准证明论语义学的扩展和替代

3.1 消除规则作为基础

大多数证明论语义学方法将引入规则视为基础、意义赋予或自我证明，而消除推理则被证明是相对于给定的引入规则有效的。这一概念至少有三个根源：第一是意义的验证理论，根据该理论，句子的可断言性条件构成了其意义。第二是我们必须区分赋予意义的因素和这种意义的后果，因为并非所有推理知识都可以由定义的应用组成。第三是断言相对于其他言语行为（如假设或否认）的首要性，这在迄今为止考虑的所有方法中都是隐含的。

人们可以研究将消除规则而不是引入规则视为证明论语义学的基础可以走多远。 Dummett (1991, Ch. 13) 勾勒出了一些基于消去规则而非引入规则的证明论语义学思想，尽管形式非常初级。Prawitz (1971; 2007; 另见 Schroeder-Heister 2015) 对基于消去推理的有效性进行了更精确的定义。其基本思想是，如果将消去规则应用于其最终公式的结果是有效证明或简化为有效证明，则封闭式证明被认为是有效的。例如，如果对于任何给定的 A 的封闭式有效证明，将肯定前件式

�→��

应用于这两个证明的结果是 B 的有效证明，或简化为这样的证明，则蕴涵 �→� 的封闭式证明是有效的。这一概念保留了 Prawitz 式证明论语义学的三个基本要素中的两个（参见第 2.2.2 节）：证明简化的作用和假设的替代观点。只有以引言结尾的证明的规范性才会转变为以消除结尾的证明的规范性。

3.2 否定和否认

标准证明理论语义以断言为中心，因为可断言性条件决定了逻辑常数的含义。对应于直觉主义的处理方式，公式 A 的否定通常被理解为暗示荒谬 �→⊥，其中 ⊥ 是一个不能断言的常数，即没有定义可断言性条件。这是一种理解否定的“间接”方式。在文献中，人们讨论了根据 von Kutschera (1969) 的说法可以称为“直接”否定的内容。通过这种方式，人们可以理解一个一元的否定原始运算符，它不能或至少不会简化为暗示荒谬。它也不是经典的否定。它遵循对逻辑常数的通常规则进行对偶化的规则。有时它被称为句子的“否定”，有时也被称为“强否定”（参见 Odintsov，2008）。否定 A 的典型规则是

∼�∼�∼(�∨�)∼�∼(�∧�)∼�∼(�∧�)

本质上，运算符的否定规则对应于对偶运算符的断言规则。已经研究了几种否定逻辑，特别是 Nelson (1949) 的“可构造假性”逻辑，该逻辑由 Nelson 针对某种可实现语义所激发。主要关注的是他的系统，后来称为 N3 和 N4，它们在矛盾处理方面有所不同（N4 是没有 ex contradictione quodlibet 的 N3）。使用否定，任何证明论语义学方法都可以通过交换断言和否定并从逻辑常数转变为它们的对偶来实现对偶化。这样一来，人们就获得了一个基于反驳（= 否定证明）而不是证明的系统。这可以理解为将波普尔观点应用于证明论语义学，同时保持其直觉主义精神。形式上，它通过赋予它们证明论语义学来产生诸如对偶直觉主义逻辑之类的系统。

另一种方法是不仅将以断言为中心的证明论语义学对偶化，转而采用以否定为中心的反驳论语义学，而且将断言规则和否定规则之间的关系视为受其自身的反转原则或定义反射原则支配。这可以称为“断言-否定-和谐”原则。在标准证明论语义学中，反转原则控制断言与假设（或后果）之间的关系，而这种原则现在将规范断言与否定之间的关系。给定 A 的某些定义条件，它会说否定 A 的每个定义条件都会导致否定 A 本身。对于合取和析取，这导致了常见的断言和否定规则对

��∨���∨�∼�∼�∼(�∨�)���∧�∼�∼(�∧�)∼�∼(�∧�)

这个想法可以很容易地推广到定义反射，产生一个断言和否定交织在一起的推理系统。它与传统对立方中研究的判断形式之间的演绎关系相似（Schroeder-Heister，2012a；Zeilberger，2008）。需要强调的是，这里的否定运算符是一个表示判断形式的外部符号，而不是逻辑运算符。这特别意味着它不能被迭代。

主张和拒绝条件的想法对句子表示意义，因此对逻辑运营也是“双边主义”一词，这是一个由Rumfitt创造的术语。

进一步阅读

对于否定和拒绝的证明理论语义，拒绝参见Tranchini（2012B），Wansing（2001; 2017），以及Carrara，Chiffi和De Florio（2017）和进入的断言和拒绝的特殊问题关于否定，凯切逻辑的条目和矛盾的条目。

对于双边主义的想法，看RUMFITT（2000），Kürbis（2016; 2019），Drobyshevich（2021）以及Sara编辑的双边主义和证据理论语义的特殊问题艾汉（2023）。

对于Popperianism和证据理论语义，请参阅Binder等人。 （2022），Kapsner（2014）。

3.3在序列微积分中的和谐与反射

Gentzen的序列微积分在右侧和左引入规则之间表现出对称性，该规则建议寻找与对称性的和谐原则来说是对校对理论语义的影响。 至少有三条线条追求处理这种现象。 （i）正确介绍或或左介绍规则被认为是介绍规则。 然后使用相应的消除规则对相反的规则（分别为左介绍和右介绍）。 这意味着之前讨论的方法应用于整个顺序而不是顺序内的公式。 与这些公式不同，该顺序没有逻辑结构。 这种方法建立在定义反射上，这适用和谐和反转对任意结构化实体的规则而不是仅适用于逻辑化合物。 它已被De Campos Sanz和Piecha（2009年）追求。 （ii）右键和左介绍规则是从Došen的双线规则（第2.4节）感的表征中的表征，然后将其作为某种定义读取。 双线规则的自上而下方向已经是正确的或左侧介绍规则。 另一个可以通过某些原理从自下而上方向导出。 这是Sambin等人的基本意义成分。的基本逻辑（Sambin，Battilotti和Faggian，2000）。 （iii）右键和左引入规则被视为使用切割规则的顺序之间的相互作用。 鉴于权利或左侧规则，互补规则表明，所有与其违约的一切都与其结论所做的一切互动。 这种相互作用的想法是定义反射的广义对称原理。 它可以被认为是反演原则的概括，使用相互作用的概念而不是后果的衍生能力（参见Schroeder-Shister，2013）。 所有三种方法都适用于其经典形式的搜索结石，其中包含在Sequent的成功中的多于一个公式，包括在线性和其他逻辑中研究的结构限制版本。 因此，这一主题非常触及诸于结构逻辑和校验理论语义的子结构方法的问题（参见第3.10节）。

3.4子原子结构和自然语言

即使在定义反射中，我们也在考虑原子的定义规则，它们的定义条件通常不会分解这些原子。 więckowski（2008年; 2016; 2016; 2021）提出了一种验证理论方法，以考虑原子句子的内部结构。 他使用介绍和消除原子句子规则，其中这些原子句不仅仅将其还原到其他原子句，而是代表谓词和个人名称的含义的解剖表达式。 除了其基础意义之外，这可以被视为朝着校验理论语义的自然语言应用的第一步。 法国的进一步迈出了这方面的进一步迈出了法国，他们为几个英语碎片开发了一个校样理语学（见法国，Dyckhoff和Ben-Avi，2010; Francez和Dyckhoff，2010; Francez和Ben-Avi，2015;法国，2022年）。 具体来说，法国能够使用证明理论方法来处理范围歧义和语义意义变化的许多其他问题。 除了计算机科学外，自然语言语法和自然语言语言的语言语言将在证明理论语义的实际应用中发挥关键作用。

进一步阅读

对于自然语言的证明理论语义，请参阅法国（2015，第二部分）。