邏輯常項的使用規則的生成與證成

周志榮

在證明論語義學中，邏輯常項的意義是通過它的兩個核心的使用規則來刻畫的，那就是引入規則和消去規則（以下簡稱為“I-規則”和“E-規則”）。通常，其中一者在對邏輯常項的語義解釋中會被賦予優先性，而具有優先性的規則被看作是意義定義性的，它們是自我證成的，而另外一個規則被看作是意義應用性的，需要借助語義優先的規則來證成。證明論語義學提供的常見的語義解釋原則有兩種：I-優先原則和E-優先原則（在哲學上，它們分別對應于證實主義和實用主義的意義觀念）。不過，邏輯常項的使用規則的證成面臨著一個嚴峻的挑戰，那就是tonk-問題。普萊爾（A.N.Prior）于1960 年提出了著名的tonk 算子，它的兩個使用規則分別是：α ?αtonkβ（tonkI）和αtonkβ ?β（tonkE）。（[12]）1通常，規則是采取樹形方式來表達的，由橫線隔開，處于橫線上方的公式是規則應用（推導）的前提，處于橫線下方的公式是規則應用（推導）的后果。為節約空間，在非必要的情形下我們采取橫式的描述方式，用“?”代替樹形中的橫線，將前提和結論分開。對于假設性前提，我們用“α ?β”表示由假設α 到β 的一種推導，β 是基于α這個假設推導出來的后果，其中“?”對應于樹形表達中的“”。（注意，這與施羅德-海斯特（P.Schroeder-Heister）將“α ?β”當作二階規則不同，在他給出的樹式規則中，“α ?β”既可以表示由假設α 到β 的推導構成的前提，也可以整個地被處理為一個假設性前提中的假設，比如(α ?β) ?γ。）（[18]）無論按照I-優先原則還是E-優先原則，tonk 似乎都應該被當作一個有意義的邏輯常項。但問題是，在一個一致的演繹系統中添加tonk 的使用規則會導致擴張系統的平凡化，即在該擴張系統中，對任意公式α和β都有：α ?β。關于tonk-問題，主要有兩種應對方案：一是通過修改推導關系或邏輯后承關系的性質來阻止tonk 產生壞的后果，比如禁止傳遞性的推導關系，或修改保真性的邏輯后承關系（[2,16]）；二是對邏輯常項的使用規則提出協調性的要求，以便阻止那些具有不協調的使用規則的算子（[19,22]）。本文同樣將tonk-問題歸結為（邏輯）常項的使用規則的協調性問題。

貝爾納普（N.Belnap）的保守性要求（[1]）、普拉維茨（D.Prawitz）的“倒置原則”（[10]）、達米特（M.Dummett）的“局部峰的削平”思想（[3]）都是對協調性問題做出的回應。這些對協調性的理解都遵循了I-優先原則，忽略了E-規則對協調性的貢獻，因此這些標準無法阻止另外一些不協調情形。近來較受關注的GE-協調性標準訴諸于E-規則的普遍形式（即GE-規則形式）來表達I-和E-規則之間的協調性。（[4,15]）2“GE-協調性”是“普遍的消去的協調性（general-elimination harmony）”（有時候也寫作“普遍化的消去的協調性（generalised-elimination harmony）”）的簡稱。這種說法是由弗朗西斯（N.Francez）和迪克霍夫（R.Dyckhoff）于1997 年先提出來的，可惜他們的這篇論文直到2012 年才公開發表，里德（S.Read）于2010 發表的論文則直接在其標題中使用了“GE-協調性”，但他在文中也承認他借用了弗朗西斯和迪克霍夫的說法。（[15]，第562 頁）這種做法欠缺對于普通I-和E-規則與GE-規則之間關系的考慮，因而同樣無法排除一些明顯的不協調情形。本文的核心工作在于描述由邏輯常項的I-規則生成其GE-規則以及其E-規則的機制，以及直接由其E-規則生成普遍的E-規則的機制，并論證這兩種生成機制包含了兩種協調性的要求，它們（尤其是后者）可以彌補上述協調性標準的不足，從而為邏輯常項的使用規則的協調性問題以及證成問題提供一個更好的解答。

1 tonk-問題與不協調性的兩種類型

一個邏輯常項的意義是借助它的I-規則或E-規則來定義的，但這并不意味著擁有這兩種規則的常項或算子都具有融貫的意義。普萊爾1960 年提出的tonk 就是一個經典的例子，借助tonk 的兩個使用規則和結構性推導規則的應用3這里涉及的結構性推導規則就是傳遞性規則（Trans）：如果α ?β，β ?α，則α ?β。，我們可以得到：α ?β。由于α和β是任意公式，這意味著將tonk 添加到一個一致的演繹系統S中會造成非保守的擴張，其擴張系統S ∪{tonk}中的推導關系被平凡化。由tonk 導致的問題包含了兩個層面：第一、我們希望一個邏輯常項至少應該具有融貫的意義。如果一個常項的使用規則導致了不一致的后果，那么這個常項的意義就不是融貫的，這不僅說明包含該常項的語言功能異常，而且這樣的常項也不應該被看作是邏輯的常項。因此，導致平凡化后果的規則是不可接受的，像tonk 這樣的常項必須作為異常算子被排除掉。第二、作為邏輯的常項而言，保守性擴張是一個必要的要求，否則就會與邏輯的單純性原則（principle of innocence）相沖突。按照邏輯的單純性原則，將一個邏輯常項及其規則添加到一個語言或理論中不應該對原有語言的意義和原有理論所斷定的內容造成任何影響。（[3]，第220 頁；[21]，第619 頁；[7]，第207 頁）4當然，并非所有學者都認為單純性原則是一個合理的要求。（[17]，第238 頁）不過，將意義的融貫性和邏輯單純性原則看作是要求邏輯常項的I-和E-規則必須具有協調性的理由，這是研究邏輯常項的使用規則的證成問題或協調性問題的基本出發點。這兩點也是我們考察一個協調性標準是否合理的依據。本文所要提出的協調性標準的合理性同樣可以依據這兩點來評估，實際上它也通過彌補了其他協調性標準在這兩點上的不足而得到自我辯護。

