逻辑常项的使用规则的生成与证成

周志荣

在证明论语义学中，逻辑常项的意义是通过它的两个核心的使用规则来刻画的，那就是引入规则和消去规则（以下简称为“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-问题以及逻辑常项的使用规则的证成问题。