切消定理

切消定理
术语名称	切消定理
英语名称	cut theorem
别名	切割消去定理, cut-elimination theorem, Cut

切消定理(cut theory)是重要的元定理，由演绎的定义即可得出，因此适用于绝大多数常见公理系统。

定理

对任意公式集 [math]\displaystyle{ \Gamma }[/math] 、 [math]\displaystyle{ \Delta }[/math] 和公式 [math]\displaystyle{ \phi_1,\dots,\phi_k, \psi }[/math] ，若有 [math]\displaystyle{ \Gamma, \phi_1, \dots, \phi_k \vdash \psi }[/math] ，且对每个 [math]\displaystyle{ i = 1, \dots, k }[/math] 都有 [math]\displaystyle{ \Delta \vdash \phi_i }[/math] ，则 [math]\displaystyle{ \Gamma\cup\Delta \vdash \psi }[/math] 。

注：

1. 假设中的情况称为切规则。定理表明使用切规则的演绎一定能建立对应的不使用的演绎。这使得证明可演绎时，可以通过一些其他已确定可演绎的结论进行演绎，只要对应地把前提放在一起即可。

证明

设 [math]\displaystyle{ \Gamma, \phi_1, \dots, \phi_k \vdash \psi }[/math] 的一个演绎为 [math]\displaystyle{ \psi_0 \dots \psi_l }[/math] ， 对 [math]\displaystyle{ i = 1, \dots, k }[/math] ， [math]\displaystyle{ \Delta \vdash \phi_i }[/math] 的一个演绎为 [math]\displaystyle{ \chi_1^i \dots \chi_{m_i}^i }[/math] 。

用序列 [math]\displaystyle{ \chi_1^i \dots \chi_{m_i}^i }[/math] 替换 [math]\displaystyle{ \psi_0 \dots \psi_l }[/math] 中 [math]\displaystyle{ \phi_1 \dots \phi_k }[/math] 的出现，得到新的序列。这个序列中重复的前提都是来自 [math]\displaystyle{ \Gamma\cup\Delta }[/math] 中的元素，最后一个是 [math]\displaystyle{ \psi }[/math] ，因此是从 [math]\displaystyle{ \Gamma\cup\Delta }[/math] 到 [math]\displaystyle{ \psi }[/math] 的一个演绎。

因此， [math]\displaystyle{ \Gamma\cup\Delta \vdash \psi }[/math] 。

意义

从 [math]\displaystyle{ \Delta }[/math] 可以演绎出 [math]\displaystyle{ \psi_i }[/math] ，这些 [math]\displaystyle{ \psi_i }[/math] 作为部分条件可以演绎出 [math]\displaystyle{ \psi }[/math] ，则可以以 [math]\displaystyle{ \Delta }[/math] 作为代替，“切去”中间 [math]\displaystyle{ \psi_i }[/math] 部分的出现。

证明论
形式化公理系统（形式化、公理化）
举例	公理系统、自然演绎系统
证明、演绎	证明、可证明、演绎、可演绎
命题、定理	公理、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完全性、一致性、独立性