切消定理
切消定理是根岑（Gentzen）的定理，它指出，在任何相继式演算证明中，可以移除形式化引理使用的切规则，从而使证明仅由其所涉及的公式构成。
用 PaperMind 寻找选题即将推出Find papers & topics
Tools & resources
Learn & explore
视频即将推出
Definition
切消定理是构造性过程和定理，它表明任何使用切规则的相继式演算推导都可以转换为不使用切规则的推导，从而使每个可证的相继式都具有一个仅包含最终相继式子公式的证明。
Scope
本主题涵盖切规则及其在相继式演算中的作用、切消过程及其终止性、无切证明的子公式性质、由此产生的一致性和可判定性结果，以及切消可能导致的证明大小界限。
Core questions
- 切规则表达了什么？为什么移除它意义重大？
- 切消过程如何终止？
- 什么是子公式性质？它对证明搜索意味着什么？
- 消除切的计算成本是多少？
Key theories
- 根岑主定理
- 根岑的主定理指出，切规则在相继式演算中是可容许的，因此任何使用切的证明都可以转换为同一最终相继式的无切证明。
- 子公式性质
- 无切证明中出现的每个公式都是最终相继式的子公式，这限制了证明的形状，并构成了判定过程和一致性论证的基础。
- 通过切消实现一致性
- 由于空相继式的无切证明是不可能的，切消直接证明了演算（以及它所形式化的理论）是一致的。
Clinical relevance
切消定理是一个具有广泛影响的基础性结果：它产生了相容性证明、对自动化定理证明和tableau方法至关重要的子公式性质、插值定理，并通过“证明即程序”对应关系，实现了类型化程序的范式化。
History
根岑于1934年为一阶逻辑证明了切消定理，即他的Hauptsatz（主定理），该方法成为结构证明论的基石。泰特（Tait）和吉拉德（Girard）将该技术扩展到更强的系统和高阶逻辑，而切消下证明大小增长的界限本身也成为一个研究课题。
Key figures
- Gerhard Gentzen
- William Tait
- Jean-Yves Girard
- Gaisi Takeuti
Related topics
Seminal works
- takeuti1987
- troelstra2000
- negri2001
Frequently asked questions
- 证明中的“切”是什么？
- 切规则允许人们证明一个引理然后使用它：从一个建立某个公式的推导和另一个将该公式用作前提的推导中，它得出组合结果。切消表明，原则上总可以移除此类中间引理。
- 为什么消除切会使证明变得更长？
- 移除一个切可能需要复制推导的很大一部分，并且重复此操作可能会使证明大小呈指数塔式增长。因此，无切证明在概念上更简单，但可能比原始的带切证明大得多。