证明理论语义（二）
2.2 基于引入规则的推导语义
2.2.1 反转原理与和谐
在他的《逻辑演绎研究》中，根岑对自然演绎中引入推论和消除推论之间的语义关系做出了一些（经常被引用的）纲领性评论。
可以说，引入代表了相关符号的“定义”，而归根结底，删除只不过是这些定义的结果。这个事实可以表达如下：在消除一个符号时，我们可以使用我们仅处理“在引入该符号所提供的意义上”的终结符号的公式。 （根岑，1934/35，第 80 页）
当然，这并不意味着消除规则可以从字面意义上的引入规则推导出来。事实上，他们不是。这只能意味着他们可以以某种方式为他们辩护。
通过使这些想法更加精确，应该可以根据某些要求将 E 推理显示为其相应 I 推理的独特函数。 （同上，第 81 页）
因此，Gentzen 程序的基本思想是，我们以引入规则和某种语义推理的形式拥有“定义”，通过使用“某些要求”来验证消除规则。
通过采用 Lorenzen 的术语并使其基本思想（见第 2.1.1 节）适应自然演绎的背景，Prawitz（1965）制定了一个“反演原理”，使 Gentzen 的言论更加精确：
让
�
是结果为 B 的消除规则的应用。然后，满足导出大前提的充分条件的推论
�
，当与小前提的扣除相结合时
�
（如果有的话），已经“包含”B的扣除；因此，B 的扣除可以直接从给定的扣除中获得，无需添加
�
。 （第 33 页）
这里充分条件由相应引入规则的前提给出。因此，反演原理说，如果在最后一步中使用引入规则导出了消除规则的主要前提，则无需应用消除规则即可推导消除规则的结论，这意味着组合
⋮
�
I-推理
{
�
�
}
�
电子推理
步骤，其中
{
�
�
}
代表小前提的推导列表（可能为空），可以避免。
引入规则和消除规则之间的关系通常被描述为“和谐”（Dummett 1973，第 396-397 页），或受“和谐原则”支配（Tennant，1978，第 74 页）。这个术语并不统一，有时甚至不完全清楚。它本质上表达了“反转”的含义。即使“和谐”是一个暗示对称关系的术语，它也经常被理解为表达基于引入规则的概念，例如 Read 的（2010）“一般消除和谐”（尽管偶尔包括基于消除的概念，如出色地）。有时，和谐应该意味着连接词在某种意义上是最强的或最弱的，考虑到它们的引入或消除规则。这个想法是 Tennant（1978）和谐原则以及 Popper 和 Koslow 结构特征的基础（见 2.4 节）。倒装原则中提出的引入和消除规则之间的具体关系排除了所谓的推论定义，例如连接词的定义，它结合了析取的引入规则和合取的消除规则，并且引起了仍在持续的争论关于推理定义的格式。和谐的形式表征使用了将推理规则翻译为二阶命题逻辑（吉拉德系统 F），并已成为内涵证明理论语义学的中心主题（Tranchini，2023）。
进一步阅读：
对于一般的逻辑连接词，请参阅形式逻辑中的句子连接词条目。
有关反演原理，请参见 Schroeder-Heister (2007)。
有关证明理论和谐的变体，请参阅 Francez (2015)、Schroeder-Heister (2016) 和 Tranchini (2023)。
2.2.2 证明理论有效性
证明理论有效性是证明理论语义学的主要方法。作为一个技术概念，它是由 Prawitz (1971; 1973; 1974) 开发的，通过将基于 Tait (1967) 思想的证明理论有效性概念转变为语义概念，最初用于证明强规范化。达米特为这一概念提供了很多哲学基础（参见达米特，1991）。主要有效的对象是作为参数表示的证明。从次要意义上讲，如果单个规则从有效证明引向有效证明，则它们可以是有效的。从这个意义上说，有效性是一个全球性的概念，而不是一个局部性的概念。它适用于给定原子系统的任意推导，它定义了原子的可导性。如果一个证明在最后一步中使用了引入规则，则证明理论的有效性基于以下三个想法：
封闭规范证明的优先级。
将封闭的非规范证明简化为规范证明。
开放证明的替代观点。
广告 1：有效性的定义基于 Gentzen 的思想，即引入规则是“自我证明的”并赋予逻辑常量其含义。这种自我证明功能仅用于封闭式证明，封闭式证明被认为是开放式证明的主要证明。
广告 2：通过将非规范证明简化为规范证明来证明其合理性。因此，归一化证明中使用的缩减程序（迂回缩减）起着至关重要的作用。由于它们为论证辩护，普拉维茨也将它们称为“理由”。这个定义同样只适用于封闭证明，对应于自然演绎中封闭正规推导的引入形式性质（见1.3节）。
广告 3：通过考虑其封闭实例来证明开放证明的合理性。这些封闭实例是通过用它们的封闭证明替换它们的开放假设以及用封闭项替换它们的开放变量来获得的。例如，如果通过用 A 的封闭有效证明替换开放假设 A 获得的每个封闭证明都是有效的，则 A 的 B 证明被认为是有效的。这样，开放假设被认为是封闭证明的占位符，这就是为什么我们可以谈论开放证明的替代解释。
这产生了以下证明理论有效性的定义：
底层原子系统中的每个封闭证明都是有效的。
如果封闭式规范证明的直接子证明有效，则该证明被认为是有效的。
如果封闭的非规范证明简化为有效的封闭规范证明或原子系统中的封闭证明，则该证明被认为是有效的。
如果通过用封闭有效证明替换其开放假设而获得的每个封闭证明以及用封闭项替换其开放变量都是有效的，则开放证明被认为是有效的。
形式上，这个定义必须相对于所考虑的原子系统（参见第 2.6 节），以及一组可用的理由（证明简化）。此外，这里的证明被理解为有效证明的候选者（Prawitz 术语中的“论证”），这意味着组成它们的规则不是固定的。它们看起来像证明树，但它们的各个步骤可以具有任意（有限）数量的前提，并且可以消除任意假设。有效性的定义在给定的简化程序的基础上挑选出了那些“真实”证明的证明结构。
原子系统的每个选择的有效性可以被视为逻辑有效性的广义概念。事实上，如果我们考虑直觉逻辑的标准约简，那么直觉逻辑中的所有推导都是有效的，独立于所考虑的原子系统。这是语义上的正确性。我们可能会问相反的情况是否成立，即。是否对于任何对每个原子系统有效的证明，在直觉逻辑中都存在相应的推导。直觉逻辑在这个意义上是完整的，被称为普拉维茨猜想（见普拉维茨，1973；2013）。对于超越蕴涵逻辑的系统，这个猜想的有效性存在一定的疑问。无论如何，这将取决于有效性概念的精确表述，特别是它对原子系统的处理（参见第 2.8 节）。
有关更正式的定义和证明有效性的详细示例，以及对普拉维茨猜想的一些评论，请参阅
证明理论有效性示例的补充。
进一步阅读：
有关普拉维茨证明理论有效性理论的进一步发展的详细阐述，特别是他的理由理论，请参阅 Piccolomini d’Aragona (2023)。
有关证明理论有效性作为战术证明方法的计算解释，请参阅 Gheorghiu 和 Pym（2022 年，其他互联网资源）。
2.2.3 构造类型理论
Martin-Löf 的类型理论（Martin-Löf，1984）是构造性逻辑和数学的领先方法。从哲学上讲，它与 Prawitz 共享第 2.2.2 节中提到的标准证明理论语义的三个基本假设：封闭规范证明的优先级、封闭非规范证明到规范证明的还原以及开放证明的替代观点。然而，Martin-Löf 的类型理论至少有两个特征超越了证明理论语义中的其他方法：
对证明对象的考虑以及作为对象的证明和作为证明的证明之间的相应区别。
将形成规则视为证明系统的内在规则而不是外部规则的观点。
第一个想法可以追溯到 Curry-Howard 对应关系（参见 de Groote，1995；Sørensen 和 Urzyczyn，2006），根据该对应关系，公式 A 具有确定证明的事实可以被编码为某个项 t 的事实：类型 A，其中公式 A 被标识为类型 A。这可以在类型赋值的微积分中形式化，其语句的形式为
�
：
�
。一个证明
�
：
�
该系统中的 可以被解读为表明 t 是 A. Martin-Löf (1995; 1998) 的证明。Martin-Löf (1995; 1998) 通过以下方式区分这种证明的双重意义，将其置于哲学视角中。首先我们有以下形式的陈述证明
�
：
�
。这些陈述称为判断，它们的证明称为论证。在这样的判断中，术语 t 代表命题 A 的证明。后一种意义上的证明也称为证明对象。做出判断时
�
：
�
，我们证明 t 是命题 A 的证明（对象）。在这个两层系统中，演示层是论证层。与证明对象不同，论证具有认知意义。他们的判断具有断言的力量。证明层是解释含义的层：命题 A 的含义是通过告诉 A 的证明（对象）来解释的。规范证明和非规范证明之间的区别是命题和非规范证明之间的区别。不在判断层面。这意味着一定的明确性要求。当我证明了某件事时，我不仅必须像普拉维茨的有效性概念那样为我的证明提供正当理由，而且同时必须确定这种正当理由实现了其目的。这种确定性是通过演示来保证的。从数学上讲，只有当类型可能依赖于术语时，这种双重意义的证明才能发挥其真正的力量。依赖类型是 Martin-Löf 类型理论和相关方法的基本组成部分。
第二个想法使得马丁-洛夫的方法与证明理论有效性的所有其他定义截然不同。例如，普拉维茨的程序的关键区别在于，它在性质上不是元语言的，其中“元语言”意味着首先指定证明的命题和候选，然后通过元语言中的定义，确定哪一个证明是元语言的。它们是有效的，哪些是无效的。相反，命题和证明只有在论证的背景下才发挥作用。例如，如果我们假设某件事是蕴涵的证明
�
→
�
，我们不必完全证明 A 和 B 都是格式良好的命题，但是，除了知道 A 是一个命题之外，我们只需要知道 B 是一个命题，前提是 A 已经被证明。作为一个命题是通过一种特定的判断形式来表达的，这种判断形式是在同一论证系统中建立的，该论证系统用于确定一个命题的证明已经得到实现。
在马丁-洛夫的理论中，证明论语义具有很强的本体论成分。最近的一场争论涉及这样的问题：证明对象是否具有纯粹的本体论地位，或者它们是否编纂了知识，即使它们本身不是认知行为。最近，Martin-Löf 将他的方法嵌入到断言、挑战和义务之间的相互作用理论中（Martin-Löf 2019），这使他的证明理论语义具有实用性，并将其与对话语义联系起来（见第 3.9 节）。
Martin-Löf的类型理论发现了其在同型理论中最重要的数学应用，导致同型类型理论（HOTT）和单价基础计划（2013年Univalent基金会计划）。后者通常（有时在有争议上）以直觉精神被认为是一种新型的数学基础方法，作为古典套装理论方法的替代方法。
进一步阅读：
有关马丁 - 兰夫类型理论的历史和哲学，请参见Sommaruga（2000）。对于类型理论，对于同质类型理论，以及对于单价基础程序，请参见直觉类型理论和类型理论的条目。
2.3 clausal定义和定义推理
证明理论语义通常集中在逻辑常数上。这种重点实际上永远不会质疑，显然是因为它被认为是如此明显。在证明理论中，尽管有洛伦岑的早期工作（请参阅第2.1.1节），但对原子体系的关注很少，其中逻辑规则的正当性嵌入了任意规则的理论中，而马丁·洛夫（Martin-Löf）（1971）提出了对原子公式的引入和消除规则的迭代归纳定义理论。逻辑编程的兴起已经扩大了这一观点。从证据理论的角度来看，逻辑编程是关于原子的可神经定义的原子推理理论。定义反射是一种证明理论语义的方法，它遇到了这一挑战，并试图构建一种理论，其应用范围超出了逻辑常数。
2.3.1逻辑编程的挑战
在逻辑编程中，我们正在处理表单的程序条款
�
⇐
�
1
,
……
,
�
�
这定义了原子公式。此类子句自然可以解释为描述原子的简介规则。从证明理论语义的角度来看，以下两个点至关重要：
（1）逻辑上复合公式的简介规则（条款）原则上没有区分原子的简介规则（条款）。解释逻辑编程在理论上可以促进证明理论语义向任意原子的扩展，该语义具有更广泛的应用领域的语义。
（2）计划条款不一定是有充分基础的。例如，子句的头可能出现在其体内。有充分的程序只是一种特殊的程序。在逻辑编程中使用没有进一步要求的任意子句是在证明理论语义上追求相同想法的动机。人们会承认任何形式的介绍规则，而不仅仅是特殊形式的规则，尤其是不一定是有充分根据的规则。这是定义自由的想法，它是逻辑编程的基石（语义），再次扩大了证明理论语义的应用领域。
将简介规则视为原子意义规则的思想与以其一般形式的归纳定义理论密切相关，根据该理论，归纳定义是规则的系统（参见Aczel，1977）。
2.3.2定义反射
定义反思的理论（Hallnäs，1991; 2006;Hallnäsand Schroeder-Heister，1990/91; Schroeder-Heister，1993）都从逻辑编程中受到了挑战表达式，可以给出可神经定义的表达式。正式地，此方法从所考虑的定义开始列表。每个条款都有形式
�
⇐
Δ
头A是原子公式（原子）。在最简单的情况下，身体
Δ
是原子清单
�
1
,
……
,
�
�
，在这种情况下，定义看起来像是确定的逻辑程序。我们经常考虑一个扩展的情况
Δ
也可能包含一些结构性含义”
⇒
”，有时甚至是某些结构性通用量化，这基本上是通过限制替代来处理的。如果A的定义具有形式
�
�
{
�
⇐
Δ
1
⋮
�
⇐
Δ
�
然后a具有以下介绍和消除规则
Δ
1
�
⋯
Δ
�
�
�
[
Δ
1
]
�
⋯
[
Δ
�
]
�
�
引言规则，也称为定义关闭规则，表示“沿着”条款“沿着”。消除规则称为定义反思的原理，因为它反映了整个定义。如果
Δ
1
,
……
,
Δ
�
耗尽所有可能的条件以根据给定的定义产生A，如果这些条件中的每一个都需要相同的结论C，那么一个本身就需要这一结论。如果将clausal定义视为归纳定义，则可以将该原则视为在归纳定义中表达最大条款：除了给出的条款以外的其他任何其他条款都没有定义A。显然，定义反射是讨论的倒置原理的广义形式。它在定义环境中发展其真正的力量，其自由变量超出了纯粹的命题推理，以及在没有充分基础的上下文中。非曲折定义的一个示例是原子自身的否定的定义：
�
�
{
�
⇐
（
�
⇒
⊥
）
通过否定定义原子是逻辑编程的标准示例。在定义反思的背景下，Hallnäs建议。在这里详细讨论了
关于定义反射和悖论的补充。
进一步阅读：
对于非曲折和悖论，请参阅《自我参考》和《罗素悖论》的条目。
2.4逻辑常数的结构表征
关于逻辑常数的“结构性特征”的思想和结果领域很大，其中“结构性”在这里意味着“结构规则”的证明理论，也意味着一个框架的意义带有一定的结构，该框架再次被理论上进行了证明。它的一些作者使用语义词汇，至少暗示他们的话题属于证明理论语义。其他人则明确否认这些含义，强调他们对建立常数逻辑性的特征感兴趣。问题“什么是逻辑常数？”即使常数本身的语义是真实条件：即，即通过（也许是真实条件定义的）常数显示出某种推论行为，可以用证明理论术语来描述某种推论行为，即使常数本身的语义是真实的。但是，正如一些作者认为他们的特征与语义同时考虑的那样，我们在这里提到其中一些方法是适当的。
关于逻辑常数，最直言不讳的结构主义者是科斯洛。在他的结构主义逻辑理论（1992）中，他发展了一种逻辑常数的理论，在其中他通过某些“含义关系”来表征它们，其中一种含义的关系大致与塔斯基意义上的有限后果关系（可以再次由Tarski的有限后果关系）序列系统的某些结构规则）。 Koslow以精确的metarationalsiste开发了一种结构理论，该理论并未以任何方式指定对象的域。如果给出了配备有含义关系的对象的语言或任何其他域，则可以使用结构方法来通过检查其含义属性来单列逻辑化合物。