為了阻止tonk 這樣的異常算子，貝爾納普提出了保守性的要求。（[1]）按照該要求，令S為一個背景理論，?為這個理論上的推導關系，令S+S ∪{δ}是對S的擴張。該擴張是保守的，當且僅當，對任意LS公式集Γ 和公式γ，如果Γ?S+γ則Γ?S γ。然而，不難看出，這種保守性要求依賴被擴張理論的演繹背景即推導關系或邏輯后承關系的性質，因此至少有三種情形對該要求構成例外：

(1.1) 背景理論本身就是平凡的，對它的任何擴張仍然是平凡的，因而是保守的。在這種情形下，tonk 則滿足保守性的要求。

(1.2) 相對于較弱的演繹系統，添加一個在我們看來正常的邏輯常項反而會導致非保守性的擴張。析取就是一個非常典型的反例：量子析取（）的推理規則使得析取分配律（即α ∧(βγ)?(α ∧β)(α ∧γ)）在量子邏輯系統中失效。（[3]，第66、77 頁）5量子邏輯與經典邏輯的實質區別就在于前者放棄了析取分配律。普特南在1968 年通過例證表明析取經典的分配律并不是普遍有效的，而且他指出，該規律也是在量子邏輯中唯一放棄的經典規律。（[13]，第226 頁）達米特也將量子析取看作是對經典邏輯和實在論的挑戰，盡管量子邏輯仍然接受排中律。（[3]，第333 頁）這是因為：雖然量子析取與經典析取（∨）具有相同的I-規則，但前者的E-規則卻較后者弱，因為前者的應用是有限制條件的而后者沒有，即前者禁止使用并行前提（collateral premises）進行推導。如果我們將經典析取添加到{∧,ü}這個演繹系統中，在擴張系統{∧,,∨}中，析取分配律則可以被推導出來，而它在原來的{∧,}系統中卻是不可推導的。這表明{∧,,∨}是對{∧,}的非保守性擴張。

(1.3) 如果背景理論禁止傳遞性推導，添加tonk 到這個理論中就不會導致平凡化的后果。這也指明了解決tonk-問題的一種常見做法。庫克（R.Cook）從模型論語義學的角度，借助一種四值語義學改造了經典的邏輯后承關系，提出tonk-后承關系，這種后承關系就是非傳遞的，從而保證tonkβ和αtonk，但是。（[2]）雷普利（D.Ripley）則從證明論語義學的角度論證說矢列演算系統中的切割（Cut）規則的應用是造成平凡化后果的主要原因，并且他認為這條規則缺乏充分的正當性。（[16]）如果在一個基于矢列演算的演繹系統S中禁止使用切割規則（這就相當于在自然演繹的系統中禁止了傳遞性的推導），那么添加tonk-規則就不會導致平凡化的后果。

無論通過何種方式禁止傳遞性的推導關系，都可以解決tonk 導致的平凡化問題。但這種方法并不具有普遍有效性。萬興（H.Wansing，[23]）構造出更多的類似于tonk 的異常算子6本文只將導致平凡化問題的算子稱為“異常算子”。，這些算子的使用規則分別會導致包含特定推導關系的系統平凡化。比如，下面這些推導關系：

(G) 最普遍的推導關系：{Λ?并且?α?β(α/?β)}；

(F) 前進式的推導關系：{Λ|?α?β(α ?β)?并且?α?β(α/?β)}；

(B) 后退式的推導關系：{Λ|?α?β(β ?α)?并且?α?β(α/?β)}；

(Q) 準有序性的推導關系：{Λ|?α(α ?α),?α?β?γ((α ?β并且β ?γ)?α ?γ)?并且?α?β(α/?β)}；

由于后文要用新的方法分析這些常項，這里有必要將這些常項的使用規則和導致的問題陳述如下（其中“[χ]”表示χ是被相應規則的應用所解除的假設）：7除此之外，對這些異常算子的I-和E-規則，萬興分別給出了樹形的描述和橫式的描述，他的橫式描述和我們這里給出的稍有不同，以tonk>的規則為例，他給出的橫式描述為：α ?β ?α ?tonk>(I)；α ?tonk> ?α ?β(E)。這種橫式描述與樹式描述并不是完全匹配的，橫式的表述嚴格地講不能被看做是一個算子的引入和消去規則，因為至少在I-規則中，其結論并不是以該算子為主算子的公式，而是一個推導。在本文中，我們對規則提供的橫式描述更符合萬興的樹式所要表達的意思。

