证明论语义学（一）

1. 背景

1.1 一般证明理论：推论与证明

1.2 推理主义、直觉主义、反现实主义

1.3 Gentzen 式证明理论：归约、规范化、切割消除

2. 证明论语义的一些版本

2.1 蕴涵的语义：可接受性、可导出性、规则

2.1.1 操作逻辑

2.1.2 Gentzen 语义

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.1 一般证明理论：结果与证明

“一般证明理论”一词由 Prawitz 创造。在一般证明理论中，“研究证明本身是为了了解其性质”，与希尔伯特式的“还原证明理论”相反，后者是“试图分析数学理论的证明，目的是将它们简化为数学的一些更基本的部分，例如有限数学或构造数学”（Prawitz，1972 年，第 123 页）。同样，克雷泽尔 (1971) 要求重新定位证明理论。他想从被忽视的角度解释“证明理论的近期工作。证明及其通过形式推导的表示被视为研究的主要对象，而不仅仅是分析结果关系的工具。”（克雷泽尔，1971，第 109 页）克雷泽尔关注证明理论和可证明性理论之间的二分法，而普拉维茨则专注于证明理论可能追求的不同目标。然而，两人都强调了将证明作为基本实体来研究的必要性，通过这些实体我们可以获得演示（尤其是数学）知识。这尤其意味着证明是认知实体，不应与形式证明或推导混为一谈。它们更像是推导在被视为论证表示时所表示的内容。 （不过，在下文中，我们经常将“证明”与“推导”同义使用，让读者自行判断其指的是形式证明还是作为认识论实体的证明。）在讨论 Prawitz (1971) 的调查时，Kreisel (1971, p. 111) 明确谈到了推导和心理行为之间的“映射”，并认为阐明这种映射是证明理论的任务，包括研究证明的同一性，这是 Prawitz 和 Martin-Löf 已列入证明理论议程的一个主题。

这意味着，在一般证明理论中，我们感兴趣的不仅仅是 B 是否源于 A，还在于我们如何从 A 出发得出 B。从这个意义上说，一般证明理论具有内涵和认识论的特征，而模型论则具有外延和形而上学的特征，它关注的是结果关系而不是建立结果关系的方式。