查看“︁切消定理”︁的源代码

[[分类:证明论]]
{{InfoBox
|name=切消定理
|eng_name=cut theorem
|aliases=切割消去定理,cut-elimination theorem,Cut
}}
'''切消定理'''('''cut theory''')是重要的元定理，由[[演绎]]的定义即可得出，因此适用于绝大多数常见[[公理系统]]。

== 定理 ==

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

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

== 证明 ==

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

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

因此， <math>\Gamma\cup\Delta \vdash \psi</math> 。

== 意义 ==

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


{{证明论}}