這里要注意：在所有這些E-規則中，結論β與相應I-規則的前提中的β不必相同。與之前我們討論過的邏輯常項不同，這里算子都是0-元的，α和β與I-規則的結論以及E-規則的大前提并沒有結構上的聯系，所以I-規則的前提與E-規則的小前提以及結論并沒有實質的聯系，甚至可以說I-和E-規則除了出現了0-元算子構成的公式相同之外，其他公式可以完全沒有聯系，這些公式分別對于相應的I-和E-規則而言是任意的。分別將這四組規則添加到F-邏輯、B-邏輯、Q-邏輯和G-邏輯的演繹系統中，就會得到以下結果：（[23]，第658-659 頁）

(1.8) tonk>是使F-邏輯的演繹系統平凡化的算子；

(1.9)

(1.10) 是使Q-邏輯的演繹系統平凡化的算子；

(1.11) super-tonk 是使G-邏輯的演繹系統平凡化的算子。

以tonk>和super-tonk 為例。由于在F-邏輯的演繹系統中，推導關系具有“前進式”的性質：對于任意公式α，都存在一個公式β使得α ?β。我們可以將這種性質理解為一種結構性規則，稱之為（F）。類似地，在G-邏輯的演繹系統中，推導關系具有普遍形式，即存在公式φ、ψ使得φ ?ψ，稱之為（G）。

由以上兩個推導過程可見，分別在F-邏輯和G-邏輯的擴張系統中，我們可以由任意公式α可推導出任意公式γ，這意味著，將tonk>和super-tonk 的I-規則和E-規則分別添加到F-邏輯和G-邏輯的演繹系統中，就會導致平凡化的后果。另外兩個異常算子的情況與此相似。

根據萬興得到的結果，要解決平凡化問題，我們似乎不得不禁止上述所有推導關系。甚至為了解決super-tonk 的問題，我們不得不禁止做任何推導。這顯然不是解決問題的恰當方式。因此，回到起點，我們要考慮的tonk-問題并不僅僅指由tonk 造成的平凡化問題，而是由所有類似的異常算子造成的平凡化問題，而這個問題可以進一步地歸結為：什么樣的I-規則和E-規則才能賦予一個邏輯常項以融貫的意義？人們的共識是：一個邏輯常項的這兩種使用規則應該具有某種滿足邏輯單純性原則的協調性。假設一個邏輯常項的這兩種使用規則是協調的，就會存在兩種不協調的情形：（[21]，第621 頁）

(1.12) 增強其E-規則（或削弱其I-規則），由此得到的新算子就帶有強E-規則（或弱I-規則），相應導致的不協調性可被稱為“強消去的不協調性”（或“弱引入的不協調性”），例如tonk 及其類似的異常算子的使用規則體現出來的不協調性。

(1.13) 削弱其E-規則（或增強其I-規則），由此得到的新算子就帶有弱E-規則（或強I-規則），相應導致的不協調性可被稱為“弱消去的不協調性”（或“強引入的不協調性”），例如量子析取的使用規則的不協調性。

為了阻止“不協調的”情形，我們首先需要明確一個恰當的“協調性”標準。但事實上，人們對于“協調性”這個概念有著不同的理解。除了上述基于系統保守性的理解之外，還有另外一些理解，例如普拉維茨的“倒置原則”、達米特的“局部峰的削平”以及近來受關注較多的“GE-協調性”。接下來，本文分別闡釋這些概念，并著重探討GE-協調性，因為這種協調性與本文要描述的I-和E-規則之間的生成關系密切相關。

2 GE-規則與GE-協調性

達米特將貝爾納普的保守性要求稱為“背景協調性”或“總體協調性”，與此相對應的是他所主張“內在協調性”（[3]，第250 頁），后者只與一個常項的I-和E-規則的連續應用在推導中造成的“局部峰”有關。一個“局部峰”就是關于E-規則應用的結果的一種迂回的、間接的推導，而削平局部峰（leveling a peak）是確保I-和E-規則具有內在協調性的途徑，這就是要實現從I-規則應用的前提到相應的E-規則應用的結果的直接推導。這與普拉維茨的“倒置原則”所要表達的基本思想是一致的：一個邏輯常項的I-規則“定義了”該常項的意義，而其E-規則就是該意義的應用，因而其E-規則可以被看作是其I-規則的“倒置”。（[10]，第33 頁）“倒置原則”的思想可以追溯到根岑。（[5]，第81 頁）根據根岑的看法，邏輯常項的E-規則是借助作為相應的I-規則的“倒置”而得到證成的。這些協調性概念的共同之處就是假設I-規則優先于其E-規則，是意義定義性的，而E-規則是意義應用性的，前者作為定義是自我證成的，而后者需要借助與前者的協調性來證成。

無論普拉維茨的“倒置原則”還是達米特的“局部峰的削平”，都意在確保邏輯常項的I-和E-規則滿足局部的保守性要求，即至少E-規則的應用結果不會超出I-規則的應用前提。雖然這種要求可以擺脫對演繹系統本身的依賴，但其缺點也很明顯，那就是無法對弱消去的不協調性問題做出回應，當然也無法對具有標準規則的邏輯常項（如經典析取）可能造成的非保守性擴張問題做出回應。這些理解都將（邏輯）常項的I-規則置于更基礎的位置，從而忽略了E-規則對于（邏輯）常項的融貫意義的貢獻，這還導致：如果兩個（邏輯）常項具有相同的I-規則且它們的E-規則都不強于該I-規則的話，那么它們就是同義的。

