证明论语义学（三）
进一步阅读：
有关一般的逻辑连接词，请参阅形式逻辑中的句子连接词条目。
有关倒置原则，请参阅 Schroeder-Heister (2007)。
有关证明论和谐的变体，请参阅 Francez (2015)、Schroeder-Heister (2016) 和 Tranchini (2023)。
2.2.2 证明论有效性
证明论有效性是证明论语义学的主要方法。作为一个技术概念，它是由 Prawitz (1971; 1973; 1974) 开发的，它将基于 Tait (1967) 的思想的证明理论有效性概念（最初用于证明强规范化）转变为语义概念。Dummett 为这一概念提供了许多哲学基础（参见 Dummett，1991）。主要有效的对象是作为论证表示的证明。在次要意义上，如果单个规则从有效证明引出有效证明，则它们可以是有效的。从这个意义上讲，有效性是一个全局概念，而不是局部概念。它适用于给定原子系统上的任意推导，它定义了原子的可推导性。如果证明在最后一步使用引入规则，则称其为规范证明，证明理论有效性基于以下三个思想：
封闭规范证明的优先级。
将封闭的非规范证明简化为规范证明。
开放证明的替代观点。
补充 1：有效性的定义基于 Gentzen 的观点，即引入规则是“自我证明的”，并赋予逻辑常数其含义。这种自我证明特性只用于封闭式证明，封闭式证明被认为是比开放证明更主要的。
补充 2：非规范证明通过将其简化为规范证明来证明其合理性。因此，在规范化证明中使用的简化程序（绕道简化）起着至关重要的作用。由于它们证明了论证的合理性，因此 Prawitz 也将它们称为“合理性”。这个定义同样仅适用于封闭式证明，对应于自然演绎中封闭式正则推导的引入形式属性（参见第 1.3 节）。
补充 3：开放证明通过考虑其封闭实例来证明其合理性。这些封闭实例是通过用它们的封闭证明替换它们的开放假设，用封闭项替换它们的开放变量而获得的。例如，如果用 A 的封闭有效证明替换开放假设 A 而获得的每个封闭证明都是有效的，则 A 的 B 证明被认为是有效的。这样，开放假设被认为是封闭证明的占位符，这就是为什么我们可以说开放证明是一种替代解释。
这产生了以下证明理论有效性的定义：
底层原子系统中的每个封闭证明都是有效的。
如果其直接子证明有效，则封闭规范证明被认为是有效的。
如果封闭非规范证明简化为有效的封闭规范证明或原子系统中的封闭证明，则被认为是有效的。
如果通过用封闭的有效证据替换其开放假设而获得的每个封闭式证明，则视证明是有效的。
正式地，该定义必须依赖于考虑的原子系统（参见第2.6节），以及一组可用的理由（证明减少）。 此外，此外，证明在这里被理解为普拉威茨术语中的有效证明的候选者（“争论”的术语），这意味着它们由组成的规则不是固定的。 它们看起来像证明树，但他们的个别步骤可以有一个任意（有限）的罚款，可以消除任意假设。 有效性的定义单独出现在给定的减少程序的基础上是“真实”证明的证明结构。
可以将关于原子系统的各种选择的有效性被视为逻辑有效性的广义概念。 实际上，如果我们考虑直觉逻辑的标准缩短，那么直觉逻辑中的所有导出都与所考虑的原子系统无关。 这是语义正确性。 我们可能会询问匡威是否持有，viz。 无论是对每个原子系统有效的任何证据，直觉逻辑都存在相应的推导。 在这种意义上完整的直觉逻辑被称为普拉威茨的猜想（参见Prawitz，1973; 2013）。 对于超越伸展逻辑的系统，存在某些疑问的疑虑。 无论如何，它将取决于有效性概念的精确制定，特别是在其处理原子系统（见第2.8节）。
有关展示有效性的更正式的定义和详细示例，以及关于普拉维茨的猜想的一些评论
证明理论有效性的例子补充。
进一步阅读：
详细阐述了普拉维茨证明理论有效性的进一步发展，特别是他的理由理论，见Piccolomini D'Aragona（2023）。
对于证明理论有效性的计算解释作为战术证明的方法，请参阅Gheorghiu和Pym（2022，其他互联网资源）。
2.2.3建设性型理论
Martin-Löf的类型理论（Martin-Löf，1984）是建设性逻辑和数学的主要方法。 哲学上，它与普拉维茨股份股份标准证明理论语义的三个基本假设，第2.2.2节：封闭式规范证明的优先级，减少了封闭的非规范证明对规范的证据和替代打开证明的视图。 然而，Martin-löf的类型理论至少具有两个特征，超出了校验理论语义的其他方法：
证明对象的思考和证明和校样之间的相应区别。
形成规则视图为校对系统的内在，而不是外部规则。
第一个想法返回咖喱霍华德信函（参见De Groote，1995;Sørensen和urzyczyn，2006），这是公式A具有某种证据的事实可以被编写编码，因为某个术语T是类型A的事实，由此通过类型A识别公式A.这可以在型分配的微积分中正式化，其语句是�：�的陈述。 在这个系统中的证据可以阅读，可以阅读，表明T是A. Martin-löf（1995; 1998年）的证据，以通过以下方式区分这两倍的证据感。 首先，我们有表单的陈述�：�。 这些陈述称为判决，他们的证据称为演示。 在此类判决中，术语T表示命题A的证据A.后一个意义上的证据也称为证明对象。 在演示判断时：�，我们证明T是命题A的证据（对象）。在这个双层系统中，演示层是参数层。 与证明对象不同，示威性具有认识意义; 他们的判断携带分组力量。 证明层是解释含义的层：通过讲述作为证明（物体）的验证（对象）来解释命令A的含义。在规范和非规范证据之间的区别是在命题的区别而不是判断层。 这意味着某种明确要求。 当我证明了一些东西时，我不仅可以在我的验证中对我的证明有理由，因为在普拉威茨的有效性的概念中，但同时必须确定这条司法符合其目的。 这一确定性通过示范保证。 在数学上，这两个折叠的证据感仅在类型可以取决于术语时才开发它的真实功率。 依赖类型是马丁-LÖF的理论和相关方法的基本成分。
第二个想法使Martin-Löf的方法与所有其他验证理论有效性的定义相差。 例如，至于普拉维茨的程序的关键差异是它在特征中不是金属语言，其中“金属语言”是指首先指定证据和证据的命题和候选者，然后通过在Metalangage中的定义来确定，它是固定的，它是有效的哪些不是。 相反，命题和证据仅在示威范围内发挥作用。 例如，如果我们假设某些东西是一个暗示的证据�→�，我们不必表明A和B都是完全良好的命题，但除了了解A是一个命题之外，我们只需要知道B是一个命题提供了一个已被证明。 作为一个命题是由特定形式的判断表示，该判决是在相同的示范系统中建立，该系统用于建立一个命题证明的证据。
在马丁-Löf的理论中，证明理论语义接收了强烈的本体组成部分。 最近的辩论涉及证明对象是否具有纯粹的本体状况或者是否编纂知识，即使它们不是事实的行为。 最近，Martin-Löf已经嵌入了他的方法，进入了主张，挑战和义务之间的互动理论（Martin-Löf2019），它给出了他的证据理论语义是一个务实的方面，也将它与对话语义相关联（见第3.9节）。
Martin-Löf的类型理论已经发现了其在同型理论中最重要的数学应用，导致同型型理论（HOTT）和单价基础计划（单价基础计划2013）。 后者往往（有时争议）被认为是一种在直觉精神中的新的数学的新颖性方法，作为古典集理方法的替代方案。
进一步阅读：
对于Martin-Löf的历史和哲学的理论，看Sommaruga（2000）。 对于类型理论，一般来说，对于同型型理论，以及为单价基础计划，请参阅直觉类型理论的条目和类型理论的条目。
2.3 子句定义和定义推理
证明论语义学通常关注逻辑常数。这一关注点实际上从未受到质疑，显然是因为它被认为是显而易见的。在证明论中，很少有人关注原子系统，尽管有 Lorenzen 的早期工作（见第 2.1.1 节），其中逻辑规则的论证嵌入在任意规则理论中，以及 Martin-Löf (1971) 的迭代归纳定义理论，其中提出了原子公式的引入和消除规则。逻辑编程的兴起拓宽了这一视角。从证明论的角度来看，逻辑编程是一种关于原子子句定义的原子推理理论。定义反射是一种证明论语义学方法，它接受了这一挑战并试图建立一种应用范围超越逻辑常数的理论。
2.3.1 来自逻辑编程的挑战
在逻辑编程中，我们处理的是形式为
�⇐�1,…,��
的程序子句，它们定义原子公式。此类子句可以自然地解释为描述原子的引入规则。从证明论语义的角度来看，以下两点至关重要：
(1) 逻辑复合公式的引入规则（子句）在原则上与原子的引入规则（子句）没有区别。从证明论的角度解释逻辑编程促使将证明论语义扩展到任意原子，从而产生具有更广泛应用领域的语义。
(2) 程序子句不一定有理有据。例如，子句的头部可能出现在其主体中。有理有据的程序只是一种特殊的程序。在逻辑编程中使用任意子句而不需要进一步的要求是追求证明论语义中相同想法的动机。人们会承认任何类型的引入规则，而不仅仅是特殊形式的规则，特别是不一定是那些有充分根据的规则。这将定义自由的思想（逻辑编程的基石）带到了语义学中，再次扩大了证明论语义学的应用范围。
将引入规则视为原子的意义赋予规则的想法与一般形式的归纳定义理论密切相关，根据该理论，归纳定义是规则系统（参见 Aczel，1977）。
2.3.2 定义反射
定义反射理论（Hallnäs，1991；2006；Hallnäs 和 Schroeder-Heister，1990/91；Schroeder-Heister，1993）接受了逻辑编程的挑战，并给出了证明论语义，不仅针对逻辑常量，而且针对可以给出子句定义的任意表达式。正式地，这种方法从子句列表开始，该列表是所考虑的定义。每个子句的形式为
�⇐Δ
其中头部 A 是原子公式（原子）。在最简单的情况下，主体 Δ 是原子列表 �1,…,��，在这种情况下，定义看起来像一个确定的逻辑程序。我们经常考虑一种扩展情况，其中 Δ 还可能包含一些结构蕴涵“⇒”，有时甚至包含一些结构全称量化，这本质上是通过限制替换来处理的。如果 A 的定义具有以下形式
�� {�⇐Δ1⋮�⇐Δ�
则 A 具有以下引入和消除规则
Δ1�⋯Δ���[Δ1]�⋯[Δ�]��
引入规则，也称为定义闭包规则，表达“沿着”子句的推理。消去规则被称为定义反射原理，因为它反射的是整个定义。如果Δ1，…，Δ�穷尽了根据给定定义生成A的所有可能条件，并且每个条件都包含同一个结论C，则A本身包含这个结论。如果将子句定义视为归纳定义，则该原理可视为表达归纳定义中的极值子句：除了给定的子句之外，没有其他任何东西可以定义A。显然，定义反射是所讨论的反转原理的一种广义形式。它在具有超越纯命题推理的自由变量的定义情境中，以及在非良基情境中发挥其真正的威力。一个非充分依据定义的例子是原子 R 通过其自身的否定进行定义：
��{�⇐(�⇒⊥)
通过否定来定义原子是逻辑编程中的一个标准示例。在定义反射的上下文中，它是由 Hallnäs 提出的。在定义反射和悖论补充中对此进行了详细讨论。
进一步阅读：
有关非充分依据和悖论，请参阅自指条目和罗素悖论条目。
2.4 逻辑常数的结构特征
关于所谓的逻辑常数的“结构特征”，存在大量的想法和结果，其中“结构”在这里既指证明理论意义上的“结构规则”，也指具有特定结构的框架，其中该框架再次被证明理论地描述。其中一些作者使用语义词汇，至少隐含地暗示他们的主题属于证明论语义学。其他人则明确否认这些内涵，强调他们对确定常数逻辑性的特征感兴趣。即使常数本身的语义是真值条件的，也可以用证明论术语来回答“什么是逻辑常数？”这个问题：即要求（可能是真值条件定义的）常数表现出可以用证明论术语描述的某种推理行为。然而，由于一些作者同时将其特征视为语义，因此我们在这里提到其中一些方法是恰当的。
关于逻辑常数，最直言不讳的结构主义者是科斯洛，他明确地将自己理解为逻辑常数。在他的《结构主义逻辑理论》（1992）中，他发展了一种逻辑常数理论，其中他用某些“蕴涵关系”来描述它们，其中蕴涵关系大致对应于塔斯基意义上的有限后果关系（这又可以通过序列式系统的某些结构规则来描述）。科斯洛发展了一种精确的元数学意义上的结构理论，它没有以任何方式指定给定公理之外的对象域。如果给出了一种具有蕴涵关系的语言或任何其他对象域，则可以使用结构方法通过检查其蕴涵属性来挑选出逻辑化合物。
在他早期关于逻辑基础的论文中，波普尔（1947a；1947b；Binder 等人，编辑，2022）用证明理论术语给出了逻辑常数的推理特征。他使用序列演算，并用某些可导性条件来描述逻辑常数。他的术语清楚地表明，他想要的是逻辑常数的证明论语义，因为他谈到了“推理定义”和通过以所述方式定义常数而实现的“数理逻辑的琐碎化”。虽然他的陈述并非没有概念上的不精确和错误，但他预见了许多现在在证明论语义中常见的思想，例如通过引入或消除规则的某些最小或最大条件来描述逻辑常数。
Kneale (1956) 和 Hacking (1979) 对逻辑性争论做出了重要贡献，他们用序列演算规则来推理性地描述逻辑常数。Došen (1980; 1989) 在他的理论中提出了对逻辑性的全面解释，他将逻辑常数视为“标点符号”，在逻辑层面上表达结构特征。他认为逻辑常数遵循某些双线规则，这些规则可以双向读取。例如，合取和析取遵循（在经典逻辑中，具有多个公式后继）双线规则
=Γ⊢�∧�,ΔΓ⊢�,ΔΓ⊢�,Δ=Γ,�∨�⊢ΔΓ,�⊢ΔΓ,�⊢Δ
Došen 能够给出包括模态逻辑系统在内的表征。他明确地认为他的工作是对逻辑性争论的贡献，而不是对任何证明论语义学概念的贡献。Sambin 等人在他们的《基本逻辑》（Sambin、Battilotti 和 Faggian，2000 年）中明确地将 Došen 所称的双线规则理解为基本含义赋予规则。合取和析取的双线规则被解读为这些常量的隐式定义，通过某种程序可以将其转化为我们习惯的显式顺序式规则。因此，Sambin 等人使用与 Došen 相同的出发点，但不是将其解释为常量行为的结构描述，而是在语义上将其解释为它们的隐式定义。
