证明理论语义（一）
一、背景
1.1 一般证明理论：结果与证明
1.2 推理主义、直觉主义、反实在论
1.3 Gentzen式证明理论：归约、归一化、割消去
2. 证明理论语义的一些版本
2.1 蕴含语义：可接纳性、可推导性、规则
2.1.1 运算逻辑
2.1.2 Genzen 语义
2.1.3 具有更高级别规则的自然演绎
2.2 基于引入规则的推导语义
2.2.1 反转原理与和谐
2.2.2 证明理论有效性
2.2.3 构造类型理论
2.3 子句定义和定义推理
2.3.1 逻辑编程的挑战
2.3.2 定义反射
2.4 逻辑常数的结构表征
2.5 范畴证明理论
2.6 原子系统
2.7 基于句子的语义
2.8 语义完整性
3. 标准证明理论语义的扩展和替代
3.1 基本淘汰规则
3.2 否定与否定
3.3 后续演算中的和谐与反思
3.4 亚原子结构和自然语言
3.5 经典逻辑
3.6 假设推理
3.7 内涵证明理论语义
3.8.悖论
3.9 约简、博弈论和对话
3.10 底层方法
4 结论与展望
参考书目
学术工具
其他互联网资源
相关条目
该条目还包括链接到文本中的以下补充文档：
证明理论有效性的例子
定义的反思和悖论
一、背景
1.1 一般证明理论：结果与证明
“一般证明论”这个术语是普拉维茨创造的。在一般证明论中，“证明本身是为了理解其本质而研究的”，这与希尔伯特式的“还原证明论”形成鲜明对比，希尔伯特式的“还原证明论”是“试图分析数学理论的证明，其目的是将它们简化为数学的一些更基本的部分，例如有限性或构造性数学”（Prawitz，1972，第 123 页）。以类似的方式，Kreisel（1971）要求重新定位证明理论。他想从一个被忽视的角度解释“证明论中最近的工作”。证明及其通过形式推导的表示被视为主要研究对象，而不仅仅是分析结果关系的工具。” (Kreisel, 1971, p. 109) Kreisel 关注的是证明理论和可证明性理论之间的二分法，而 Prawitz 则关注的是证明理论可能追求的不同目标。然而，两者都强调研究证明作为基本实体的必要性，通过证明我们获得论证性（尤其是数学）知识。这尤其意味着证明是认知实体，不应与形式证明或推导混为一谈。当它们被认为是论证的表示时，它们更确切地说是推导所表示的意思。 （然而，在下文中，我们经常将“证明”与“推导”同义使用，让读者自行决定是形式证明还是作为认知实体的证明。）在讨论 Prawitz（1971）的调查时，Kreisel（1971，p） 111）明确谈到了推导和心理行为之间的“映射”，并认为阐明这种映射（包括调查）是证明理论的任务。证明恒等性的问题，Prawitz 和 Martin-Löf 已经将这个话题提上了证明论的议程。
这意味着，在一般证明理论中，我们不仅仅关心 B 是否从 A 得出，而且关心我们从 A 出发到达 B 的方式。从这个意义上说，一般证明理论在性质上是内涵性和认识论的，而模型证明论是内涵性的和认识论的。理论感兴趣的是结果关系，而不是建立它的方式，它是外延的和形而上学的。
1.2 推理主义、直觉主义、反实在论
证明理论语义本质上是推理性的，因为推理活动在证明中表现出来。因此，它属于推论主义（布兰顿创造的术语，见他的 1994 年；2000 年），根据该推论和推论规则建立了表达式的含义，这与指称主义相反，根据指称主义，指称是意义的主要类别。推理主义和语义学的“意义即使用”观是证明论语义学的广泛哲学框架。这种一般的哲学和语义观点与起源于数学哲学，特别是数学直觉主义的建设性观点相结合。大多数形式的证明理论语义学在精神上都是直觉主义的，这特别意味着诸如排中律或双重否定律之类的经典逻辑原理被拒绝或至少被认为是有问题的。这部分是由于证明论语义学的主要工具——自然演绎演算——偏向于直觉逻辑，因为其消除规则的直接表述就是直觉逻辑。经典逻辑只能通过某种间接证明规则来实现，这至少在某种程度上破坏了推理原理的对称性（参见第 3.5 节）。如果采取自然演绎的立场，那么直觉逻辑就是一种自然逻辑系统。逻辑符号的 BHK（Brouwer-Heyting-Kolmogorov）解释也发挥着重要作用。这种解释并不是一种独特的语义方法，而是包含各种想法，这些想法通常比正式描述更非正式。特别重要的是它的含义的功能观点，根据该观点，证明
�
→
�
是一个构造函数，当应用于 A 的证明时，会产生 B 的证明。这种函数视角是证明理论语义的许多概念的基础，特别是 Lorenzen、Prawitz 和 Martin Löf 的概念（参见第 2.1.1、2.2 节）。 2、2.2.3）。
根据达米特（Dummett，1975）的观点，直觉主义的逻辑立场与反实在论的哲学立场相对应。现实主义关于独立于识别的现实的观点是形而上学的对应观点，即所有句子要么是真要么是假，与我们识别它的方式无关。证明论语义学的主要部分遵循达米特及其与反实在论的联系。
1.3 Gentzen式证明理论：归约、归一化、割消去
Gentzen 的自然演绎演算及其由 Prawitz 的呈现是大多数证明理论语义学方法的背景。自然演绎至少基于三个中心思想：
排除假设：在推导过程中，假设可以被“排除”或“消除”，因此自然演绎的核心概念是基于假设的推导。
分离：每个原始规则模式仅包含一个逻辑常量。
介绍和消除：逻辑常量的规则是成对出现的。引入规则允许人们推断出一个以所讨论的常数作为其主要运算符的公式，消除规则允许从这样的公式中得出结果。
在 Gentzen 的一阶逻辑自然演绎系统中，推导以树的形式编写，并基于众所周知的规则。例如，蕴涵有如下引入和消除规则
[
�
]
�
�
→
�
→
我
�
→
�
�
�
→
乙
其中括号表示排除假设 A 出现的可能性。推导的开放假设是最终公式所依赖的那些假设。如果一个推导没有开放假设，则该推导称为封闭推导，否则称为开放推导。如果我们处理量词，我们也必须考虑开放的单个变量（有时称为“参数”）。 Prawitz (1965) 首次系统研究并发表的对证明理论语义学至关重要的元逻辑特征包括：
减少：对于每个由介绍和消除组成的迂回，都有一个减少步骤来消除该迂回。
规范化：通过连续应用归约，可以将推导转化为不走弯路的规范形式。
暗示消除弯路的标准减少步骤如下： [
�
]
⋮
�
�
→
�
|
�
�
减少到
|
�
⋮
�
规范化的一个简单但非常重要的推论如下：直觉逻辑中的每个封闭推导都可以简化为在最后一步中使用引入规则的推导。我们还说直觉自然演绎满足“引入形式性质”。在证明理论语义学中，这一结果在“基本假设”标题下显得尤为突出（Dummett，1991，第 254 页）。 “基本假设”是对技术证明理论结果进行哲学重新解释的典型例子。
进一步阅读：
关于证明理论语义学的一般方向，请参阅 Kahle 和 Schroeder-Heister 编辑的 Synthese 特刊 (2006)、Piecha 和 Schroeder-Heister 编辑的读者 (2016b)、Francez 的教科书 (2015) 以及Wansing (2000) 和 Schroeder-Heister (2016) 的调查。
关于证明论的哲学立场和发展，参见希尔伯特纲领条目、证明论发展条目以及Prawitz (1971)。
关于直觉主义，参见直觉逻辑条目、数学哲学中的直觉主义条目和直觉逻辑发展条目。
对于反实在论，请参阅对形而上学实在论的挑战以及 Tennant (1987; 1997) 和 Tranchini (2010; 2012a) 的条目。
对于 Gentzen 式的证明理论和自然演绎理论，请参见逻辑中自然演绎系统的条目，以及除了 Gentzen (1934/35) 的原始介绍之外，Jaśkowski (1934) 的假设理论、Prawitz (1965) 的理论。 ）经典专着，Tennant（1978；2017），Troelstra 和 Schwichtenberg（2000）， Negri 和 von Plato (2001)、Mancosu、Galvan 和 Zach (2021) 以及 Andrzej Indrzejczak 在互联网哲学百科全书中关于自然演绎的条目。
2. 证明理论语义的一些版本
2.1 蕴含语义：可接纳性、可推导性、规则
蕴涵语义是证明理论语义的核心。与经典的真值条件语义学不同，蕴涵本身就是一个逻辑常数。它还有一个特点，即它与后果的概念联系在一起。由于肯定前件和希尔伯特式系统中所谓的演绎定理，它可以被视为在句子层面上表达结果，即
γ
,
�
⊢
�
和
γ
⊢
�
→
�
。
对含义的非常自然的理解
�
→
�
将其解读为表达允许从 A 到 B 的推理规则。根据以下条件许可从 A 到 B 的步骤
�
→
�
正是 modus ponens 所说的。演绎定理可以被视为建立规则的手段：证明 B 可以从 A 推导出来，证明我们可以从 A 传递到 B 的规则是合理的。沿着这样的思路，基于规则的蕴涵语义奠定了几个概念的基础证明论语义学，尤其是洛伦岑、冯·库切拉和施罗德-海斯特的著作。
2.1.1 运算逻辑
洛伦岑（Lorenzen）在他的《操作逻辑和数学导论》（1955）中从无逻辑（原子）演算开始，它对应于产生式系统或语法。如果一条规则可以添加到系统中而不扩大其可导出原子的集合，他称该规则在这样的系统中是可接受的。暗示箭头
→
被解释为表达可受理性。一个暗示
�
→
�
如果作为规则阅读时，它是可接受的（相对于基础微积分），则被认为是有效的。对于迭代的影响
（
=
规则）洛伦岑发展了一种更高级别的可接受性陈述理论。某些陈述，例如
�
→
�
或者
（
（
�
→
�
）
,
（
�
→
�
）
）
→
（
�
→
�
）
独立于基础微积分而成立。它们被称为普遍可接受的[“allgemeinzulässig”]），并构成了一个积极蕴涵逻辑的系统。与此相关的是，通用量化定律
∀
使用具有图解变量的规则的可接受性声明来证明其合理性。
为了证明逻辑常数定律的合理性
∧
,
∨
,
∃
和
⊥
，洛伦岑使用了反转原理（他创造的术语）。反演原理以非常简化的形式表示，在不考虑规则中的变量的情况下，从 A 的每个定义条件中可以获得的所有内容都可以从 A 本身获得。例如，在析取的情况下，令 A 和 B 各自为以下定义条件：
�
∨
�
正如原始规则所表达的
�
→
�
∨
�
和
�
→
�
∨
�
。那么逆原理说
�
∨
�
→
�
是可接受的假设
�
→
�
和
�
→
�
，这证明了析取消除规则的合理性。其余的连接词也以类似的方式处理。如果是
⊥
, 荒谬法则
⊥
→
�
是从没有定义条件这一事实得出的
⊥
。
2.1.2 Genzen 语义
在他所谓的“Gentzen 语义学”中，von Kutschera（1968）像 Lorenzen 一样给出了逻辑上复杂的蕴涵式陈述的语义。
�
1
,
……
,
�
�
→
�
关于控制原子句子推理的演算 K。与洛伦岑的根本区别在于
�
1
,
……
,
�
�
→
�
现在表达的是可推导性而不是可接受性声明。
为了将其转化为命题逻辑的逻辑常数的语义，冯·库切拉（von Kutschera）提出如下观点：当放弃二价性时，我们不能再对原子公式使用经典的真值赋值。相反，我们可以使用微积分来证明或反驳原子句子。此外，由于微积分不仅生成证明或反驳，而且生成任意的可导性关系，因此这个想法是直接从原子系统中的可导性开始，并用表征逻辑连接词的规则来扩展它。为此，von Kutschera 给出了一个顺序演算，其中包含在后继词和先行词中引入 n 元命题连接词的规则，从而产生广义命题连接词的顺序系统。冯·库切拉接着证明，如此定义的广义联结词都可以用直觉逻辑的标准联结词（合取、析取、蕴涵、荒谬）来表达。
进一步阅读：
以 von Kutschera 的风格扩展表达完整性：Wansing (1993a)。
2.1.3 具有更高级别规则的自然演绎
在开发任意逻辑常量的推理规则的通用模式时，Schroeder-Heister (1984) 提出，作为语义要求，逻辑复杂的公式表达规则系统的内容或公共内容。规则 R 是公式 A 或具有以下形式
�
1
,
……
,
�
�
⇒
�
， 在哪里
�
1
,
……
,
�
�
是规则。这些所谓的“更高级别的规则”将规则可以释放假设公式的想法概括为它们可以释放假设规则（即用作假设的规则）的情况。对于标准连接词，这意味着
�
∧
�
表达对的内容
（
�
,
�
）
;
�
→
�
表达规则的内容
�
⇒
�
;
�
∨
�
表示A和B的共同内容；和荒谬
⊥
表达了空族规则系统的共同内容。对于任意 n 元命题连接词，这导致了具有广义引入和消除规则的自然演绎系统。这些一般连接词被证明可以根据标准连接词来定义，这建立了标准直觉连接词的表达完整性。