GE-協調性則有所不同，它將E-規則置于更重要的位置。它并不否認I-規則是意義定義性的，而是直接將協調性問題歸結為E-規則的普遍形式問題，試圖借助邏輯常項的E-規則的特定普遍形式來說明其E-規則與I-規則的“倒置”關系。邏輯常項的E-規則的特定普遍形式（即GE-規則）被認為包含了一種協調性的要求：

(HGE)（邏輯）常項δ的“I-規則與E-規則是GE-協調的，當且僅當其E-規則是由I-規則所協調地導致的GE-規則”。（[4]，第623 頁）

由于一個邏輯常項的GE-規則也是它的其中一個E-規則，為有所區別，可稱其非普遍形式的E-規則為“普通E-規則”（當不引起誤解時，我們談論的“E-規則”指的就是普通E-規則）。考慮到一個邏輯常項的I-規則可能不唯一，其導致的E-規則也可能不止一個，令n-元邏輯常項δ的其中一個I-規則為：Πi ?（δIi），其中δ→α表示δ(α1,...,αn)；Πi是斷定的一個直接根據集（其中就被看作是斷定的直接根據）。如果δ E-規則與其I-規則是相協調的，則它就是具有如下形式的GE-規則（其中，“[Πi]”是對“[],[],...,[]”的縮寫）：

在這個形式中，被稱為“大前提”，其余前提都被稱為“小前提”。其中的“[ξ]”仍然表示ξ是被該規則的應用所解除的假設。（邏輯）常項δ的GE-規則的大前提正是其I-規則的結論，而在小前提中，作為被解除的假設的那些公式正是δ的I-規則的前提，因而也是斷定的直接根據。由此，GE-規則似乎包含了對協調性的一種理解。對此有兩種不同的說明：

第一種觀點認為，GE-規則滿足了普拉維茨的倒置原則的要求。普拉維茨的倒置原則的基本思想可以概括為：凡是由可以推出的后果，可以直接由的直接根據推導出來。在普拉維茨那里，（邏輯）常項δ的I-和E-規則是否滿足倒置原則，是通過對推導的更一般的“規范化”程序來實現的。在一個推導中，一個公式既作為δ I-規則應用的結論和δ E-規則應用的大前提出現（這兩種應用未必是連續的），就是被稱為“最大公式”；如果δ的I-規則和E-規則滿足倒置原則的要求，那么這個最大公式就可被移除。不包含最大公式的推導就具有規范形式的推導（即規范的推導），而一個推導是可被規范化的，就意味著它可以被還原為一個規范的推導。借助下面這個還原可以看到，δ的GE-規則與相應的I-規則滿足倒置原則的要求：

還原之后的推導就是由的理由出發的關于γ的直接推導，也被稱為“規范的”推導，因為它不再包含最大公式（當然還需要假設在這個推導中不包含其他最大公式）。由Πi到γ的推導的規范性表明：凡是由可以推導出來的東西都可以由它的直接推導出來。這恰恰滿足了基于局部保守性的協調性要求。

另一種觀點認為：GE-規則體現了另外一種倒置原則：“無論由推出一個命題的直接根據得到什么東西，都必須從該命題得到。”（[8]，第6 頁）8里德也持有類似的立場。（[15]，第563 頁）這個倒置原則與普拉維茨的不同，后者主張的是：借助δ E-規則的應用，不能推導出“多于”其直接根據的東西；而前者主張的是：借助δ E-規則的應用，不能推導出“少于”其直接根據的東西。GE-規則之所以也可以滿足后一種倒置原則的要求，是因為通過簡單的排列換位（permutation）就可以得到與它等價的推導：9“排列換位”可以被理解為是一種結構性的推導規則，它由兩條規則構成：（1）由Γ ?α 可得Γ,α ?γ ?γ；（2）由Γ,α ?γ 可得Γ ?α ?γ。

按設想，GE-協調性似乎不僅可以阻止具有強E-規則的異常算子，還應該可以阻止具有弱E-規則的算子。一個邏輯常項的GE-規則之所以能夠滿足協調性的要求，這完全是因為其GE-規則本身是由相應的I-規則“協調地導致的”。不過，到目前為止，“I-規則是如何‘協調地導致’GE-規則的”這個問題還沒有得到清晰地回答，這恰恰是本文的工作重點。另外，GE-協調性的一個明顯的問題是：只有當一個邏輯常項的E-規則就是其GE-規則時，它與相應的I-規則才是協調的。然而，需要我們證成的規則不僅僅是GE-規則，還包括普通E-規則。嚴格來說，只有析取的E-規則具有GE-形式，我們所熟悉的其他邏輯常項以及tonk 這樣的異常算子的E-規則都非天然地具有GE-形式，它們的E-規則通常僅僅是其GE-形式的其中一個實例而已。更嚴重的是，所有具有弱E-規則的算子都與對應的標準邏輯常項具有相同的I-規則，它們的E-規則因此都是同一個GE-形式的實例。故而，借助GE-規則的形式仍然無法回應弱E-規則的協調性問題。

