切消定理

切消定理是確立相繼式演算重要性的主要結果。它最初由 Gerhard Gentzen 在他的劃時代論文 "邏輯演繹研究" 對分別形式化直覺邏輯和經典邏輯的系統 LJ 和 LK 做的證明。切削定理聲稱在相繼式演算中，擁有利用了切規則的證明的任何判斷，也擁有無切證明，就是說，不利用切規則的證明。

相繼式是與多個句子有關的邏輯表達式，形式為 "$A,B,C,\ldots \vdash N,O,P$"，它可以被讀做 "A, B, C, $\ldots$ 證明 N, O, P"，並且(按 Gentzen 的註釋)應當被理解為等價於真值函數 "如果 (A & B & C $\ldots$) 那麼 (N or O or P)"。注意 LHS(左手端)是合取(and)而 RHS(右手端)是析取(or)。LHS 可以有任意多個公式；在 LHS 為空的時候，RHS 是重言式。在 LK 中，RHS 也可以有任意數目的公式--如果沒有，則 LHS 是個矛盾，而在 LJ 中，RHS 只能沒有或有一個公式: 在右緊縮規則前面，允許 RHS 有多於一個公式，等價於容許排中律。注意，相繼式演算是相當有表達力的框架，已經為直覺邏輯提議了允許 RHS 有多個公式的相繼式演算，而來自 Jean-Yves Girard 的邏輯 LC 得到了 RHS 最多有一個公式的經典邏輯的更加自然的形式化；邏輯和結構規則的相互作用是它的關鍵。

"切"是在相繼式演算的正規陳述中的一個規則，並等價於在其他證明論中的規則變體，給出

(1) $(A,B,\ldots )\vdash C$

和

(2) $C\vdash (D,E,\ldots )$

你可以推出

(3) $(A,B,\ldots )\vdash (D,E,\ldots )$

就是說，在推論關係中"切掉"公式 "C" 的出現。

切消定理聲稱(對於一個給定的系統) 使用切規則的任何相繼式證明也可以不使用這個規則來證明。如果我們認為 $(D,E,\ldots )$ 是一個定理，則切消簡單的聲稱用來證明這個定理的引理 $C$ 可以被內嵌(inline)。在這個定理的證明提及引理 $C$ 的時候，我們可以把它代換為 $C$ 的證明。因此，切規則是可接納的。

對於用相繼式公式化的系統，分析性證明是不使用切規則的證明。這種證明典型的會很長，當然沒有必要這麼做。在散文 "Don't Eliminate Cut!" 中，George Boolos 展示了可以使用切在一頁中完成的推導，而它的分析性證明要耗盡宇宙的壽命來完成。

這個定理有很多豐富的推論。一旦一個系統被證明有切消定理，這個系統通常立即就是一致的。這個系統通常也有子公式性質，這是達成證明論語義的重要性質。切削是證明 interpolation theorem 的最強力工具。完成基於歸結原理的證明查找的可能性，本質洞察導致了 Prolog 程式語言，依賴於在適當的系統中接納切規則。