（逻辑/证明论）割消去：指在序列演算等形式系统中，通过一系列变换把证明里使用的 cut（割）规则去掉，同时仍能证明同一个结论。直观上，它把“先引入一个中间命题再消去”的推理步骤改写为更“直接”的推导，常用于说明系统的一致性、可判定性、子公式性质等。该术语在更广义上也可指“消除中间引理式步骤”的证明正规化思想。
/kt lmen/
Cut elimination can simplify a proof by removing unnecessary intermediate steps.
割消去可以通过移除不必要的中间步骤来简化一个证明。
In sequent calculus, the cut elimination theorem shows that any proof using cut can be transformed into a cut-free proof, often yielding the subformula property.
在序列演算中，割消去定理表明任何使用割规则的证明都能转换为不含割的证明，并且往往由此得到子公式性质。
cut 在证明论里是“割规则”的名称（把一个中间公式当作“切口/接口”，把两段推导接起来）；elimination 来自拉丁语 eliminare，有“移出、去除”的意思。术语整体主要与德国逻辑学家 Gentzen（根岑）在 1930 年代提出的证明论工作相关，他用割消去来刻画证明的“正规化/纯化”。
Select Language