GE-協調性標準僅僅陳述了一個重言命題：當且僅當由相應的I-規則協調地導致的GE-規則，才與該I-規則是GE-協調的，所以這種標準無法說明一個普通E-規則如何能夠與相應的I-規則是GE-協調的。要說明這一點，我們不僅要回答一個邏輯常項的I-規則是如何“協調性的導致”其GE-規則的，還要厘清其E-規則與GE-規則之間的關系。這都是以往研究者忽略的問題。為了回答前一個問題，本文將描述一個由I-規則“生成”GE-規則和E-規則的機制；為了說明后一個問題，我們需要區分GE-規則和Ge-規則，后者是直接由E-規則通過恰當的排列換位“生成”的普遍的E-規則。接下來，我們要描述這兩種生成機制。

3 邏輯常項的使用規則與生成機制

邏輯常項的I-規則和E-規則的普遍模式曾出于不同的目的被研究過。普拉維茨和施羅德-海斯特在上世紀八十年代各自借助普遍模式證明邏輯常項集{⊥,∧,∨,→}的完備性。（[11,20]）當然，I-或E-規則的普遍模式還被用于研究協調性問題（[4,6,9,14,15]），GE-協調性的描述同樣借助了消去規則的普遍模式。關于普遍模式的這些研究對于我們探討I-規則和E-規則之間的生成關系很有幫助。不過，以前討論的普遍模式還不夠“普遍”，這體現為：如果一個邏輯常項存在多個I-規則或E-規則時，它們也相應地有多個普遍模式，這種普遍模式可被稱為“分枝式的（bifurcated）”。例如，合取就有兩個E-規則：α ∧β ?α和α ∧β ?β。（有時候也寫作：α1∧α2?αi(i1,2)）合取消去的分枝式的普遍模式為：

也有學者建議采取下列這種單一的模式：（[15]，第566 頁）

這個單一的普遍模式的問題在于，它需要做出說明以便與下列兩種模式區分開來：

其中，（$-GE）類似析取的E-規則，（#-GE）是包含并行的（collateral）假設前提的E-規則（后文會再討論這種類型的前提）。而（∧-GE*）與這兩個規則都不同，它是兩個分枝式的GE-規則的合并，它要表達的思想是：如果無論由假設α還是由假設β都能夠推導出γ，則由α ∧β能夠推導γ。即使做出說明，采用類似（∧-GE*）這種普遍模式的表示方法，在刻畫合取和析取的I-規則和E-規則之間的關系時也不方便。因為析取的I-規則同樣有兩個，采用上述的單一表達方法就不方便構造相應的單一的I-規則。為了避免這個問題，我們區分了“可選性（alternative）”前提（假設）和“共同性的（joint）”前提（假設）：

(D1) 如果γ可由任意αi（1≤i ≤n）推出，則αi相對于αj（且1≤j ≤n）為γ的可選性前提，表示為：α1/.../αn ?γ。Γ{α1,...,αn}則為γ的可選性前提集。

(D2) 如果γ由α1,...,αn共同推出，則αi相對于αj（且1≤j ≤n）為γ的共同性前提，表示為：α1;...;αn ?γ。Γ{α1,...,αn}則為γ的共同性前提集。

除此之外，當然還需要區分“直言性（categorical）前提”和“假言性（hypothetical）前提”：

(D3) 如果αi是γ的前提且形如χ ?ξ（1≤i ≤n）（其中χ為關于ξ的一個推導的假設），則αi為γ的假言性前提。如果α1,...,αn都是γ的假言性前提，Γ{α1,...,αn}為γ的假言性前提集。

(D4) 如果αi（1≤i ≤n）是γ的前提且不包含假設，則是γ的直言性前提。如果α1,...,αn都是γ的直言性前提，則Γ{α1,...,αn}為γ的直言前提集。

基于上述四個概念的定義，我們可以將一個n-元命題邏輯常項δ的I-規則的普遍模式（schemata）描述如下10這里用分號“;”表示不同類型的前提，以便與逗號“,”表示的共同性前提區別開來。但是，這并不意味著，在不同類型的前提之間不可以存在共同關系。在具體的情形中，如果的確存在兩種類型的共同性前提，則需要使用逗號隔開來表示。：

其中δ(α1,...,αn)，且令p、q、r、s0,1,2,...m。通過對I-規則的普遍模式實例化，可以得到一些常見的（邏輯）常項的I-規則：

(3.1) 當p1，qrs0，ni2 時，該模式的實例就是合取的I-規則，即α1,α2?α1∧α2；

(3.2) 當r1，qrs0，nk2 時，該模式的實例就是析取的I-規則，即α1/α2?α1∨α2；

(3.3) 當q1，prs0，n2 且j1 時，該模式的實例就是蘊涵的I-規則，即χ1?α1?χ1→α1；

(3.4) 當q1，prs0，nj2 時（令χ2α1且χ1α2），該模式的實例就是等值的I-規則，即χ1?α1,α1?χ1?χ1?α1；

(3.5) 當q1，prs0，nj1 時（令α1⊥），該模式的實例就是直覺主義否定的I-規則，即χ1?⊥??χ1；

