切消定理是確立相繼式演算重要性的主要結果。它最初由格哈德·根岑在他的劃時代論文《邏輯演繹研究》對分別形式化直覺邏輯和經(jīng)典邏輯的系統(tǒng)LJ和LK做的證明。切消定理聲稱在相繼式演算中，擁有利用了切規(guī)則的證明的任何判斷，也擁有無切證明，就是說，不利用切規(guī)則的證明。
切消定理簡介
相繼式是與多個句子有關的邏輯表達式，形式為，它可以被讀做"A, B, C, 證明N, O, P"，并且（按Gentzen的注釋）應當被理解為等價于真值函數(shù)"如果（A & B & C ......）那么（N or O or P）"。注意LHS（左手端）是合取（and）而RHS（右手端）是析取（or）。LHS可以有任意多個公式；在LHS為空的時候，RHS是重言式。在LK中，RHS也可以有任意數(shù)目的公式--如果沒有，則LHS是個矛盾，而在LJ中，RHS只能沒有或有一個公式：在右緊縮規(guī)則前面，允許RHS有多于一個公式，等價于容許排中律。注意，相繼式演算是相當有表達力的框架，已經(jīng)為直覺邏輯提議了允許RHS有多個公式的相繼式演算，而來自Jean-Yves Girard的邏輯LC得到了RHS最多有一個公式的經(jīng)典邏輯的更加自然的形式化；邏輯和結構規(guī)則的相互作用是它的關鍵。
"切"是在相繼式演算的正規(guī)陳述中的一個規(guī)則，并等價于在其他證明論中的規(guī)則變體，給出
1、
2、
由1和2可以推出：
3、
就是說，在推論關系中"切掉"公式"C"的出現(xiàn)。
切消定理說明
切消定理聲稱（對于一個給定的系統(tǒng)）使用切規(guī)則的任何相繼式證明也可以不使用這個規(guī)則來證明。如果我們認為 是一個定理，則切消簡單的聲稱用來證明這個定理的引理C可以被內嵌（inline）。在這個定理的證明提及引理 C的時候，我們可以把它代換為C的證明。因此，切規(guī)則是可接納的。
對于用相繼式公式化的系統(tǒng)，分析性證明是不使用切規(guī)則的證明。這種證明典型的會很長，當然沒有必要這么做。在散文《不要消除切呀!》中，George Boolos展示了可以使用切在一頁中完成的推導，而它的分析性證明要耗盡宇宙的壽命來完成。
這個定理有很多豐富的推論。一旦一個系統(tǒng)被證明有切消定理，這個系統(tǒng)通常立即就是一致的。這個系統(tǒng)通常也有子公式性質，這是達成證明論語義的重要性質。切削是證明插值定理的最強力工具。基于歸結原理的完成證明查找的可能性，導致Prolog編程語言的本質洞察，依賴于在適當?shù)南到y(tǒng)中接納切規(guī)則。
參考資料 >