证明理论语义（完结）
有关双边主义的想法，请参见Rumfitt（2000），Kürbis（2016; 2019），Drobyshevich（2021）以及由Sara Ayhan（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-Heister，2013年）。这三种方法都适用于其经典形式的序列演算，其中可能有多个公式在序列的成功中，包括线性和其他逻辑中研究的结构限制版本。因此，该主题很大程度上涉及了副结构逻辑和证明理论语义的下结构方法的问题（请参阅第3.10节）。
3.4亚原子结构和自然语言
即使在定义反射中，我们正在考虑原子的定义性规则，它们的定义条件通常不会分解这些原子。 WięCkowski（2008; 2011; 2016; 2021）提出了一种考虑原子句子内部结构的证明理论方法。他使用原子句子的介绍和消除规则，其中这些原子句子不仅缩小到其他原子句子，而且还缩小为代表谓词和单个名称的含义的亚原子表达式。除了其基本意义外，这可以将其视为迈向证明理论语义的自然语言应用的第一步。 Francez迈出了这一方向的又一个步骤，Francez为几个英语片段开发了证明理论的语义（请参阅Francez，Dyckhoff和Ben-Avi，2010年； Francez和Dyckhoff，2010年； Francez和Ben-Avi，2015年; 2022年）。具体而言，弗朗西兹能够使用证明理论方法来应对范围歧义和许多其他语义含义变化的问题。
除了计算机科学之外，自然语言语法和自然语言语义将在证明理论语义的实际应用中发挥关键作用。
进一步阅读
有关自然语言的证明理论语义，请参阅 Francez（2015 年，第二部分）。
3.5 经典逻辑
证明论语义在直觉上是有偏见的。这是因为自然演绎作为其首选框架具有某些特征，使其特别适合直觉逻辑。在古典自然演绎中，ex falso quodlibet
⊥
�
被经典反证法规则所取代
[
�
→
⊥
]
⊥
�
在允许放电
�
→
⊥
为了推断 A，这条规则破坏了子公式原则。此外，在包含两者
⊥
和
�
→
⊥
，它在单个规则中引用两个不同的逻辑常量，因此不再存在逻辑常量的分离。最后，作为排除规则
⊥
它不遵循引入和消除的一般模式。结果，它破坏了引入形式的性质，即每个封闭推导都可以简化为在最后一步使用引入规则的推导。
经典逻辑非常适合多重后继微积分。除了直觉案例中假设的原则之外，我们不需要任何额外的原则。仅仅在后继项中承认多个公式的结构特征就足以获得经典逻辑。由于在后续微积分中存在合理的方法来在右引入和左引入之间建立和谐（参见第 3.3 节），因此经典逻辑似乎是完全合理的。然而，只有当推理被适当地构建为多重结论过程时，这才令人信服，即使这不符合我们专注于单一结论的标准实践。人们可以尝试通过论证对多个结论的推理来描绘真理所在的领域，而不是建立一个单一的命题为真，从而形成一种适当的直觉。然而，这种直觉很难维持，并且在没有严重困难的情况下无法正式捕捉。诸如 Shoesmith 和 Smiley (1978) 之类的哲学方法和诸如证明网之类的证明理论方法（参见 Girard, 1987；线性逻辑条目）都是朝这个方向的尝试。
经典逻辑引入形式属性失败的一个根本原因是析取定律固有的非决定论。
�
∨
�
可以从 A 也可以从 B 推断出。因此，如果析取律是推断的唯一方法
�
∨
�
，可导数为
�
∨
Ø
�
，这是经典逻辑的一个关键原理，将需要 A 或
Ø
�
，这是荒谬的。解决这个困难的一个方法是废除不确定性析取并使用其经典的德摩根等价物
Ø
（
Ø
�
∧
Ø
�
）
这本质上导致了没有适当析取的逻辑。在量词的情况下，也不存在适当的存在量词，如
∃
�
�
可以理解为
Ø
∀
�
Ø
�
如果一个人准备接受这一限制，那么就可以为经典逻辑制定某些和谐原则。
正如 Karl Popper 第一个观察到的那样（参见 Binder 等人，2022），经典和直觉主义连接词规则的简单组合崩溃到经典系统中。在普世主义系统中发现了以忠实方式结合古典系统和直觉系统的更复杂的理论（参见 Pimentel 和 Pereira 2021）。经典逻辑方法最初是在计算机科学中通过算法考虑而开发的，特别是在证明搜索的背景下，是米歇尔·帕里戈特（Michel Parigot）的
�
�
-微积分（Parigot 1992）以及聚焦方法在经典逻辑中的应用（Liang and Miller，2009；2024）。两种方法都基于这样的想法：通过某些索引技术，可以区分并单独处理经典序列的多公式后继中的单个公式。
进一步阅读
对于一般的经典逻辑，请参阅经典逻辑条目。
3.6 假设推理
证明理论语义的标准方法，特别是 Prawitz 的基于有效性的方法（第 2.2.2 节），以封闭推导为基础。开放推导的有效性被定义为从假设的封闭推导到断言的封闭推导的有效性传递，其中后者是通过用封闭推导代替开放假设而获得的。因此，如果人们将封闭推导称为“绝对推导”，将开放推导称为“假设推导”，那么我们可以将这种方法描述为以下两个基本思想：（I）绝对推导相对于假设的首要性，（II）结果的传递观。这两个假设（I）和（II）可以被视为标准语义的教条。这里的“标准语义”不仅指标准证明理论语义，还指经典模型理论语义，其中也假设了这些教条。我们从真理的定义开始，真理是范畴概念，而结果是假设的概念，是真理从条件到结果的传递。从这个角度来看，构造语义学，包括证明理论语义学，将真理的概念与构造或证明的概念交换，并根据构造函数或过程解释“传输”，但在其他方面保持框架不变。
这些教条原则上并没有什么问题。然而，也存在一些在标准框架内难以处理的现象。这种现象是无根据的，尤其是循环性，如果没有传递真理和可证明性，我们可能会产生后果（参见第 3.8 节）。另一个现象是子结构的区别，从一开始就包括假设的结构是至关重要的（见 3.10 节）。此外，最重要的是，我们可能会以某种方式定义事物，而事先不知道我们的定义或定义链是否有充分依据。我们并不首先对我们开始的定义进行元语言研究，而是想立即开始推理。如果我们将自己限制在逻辑常量的情况下，那么这个问题就不会出现，因为逻辑常量的定义规则基本上是有根据的。但当我们考虑超出逻辑常数的更复杂的情况时，问题立即出现。
这使得值得朝另一个方向前进并从后果的假设概念开始，即直接表征后果而不将其还原为绝对情况。从哲学上讲，这意味着范畴概念是假设概念的限制性概念。在经典情况下，真理将是结果的限制情况，即没有假设的结果。该程序与分类证明理论的方法密切相关（参见第 2.5 节），该方法基于假设实体（“箭头”）的首要地位。形式上，它会优先考虑顺序演算而不是自然演绎，因为顺序演算允许通过左引入规则来操纵序列的假设侧。在术语注释系统中，我们不会注释公式，而是通过术语注释假设陈述。如果假设陈述由以下形式的序列表示
�
⊢
�
，我们不会将其注释为
�
：
�
⊢
�
（
�
）
：
�
就像库里-霍华德的信件一样，但以某种方式
�
：
（
�
⊢
�
）
也就是说，完整的假设陈述将被注释，这使得与分类方法平行，其中 f 是箭头
�
：
�
→
�
，明显的。
进一步阅读
对于假设推理和内涵证明理论语义，请参阅 Došen (2003; 2016) 和 Schroeder-Heister (2012c, 2016)。
3.7 内涵证明理论语义
正如第一节（1.1）中提到的，证明理论语义在精神上是内涵的，因为它感兴趣的是证明而不仅仅是可证明性。对于证明理论语义来说，它不仅与 B 是否源自 A 相关，而且还与我们如何确定 B 源自 A 相关。换句话说，证明的同一性是一个重要问题。然而，尽管这是表面上显而易见的，并且证明论语义学家通常会同意这种抽象主张，但证明论语义学的实践往往是不同的，并且证明的同一性主题被严重忽视。经常会出现同样有效的规则被确定的情况。例如，当讨论和谐原则时，人们会考虑连词的标准引入规则
�
�
�
∧
�
许多证明论语义学家会认为是否选择一对投影无关紧要
�
∧
�
�
�
∧
�
�
或一对
�
∧
�
�
�
∧
�
�
�
作为合取的消除规则。第二对规则通常被认为是这对投影的更复杂的变体。然而，从内涵上看，这两对规则并不完全相同。识别它们对应于识别
�
∧
�
和
�
∧
（
�
→
�
）
，这只是外延上的正确，但内涵上并不正确。正如 Došen 经常争论的那样（例如，Došen 1997；2006），诸如
�
∧
�
和
�
∧
（
�
→
�
）
是等价的，但不是同构的。这里的“同构”是指当用一个公式证明另一个公式时，反之亦然，通过组合这两个证明，我们获得了身份证明。本例中情况并非如此。
追求这个想法会导致与标准原则不同的和谐与反转原则。由于和谐和倒置是证明论语义的核心，因此它的许多问题都受到了影响。认真对待内涵性主题意味着重塑证明理论语义学的许多领域（参见 Schroeder-Heister，2022）。这对各个邻近领域（例如悖论的处理）产生了影响。 Tranchini (2023) 撰写了第一本关于内涵证明理论语义学的专着，特别强调悖论主题。
由于证明的同一性是分类证明理论的基本主题（参见第 2.5 节），因此与目前的情况相比，后者在证明理论语义方面需要更多的关注。
3.8. 悖论
逻辑、数学和语义悖论在逻辑和数学哲学中发挥着至关重要的作用，在证明论语义学的框架中得到了新颖的呈现。如果在引入和消除规则的背景下制定悖论，则可以将证明约简的证明理论机制应用于它们。假设集合项的引入和消除规则如下（在一种朴素集合论中）：
�
（
�
）
�
ε
{
�
：
�
（
�
）
}
�
ε
{
�
：
�
（
�
）
}
�
（
�
）
那么，对于 r 作为
{
�
：
�
∉
�
}
，我们可以推断
�
ε
�
从
�
∉
�
反之亦然，这是罗素悖论的自然演绎变体。现在，普拉维茨（Prawitz，1965，附录 B）观察到，罗素悖论所产生的荒谬性的推导是不可正常化的，坦南特（Tennant，1982）能够在大量悖论中证明这一特征。从证明理论语义的角度来看，不可规范化的证明很可能被认为是无效的，至少在可规范化证明有效的意义上是无效的。这意味着我们获得了一个证明论标准来判断我们是否有有意义的证明，而悖论的证明在这个意义上将没有意义。普拉维茨-坦南特对悖论的分析开辟了悖论证明论的领域，它远远超出了狭义上的证明论语义。它与内涵性方面（见3.7节）以及定义反射的思想密切相关（见2.3.2节和定义反射与悖论的补充）。
从证明理论语义学的角度来看，一个特别有趣的悖论是埃克曼悖论。它是用最小命题逻辑编纂罗素悖论的蕴涵变体的结果。事实证明，根据如何表述绕行推导的减少，最小命题逻辑中的某些推导是不可规范化的。这有力地阐明了证明约简的概念，这在自然演绎风格的证明理论语义中是绝对必要的：很大程度上取决于它的仔细定义。事实上，证明约简的概念构成了证明同一性的概念，远远超出了消除证明中“弯路”的外延思想。
进一步阅读
对于罗素悖论的一般情况，请参阅罗素悖论的条目。
关于证明理论语义中悖论的处理，包括埃克曼悖论，请参见 Tranchini (2023)。
3.9 约简、博弈论和对话
演绎是前向的，通过合理的规则从已经建立的句子传递到进一步的句子，而还原则是向后进行的，试图为给定的主张找到论据。因此它属于证明搜索。计算机科学中已经发现并讨论了各种证明搜索方法：解析和表格系统就是突出的例子。然而，从语义的角度来看，还原方法在概念上并不仅次于演绎，而是本身就是理论。人们甚至可能认为，从语义的角度来看，还原方法是主要的，因为对论证的搜索或搜索它的可能方式构成了给定主张的含义。例如，这个想法已被采用在对话或博弈论语义中，但通常可以而且应该被纳入证明论语义中。这是证明论语义学的一个主要需求，迄今为止，证明论语义学主要基于演绎而不是还原。
进一步阅读
有关还原逻辑的思想及其语义，请参阅 David Pym 和 Eike Ritter (2004) 的专着。
对于对话逻辑，请参阅对话逻辑条目以及托马斯·皮查 (Thomas Piecha) 的对话逻辑条目，互联网哲学百科全书。
对于逻辑中的博弈论方法，请参阅逻辑和博弈条目。
3.10 底层方法
一旦人们在后续微积分的框架中处理证明论语义，从而关注假设而不是绝对主张，具有受限结构规则的逻辑领域（称为“子结构逻辑”）就需要语义考虑。在这里，假设被引入并保留在话语中的方式代表了比自然演绎中的假设更细粒度的结构，在自然演绎中，它们通常被认为是陈述集。由于以类似方式构造后继词的可能性，证明论语义学失去了其直觉主义偏见，但不一定成为经典。在子结构逻辑的框架内，可以轻松地对相关逻辑或资源敏感逻辑等异常逻辑系统进行建模。一个特别有趣的主题是捆绑含义的逻辑，它区分不同但共存的构建假设和结论的方式（参见 Pym，2002）。子结构逻辑是公认的通用工具，用于在单一的包罗万象的结构框架内描述逻辑系统。子结构逻辑是否代表语义框架仍然是一个悬而未决的问题。
进一步阅读
对于一般的子结构逻辑，请参阅子结构逻辑条目。
4 结论与展望
标准证明理论语义实际上完全被逻辑常数占据。逻辑常量在推理和推理中发挥着核心作用，但绝对不是唯一的，甚至可能不是可以推理定义的最典型的实体类型。需要一个框架来处理更广泛意义上的推理定义，并涵盖逻辑和超逻辑推理定义。关于任意定义规则的定义反射的想法（参见第 2.3.2 节）以及自然语言应用（参见第 3.4 节）都指向这个方向，但可以想象更深远的概念。此外，对和谐、倒置原理、定义反射等的关注有些误导，因为它可能表明证明论语义仅由这些组成。应该强调的是，当涉及到算术时，除了求逆之外，还需要更强大的原理。然而，尽管存在这些限制，证明理论语义学已经取得了非常实质性的成就，可以与更广泛的语义学方法竞争。
进一步阅读
有关证明理论语义学各个方面的贡献，请参见 Piecha 和 Wehmeier 编辑的读者（2024 年，开放获取）。