(3.6) 當p1，qrs0，ni1 時，該模式的實例就是雙重否定的I-規則，即α1???α1；

(3.7) 當p1，qrs0，n2 且i1 時，該模式的實例就是tonk 的I-規則，即α1?α1tonkα2；

給出（邏輯）常項的I-規則的統一的普遍模式之后，我們就可以描述一種生成機制（generating mechanism）。借助這種機制，由I-規則的普遍模式可以“生成”相應的E-規則的普遍模式，因而該機制也可被稱為“GE-生成機制”，其包含以下五條原則：

(I)I-規則普遍模式中的結論（）是相應的E-規則普遍模式中的直言性大前提；

(II)I-規則普遍模式中的共同的直言性前提（α1;...;αi）在相應的E-規則普遍模式中作為可選的假言性前提（/···/?γ），其中都是被解除的假設；

(III)I-規則普遍模式中的可選的直言性前提（/.../）在相應的E-規則普遍模式中分別作為共同的假言性前提（?γ;...;?γ），其中都是被解除的假設；

(IV)I-規則普遍模式中的共同的假言性前提（;...;）在E-規則普遍模式中作為以直言性前提與新的假言性前提的可選的組合（(?γ)/.../(?γ)）；

(V)I-規則普遍模式中的可選的假言性前提（/.../）在E-規則普遍模式中作為以直言性前提與新的假言性前提的共同的組合（([]?γ);...;([]?γ)）；

(VI) 在E-規則的普遍模式中，γ是唯一的結論。

按照GE-生成機制的原則，由（邏輯）常項δ的I-規則的普遍模式就可以生成下面下列E-規則的普遍模式（其中，“”被稱為E-規則的“大前提”，其他前提都被稱為“小前提”）：

類似地，對δ的E-規則的這個普遍模式進行實例化以及借助適當的排列換位處理，就可以生成一些常見的（邏輯）常項的GE-規則及其普通的E-規則：

(3.1’) 當p1，qrs0，ni2 時，該模式的實例就是合取的GE-規則，即α1∧α2,[α1]/[α2]?γ ?γ；當γα1（或α2）時，就得到其兩條E-規則，即α1∧α2?α1和α1∧α2?α2；

(3.2’) 當r1，qrs0，nk2 時，該模式的實例就是析取的GE-規則，即α1∨α2,[α1]?γ,[α2]?γ ?γ；該規則同時也是析取的E-規則。

(3.3’) 當q1，prs0，n2 且j1 時，該模式的實例就是蘊涵的GE-規則，即χ1→α1,χ1,[α1]?γ ?γ；當γα1時，就得到其E-規則，即χ1→α1,χ1?α1，這就我們熟悉的分離規則；

(3.4’) 當q1，prs0，nj2 時（令χ2α1且χ1α2），該模式的實例就是等值的GE-規則，即χ1?α1,(χ1,[α1]?γ)/(α1,[χ1]?γ)?γ；當γα1或者γχ1時，就得到其兩條E-規則，即χ1?α1,χ1?α1；χ1?α1,α1?χ1；

(3.5’) 當q1，prs0，nj1 時（令A1⊥），該模式的實例就是直覺主義否定的GE-規則，即?χ1,χ1,[⊥]?γ ?γ；當γ⊥時，就得到其E-規則，即?χ1,χ1?⊥；

(3.6’) 當p1，qrs0，ni1 時，該模式的實例就是雙重否定的GE-規則，即??α1,α1?γ ?γ；當γα1時，就得到其E-規則，即??α1?α1。

借助GE-生成機制，我們可以由一個（邏輯）常項的I-規則的普遍模式生成其E-規則的普遍模式，接著得到相應的GE-規則和E-規則，當然也可以直接借助這種機制，由它的I-規則生成它的GE-規則以及E-規則。當我們將GE-生成機制應用于tonk 時，就會發現情況明顯異常：由tonk 的I-規則所生成的GE-規則是α1tonkα2,α1?γ ?γ，而再由該GE-規則得到的E-規則卻是α1tonkα2?α1。這表明，tonk 的E-規則（tonkE）并不是由它的I-規則生成的。這是因為GE-生成機制包含了一種協調性的要求：由該機制生成的GE-規則與相應的I-規則在滿足倒置原則的意義上是協調的。基于該生成機制的協調性（“GM-協調性”）可定義如下：

(HGM)（邏輯）常項δ的E-規則與其I-規則是協調的，當且僅當其E-規則是由其I-規則所生成的GE-規則的實例。

由于這種協調性仍然是通過GE-規則來表達的，它蘊涵了GE-協調性。不過，它的內容更為豐富：首先、它能夠幫助我們排除tonk 這樣的異常算子，因為tonk的E-規則并不是由其I-規則所生成的GE-規則的實例；其次、它還為一個（邏輯）常項的I-規則如何“協調地導致了”GE-規則提供了說明；再次、它能夠保證：并非一個（邏輯）常項的任意具有GE-形式的規則都是與其I-規則相協調的GE-規則。不過，無論GE-協調性還是GM-協調性，都還不足以解決E-規則的證成問題，因為它們無法排除具有弱E-規則的算子。接下來，我們要提出另外一種生成機制來彌補這個不足。

4 基于Ge-規則生成機制的協調性

