切消定理

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

切消定理簡介

切消定理 切消定理
切消定理 切消定理

相繼式是與多個句子有關的邏輯表達式,形式為 ,它可以被讀做"A, B, C, 證明N, O, P",並且(按Gentzen的注釋)應當被理解為等價於真值函式"如果(A & B & C ......)那么(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、

切消定理 切消定理

2、

由1和2可以推出:

切消定理 切消定理

3、

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

切消定理說明

切消定理 切消定理

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

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

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

相關詞條

相關搜尋

熱門詞條

聯絡我們