证明论语义学（五）

3.5古典逻辑

证明理论语义是直观的偏见。 这是由于自然扣除作为其优选框架的事实具有一定的特征，使其特别适合直观逻辑。 在古典自然扣除ex falso quodlibet

⊥�

被典型的索赔副本替换为荒谬的规则

[�→⊥]⊥�

在允许放电�→⊥以便推断出来，这条规则破坏了模子原则。 此外，在包含两个和�→⊥中，它是指单个规则中的两个不同的逻辑常数，因此不再有逻辑常数的分离。 最后，作为⊥的淘汰规则，它不会遵循介绍和消除的一般模式。 因此，它会破坏引入表单属性，即每个封闭的推导都可以减少到在最后一步中使用引入规则的一个。

古典逻辑与多功能连续的序列微积分非常吻合。 在那里，我们不需要任何其他原则，超出直觉案件中的假设。 只是在成功中录取多个公式的结构特征就足以获得经典逻辑。 由于有合理的方法来在序列微积分中的右介绍和左引入之间建立和谐（参见第3.3节），古典逻辑似乎是完全合理的。 但是，如果推理被适当地被诬陷为多个结论过程，这只是令人信服，即使这与我们关注单一结论的标准做法，即使这与我们的标准做法相符合。 人们可以试图通过争论推理对多个结论的推理来发展适当的直觉，描绘了真理的区域而不是建立一个命题为真实。 然而，这种直觉难以维持，不能在没有严重困难的情况下正式捕获。 鞋匠和笑脸（1978年）和思考的哲学方法，以及证明网等校样方法（参见Girard，1987;线性逻辑的条目）是在此方向的尝试。

在古典逻辑中介绍形式财产失败的根本原因是脱位法律固有的不确定主义。 �∨�可以从A以及B.因此，如果分离法是推断�∨�的唯一方法，则�∨¬�的衍生能力是古典逻辑的关键原则，将需要一个或¬�荒谬。 出种这种困难的方式是废除不确定的分离和使用，而不是其经典的de摩根等效物¬（¬�∧¬�）。 这基本上导致逻辑而没有适当的分离。 在量化的情况下，没有正确的存在量化，也没有，因为在¬∀�¬�的意义上会被理解。 如果准备接受这种限制，那么可以为古典逻辑配制某些和谐原则。

随着Karl Popper是第一个观察的（见Binder等，2022），古典和直觉连接的简单组合折叠到经典系统中。 以忠诚的方式结合经典和直觉系统的更复杂的理论是在Ecumenical Systems（参见Pimentel和Pereira 2021）中。 通过算法考虑最初在计算机科学中开发的古典逻辑的方法，特别是在证明搜索的上下文中，是Michel Parigot的��微分（Parigot 1992）以及将聚焦方法的应用到古典逻辑（梁和米勒，2009; 2024）。 两种方法都接近了通过某些索引技术，可以单独地区分和处理多种公式中的单个公式成功中的单个公式。

进一步阅读

对于古典逻辑，一般看古典逻辑的条目。

3.6 假设推理

证明论语义学的标准方法，尤其是 Prawitz 的基于有效性的方法（第 2.2.2 节），以封闭推导为基础。开放推导的有效性被定义为有效性从假设的封闭推导传递到断言的封闭推导，后者是通过将封闭推导替换为开放假设而获得的。因此，如果将封闭推导称为“范畴的”，将开放推导称为“假设的”，则可以将这种方法描述为以下两个基本思想：（I）范畴优先于假设，（II）结果传递观。这两个假设（I）和（II）可以看作是标准语义学的教条。这里的“标准语义学”不仅指标准证明论语义学，也指经典的模型论语义学，这些教条也是假设的。在那里，我们从真理的定义开始，真理是范畴概念，并将后果，假设概念，定义为真理从条件到结果的传递。从这个角度来看，构造语义学，包括证明论语义学，用构造或证明的概念来交换真理的概念，并根据构造函数或程序来解释“传递”，但除此之外，框架保持不变。

这些教条在原则上没有错。然而，有些现象在标准框架中很难处理。这种现象是无根据的，特别是循环性，我们可能会在没有真理和可证明性传递的情况下得到后果（见第 3.8 节）。另一种现象是子结构区别，从一开始就包括假设的结构化至关重要（见第 3.10 节）。此外，这是最关键的，我们可能会以某种方式定义事物，而事先并不知道我们的定义或定义链是否有根据。我们不会首先参与到我们开始的定义的元语言研究中，而是想立即开始推理。如果我们将自己限制在逻辑常数的情况中，则不会出现此问题，因为其中定义规则是显而易见的。但是，当我们考虑超出逻辑常数的更复杂情况时，问题就会立即出现。

这使得值得朝另一个方向继续前进并从假设的结果概念开始，即直接描述结果而不将其简化为范畴情况。从哲学上讲，这意味着范畴概念是假设概念的限制概念。在经典情况下，真理将是结果的极限情况，即没有假设的结果。该程序与范畴证明理论的方法（见第 2.5 节）密切相关，该方法基于假设实体（“箭头”）的首要性。形式上，它会优先考虑序列演算而不是自然演绎，因为序列演算允许通过左引入规则来操纵序列的假设方。在带术语注释的系统中，我们不会注释公式，而是用术语注释假设陈述。如果假设陈述以形式 �⊢� 的序列表示，我们不会像在 Curry-Howard 对应关系中那样将其注释为 �:�⊢�(�):�，而是以 �:(�⊢� 的方式注释。也就是说，完整的假设陈述将被注释，这使得与范畴方法的相似性显而易见，其中 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) 能够证明这一特性适用于大量悖论。从证明论语义学的角度来看，不可规范化的证明很可能被视为无效，至少在可规范化证明有效的意义上无效。这意味着我们获得了一个证明论标准来判断我们是否有有意义的证明，而悖论的证明在这个意义上是没有意义的。Prawitz-Tennant 对悖论的分析开辟了悖论证明理论的领域，它远远超出了狭义的证明论语义学。它与内涵性方面（见第 3.7 节）以及定义反思的概念密切相关（见第 2.3.2 节和关于定义反思和悖论的补充）。

从证明理论语义学的角度来看，一个特别有趣的悖论是埃克曼悖论。 它源于在最小命题逻辑中编纂罗素悖论的隐含变体。 事实证明，取决于绕道导数的约简是如何制定的，最小命题逻辑中的某些导数是不可归一化的。 这有力地阐明了证明约简的概念，这在自然演绎风格证明理论语义学中是绝对必要的：这在很大程度上取决于其仔细的定义。 事实上，证明简化的概念构成了证明身份的概念，远远超出了证明中的“绕道”被删除的扩展概念。

延伸阅读

关于罗素悖论，请参阅罗素悖论的条目。

关于证明理论语义学中悖论的处理，包括埃克曼悖论，见Tranchini (2023)。

3.9还原、博弈论和对话

虽然扣除是前向的，但通过合理的规则从已经建立的句子传递到进一步的句子，扣除向后进行，试图为给定的索赔寻找论据。 因此，它属于证明搜索。 在计算机科学中已经发现并讨论了各种证明搜索方法：分辨率和图表系统是突出的例子。 然而，从语义学的角度来看，还原方法在概念上并不次于演绎，而是理论本身。