為了說明E-規則與GE-規則之間的關系，我們需要借助另外一種普遍的E-規則，即Ge-規則作為對照。Ge-規則是按照如下機制生成的：令1,...,χn ?ξ為任意常項δ的E-規則，首先將結論ξ通過排列換位，作為一個新的假言性前提“[ξ]?γ”中被該E-規則的應用解除的一個假設，其次將原結論的位置用γ填充，由此得到δ的Ge-規則為：

借助上述生成機制，我們可以由一些常見的（邏輯）常項的E-規則生成它們相應的Ge-規則：

(4.1) 合取的E-規則通常分為兩條，即α ∧β ?α和α ∧β ?β。由上述生成機制可得兩條Ge-規則：α ∧β,[α]?γ ?γ和α ∧β,[β]?γ ?γ；我們可以將這兩條合并為一條，即：α ∧β,([α]/[β])?γ ?γ。

(4.2) 析取的E-規則本身既是其GE-規則，也是其Ge-規則。

(4.3) 蘊涵的E-規則為：α →β,α ?β。由上述生成機制可得其Ge-規則：α →β,α,[β]?γ ?γ。

(4.4) 等值的E-規則通常分為兩條，即α ?β,α ?β和α ?β,β ?α。由上述生成機制可得其Ge-規則：α ?β,α,[β]?γ ?γ和α ?β,β,[α]?γ ?γ。與合取相似，我們可以將這兩條規則合并，即：α ?β,(α,[β]?γ)/(β,[α]?γ)?γ。

(4.5) 直覺主義否定的E-規則為：?α,α ?⊥。由上述生成機制可得其Ge-規則：?α,α,[⊥]?γ ?γ。

(4.6) 經典的雙重否定的E-規則為：??α ?α。由上述生成機制可得其Ge-規則：??α,[α]?γ ?γ。

如果一個（邏輯）常項δ的Ge-規則中的直言性前提χ1,...,χn是δ的I-規則的假言性前提中被解除的假設，ξ是其后件或者直言性前提，那么該Ge-規則就恰好是它的GE-規則。此時，常項δ的Ge-規則就與它的I-規則是協調的。于是，我們提出另外一種協調性概念（“Ge-協調性”）：

(HGe) 一個邏輯常項δ的E-規則與其I-規則是協調的，當且僅當由該E-規則生成的Ge-規則就是由該I-規則生成的GE-規則。

盡管Ge-協調性是以GE-協調性為基礎的，但它與后者并不是一回事。它不僅可以阻止具有強E-規則的異常算子，還可以阻止具有弱E-規則的算子。就第一個方面而言，Ge-協調性標準可以排除tonk 及其類似異常算子，因為它們的Ge-規則都與它們的GE-規則不相等價。具體分析如下：

(4.7) tonk 的E-規則為：αtonkβ ?β。由上述生成機制可得tonk 的Ge-規則：αtonkβ,[β]?γ ?γ；而tonk 的GE-規則為：αtonkβ,[α]?γ ?γ。

(4.8) tonk>的E-規則為：α ?tonk>?β。由上述生成機制可得tonk>的Ge-規則：α ?tonk>,[β]?γ ?γ；而tonk>的GE-規則為：tonk>,α,[β]?γ ?γ。

(4.9)

(4.10) 的E-規則為：α ??β。由上述生成機制可得的Ge-規則：α ?,[β]?γ ?γ；而的GE-規則為：,(α,[β]?γ);([α]?γ/(β,[α]?γ))?γ。

(4.11) super-tonk 的E-規則為：α ?super-tonk?β。由上述生成機制可得super-tonk 的Ge-規則：α ?super-tonk,[β]?γ ?γ；而super-tonk的GE-規則為：super-tonk,([α]?γ/(φ,[ψ]?γ))?γ。

上述異常算子的Ge-規則與它們的GE-規則并不等價。這里所列舉的算子表面上可分為兩類：tonk 和其他算子。tonk 的Ge-規則的大前提是其I-規則的結論，而其他算子的Ge-規則的大前提并不是其I-規則的結論。這種區別對于導出平凡化的結果來說并不重要，但是可能會對于協調性的判定產生一些影響。至少從表面上看，其他算子的GE-規則和Ge-規則在形式上明顯不同，而tonk 的Ge-規則更容易被當作普遍的E-規則，因而證明它并不等價于相應的GE-規則就很重要。這種證明并不復雜：令α是tonk 的I-規則應用的前提，除非αβ，否則借助GE-規則無法推導β，但是借助Ge-規則卻可以推出β。

其他異常算子的Ge-規則并不是常見的E-規則，因為它們的E-規則中的大前提并非形如“”的直言性的前提，但僅憑借這一點還不足以說明它們的Ge-規則與相應的I-規則不協調。它們的不協調性乃是因Ge-規則強于對應的GE-規則造成的。這里僅以super-tonk 為例，將它的GE-規則應用于super-tonkI-規則的結論，只能得到α或者在φ成立的前提下得到ψ，這恰恰是super-tonkI-規則應用的前提，但是借助Ge-規則就可以得到更多的結果，因為作為其結果的β可以是I-規則的前提，也可以是其他公式。與這些異常算子的E-規則非常相似，經典否定的E-規則也不是常規的。經典否定與直覺主義否定具有相同的I-規則，但經典否定的E-規則是：～α ?α ?α（或經典的歸謬律：～α ?⊥?α），這與直覺主義否定的E-規則（即?α,α ?⊥）不同，否定公式在經典否定的E-規則中并不是作為直言性大前提出現的。它的Ge-規則是：～α ?α,[α]?γ ?γ，而直覺主義否的Ge-規則是：～α,α,[⊥]?γ ?γ，這也是這兩種否定的共同的GE-規則。盡管經典否定的E-規則并沒有導致平凡性，但它仍然強于其GE-規則，進而強于其I-規則，因為在沒有荒謬性規則（即⊥?α）的情形下，直覺主義否定的E-規則應用于其I-規則的結論只能推導出在其前提中已經被推導出來的東西，即⊥；但借助經典否定的E-規則卻可以進一步推導出α。

Ge-協調性的要求不僅可以阻止具有強E-規則的算子，還可以克服GE-協調性和GM-協調性的不足，即阻止具有較弱E-規則的算子。因為Ge-規則是直接由它的E-規則通過排列換位生成的，它只是將其結論轉變為假言性前提中的假設。如果（邏輯）常項δ的E-規則是弱的，這意味著它相對于標準的E-規則而言較弱，即借助該規則由推導出來的東西要“少于”借助標準E-規則推導出來的東西。由δ的標準E-規則生成的Ge-規則與其GE-規則是等價的（相同的），因而由較弱的E-規則所生成的Ge-規則同樣弱于該GE-規則。于是，我們只需要通過比較一個（邏輯）常項的Ge-規則和GE-規則是否等價就可以判定它的E-規則與其I-規則是否協調。

這里以量子析取為例，經典析取的E-規則允許在推導中使用并行前提，它的GE-規則（同時也是它的Ge-規則）可以表示為：α∨β,((Γ,α)?γ;(Δ,α)?γ)?γ（其中Γ,Δ 允許非空）。需注意，這里的Γ 和Δ 中的公式相對于γ而言是并行前提，γ被允許由α（或β）結合Γ（或Δ）中的公式推導出來。并行前提與共同性前提不同，它們并不必定在I-規則中出現，不過I-規則本身可以包含并行前提：Φ,α/β ?α ∨β（其中，Φ 可不為空）。并行前提集應該被理解為一個演繹推導的背景（相對而言，借助矢列演算的方式來表達并行前提（集）更為方便）。由于經典析取的規則允許使用并行前提，在{∧,∨}這個演繹系統中就可以推導出經典析取的分配律（α ∧(β ∨γ)?(α ∧β)∨(α ∧γ)），其推導過程如下：

量子析取的E-規則不允許使用并行前提，因此它的E-規則為：αβ,((Γ,α)?γ;(Δ,β)?γ)?γ（其中Γ,Δ 必須為空）。該規則本身也是量子析取的Ge-規則。如果我們將上述推導過程中的經典析取全部替換為量子析取，則推導不成立，這是因為對“(α ∧β)(α ∧γ)”的推導需要使用β和γ以外的并行前提（即α），但這樣一來就不能直接應用量子析取的E-規則。因此在{∧,}這個演繹系統中，量子析取的分配律（α ∧(βγ)?(α ∧β)(α ∧γ)）失效。但是，該分配律在{∧,,∨}這個擴張的演繹系統中則可以推導出來，過程如下：

在這個推導中，最后一步應用了經典析取的E-規則推導出結論，從而避免了直接應用量子析取的E-規則。這個結果也說明，添加經典析取，會對{∧,}這個演繹系統造成非保守的擴張。但與tonk 不同，這種非保守擴張并不會導致平凡化問題。雖然在這里造成非保守性問題的是經典析取，但是由于經典析取的Ge-規則本身就是它的GE-規則，經典析取的E-規則與它的I-規則是Ge-協調的。量子析取的Ge-規則禁止了并行前提，在一致的演繹系統中，僅由{β}（或{γ}）推導出來的結果無疑要少于由Γ∪{β}（或Δ∪{γ}）（其中Γ,Δ）。所以，量子析取的Ge-規則要弱于經典析取的Ge-規則，它相對于同樣的I-規則而言是不協調的。

5 結論

在證明論語義學中，邏輯常項的使用規則的證成面臨著tonk-問題的嚴峻挑戰。解決這個問題，需要尋找一種恰當的協調性標準。本文描述了由邏輯常項的I-規則生成其GE-和E-規則的機制，以及由其E-規則生成Ge-規則的機制。借助第一個機制，GE-規則由相應的I-規則“協調地導致”的方式得到清晰地描述，借助第二機制，弱化E-規則與標準E-規則在協調性上的區別得以明確。基于GE-生成機制的GM-協調性概念可以替代保守性要求等標準，阻止具有強E-規則的異常算子，但它還是無法處理弱E-規則的不協調性問題。Ge-協調性是這兩種生成機制共同蘊涵的后果，它進一步將邏輯常項的使用規則的協調性歸結為其Ge-規則與GE-規則之間的等價性，它不僅可以像以往的協調性標準一樣阻止具有強E-規則的異常算子，還可以彌補以往的協調性標準的不足，明確了具有弱E-規則的算子的不協調性。比較而言，Ge-協調性要求能夠更好地解答tonk-問題以及邏輯常項的使用規則的證成問題。