协调、一致与一阶公理系统的强完全性

邓雄雁，胡泽洪

（华南师范大学政治与行政学院，广东广州510631）

协调、一致与一阶公理系统的强完全性

邓雄雁，胡泽洪

（华南师范大学政治与行政学院，广东广州510631）

在公理系统中演绎定理是连接一致性和协调性的桥梁。对于带演绎定理的公理系统，可以证明公式集的一致性和协调性是等价的。在不带演绎定理的一阶公理系统中，一致性和协调性的差异集中体现在强完全性证明过程中。基于一致性的证明不依赖演绎定理，但基于协调性的强完全性证明多处受演绎定理束缚。文中将给出一个松绑方案，基于协调性上证明一阶公理系统QC1的强完全性。

一致；协调；演绎定理；强完全性

一致、协调和演绎定理

一致和协调有两个层面：一是系统本身的一致与协调，令S是公理系统，称S协调⇔①S⊥，称S是一致系统⇔S的定理集Th（S）是S一致集；二是公式集的一致和协调，称Φ是S一致集⇔对所有有穷集Ψ⊆Φ，S¬∧Ψ，称Φ是S协调集⇔ΦS⊥②。

按照直观理解，一个“好”的推理要求不能推出矛盾“⊥”。由这个标准，公式集的一致性达不到这个要求。因为可能出现这种情况，Φ├⊥但Φ还是一致的。例如，在某些系统中，比如下文的QC1，公式集Φ＝｛A，∀xA→∀xB，∀xA→∀x¬B｝├QC1⊥，但是不存在有穷集Ψ⊆Φ，使得QC1¬∧Ψ。相对来说，一个协调集Φ肯定推不出矛盾“⊥”，所以，协调更符合直观。然而，在形式系统中特别是基本模态系统的完全性证明中用得较多的却是一致性。个中原因值得探讨。

一致和协调性的逻辑性质跟系统是否有演绎定理密切相关。按照是否有一般性演绎定理（下文简称为演绎定理），公理系统可以分为两类：一类是有演绎定理的系统，一类是没有演绎定理的系统。鉴于本文主要考虑一阶系统情况中协调性和演绎定理以及其完全性证明三者之间的关系，有必要把这些系统简要的列出来。较为常见的QC1是由下列公理模式和推理规则构成的形式系统：

（一）公理模式：

1，A→B→A

2，（A→B→C）→（A→B）→A→C

3，¬（A→¬B）→（B→A）

4，∀xA→A（t／x），其中t对x代入自由，

5，∀x（A→B）→A→∀xB，x在A中不自由

（二）推理规则：

1，分离规则（MP），从A和A→B可以推出B

2，全称概括规则（UG），从A可以推出∀xA

Φ├QC1A指A为公式集Φ的QC1语法后承，也可称为从Φ到A的QC1推演（在本文里，除非特别说明，用Φ├A表示Φ├QC1A）。当Φ为空集时，A为QC1定理，记为├A，也称A在QC1中可证。Φ⊨A指对一阶语言L的任一解释M＝＜D，H＞和Μ上的任一指派σ，M⊨Φ［σ］⇒M⊨A［σ］；当Φ为空集时，A为有效式，记为⊨A。其中D为非空个体域；H为一阶语言L的非逻辑符号集到Dn的一个映射。若s是L的特征符号，也可用sM表示H（s）。

QC2的公理模式1－4与QC1的相同，模式5是：A→∀xA，其中x在A中不自由；模式6：∀x（A→B）→∀xA→∀xB；模式7：∀x1…∀xnA，A是前六类公理之一，x1…xn是任意变元符号且n≥1；推理规则只有MP。类似于QC2的系统有叶峰的系统［7］，李小五的P［4］。

QC3的公理模式和推理规则与QC1相同，但对UG进行限制，规定只允许对系统定理运用UG。类似系统有陈慕泽、余俊伟的Q系统［2］。

QC2和QC3、QC1对于UG规则的不同使用所导致的结果就是：QC2和QC3有演绎定理，而QC1没有演绎定理。陈慕泽详细论述了演绎定理与UG的关系［1］，这里不再赘述。

与一阶系统情况类似，对于含有必然化规则（RN）的模态系统，如果RN只运用于定理集，则这个系统有演绎定理；如果RN运用于前提集，则没有的演绎定理。

但QC1有受限制演绎定理：令A和B是任意L公式，Φ是L任公式集，若Φ∪｛A｝├B，并且演绎对涉及A中的自由变元没有使用概括，那么Φ├A→B。证明从略。（下文中凡是出现类似的较为常识性的定理、引理或结论，这些定理、引理或结论的证明在数理逻辑著作中均可找到，此处就不再赘述）

推论：若Φ∪｛A｝├B，且A是闭公式，则Φ├A→B。

一致和协调的逻辑性质须从如下两个方面加以探讨。

一、系统本身的协调性和一致性：S一致⇔S协调。

证明：“⇒”设S一致。据系统一致定义，Th（S）是S一致的。∵∅是任何集合的有穷子集，∴据公式集一致定义，S¬∧∅③。 ∴S⊥，也就是S协调。

二、公式集的协调性和一致性：在有演绎定理的系统S中，Φ是S一致⇔Φ是S协调；在无演绎定理的系统S中，Φ是S－协调⇒Φ是S一致，反向不成立。

证明：“⇒”，设Φ是S一致，假如Φ不是S协调，则Φ├s⊥，∵推演的长度是有穷的，∴存在有穷集｛A1…An｝⊆Φ，使得｛A1…An｝├s⊥，运用演绎定理n次得，├sA1→…→An→⊥（无演绎定理的系统在此处通不过），即├s（A1∧…∧An）→⊥，∵├PCA→B⇒├PC¬B→¬A有├s¬⊥→¬（A1∧…An），再据├s⊥，∴├s¬（A1∧…∧An），矛盾于题设。

“⇐”，设Φ是S协调但不S一致，则存在有穷集Ψ⊆Φ，使得├s¬∧Ψ，易见Φ├s¬∧Ψ且Φ├s∧Ψ，∵├PC¬A→A→B，∴Φ├s⊥，矛盾。

上述结果表明，对于系统本身的协调性和一致性，我们可以等价地运用这两个概念，无需顾忌系统是否有演绎定理。但对于公式集的协调性和一致性，必须分情况对待：对于有演绎定理的系统，比如QC2与QC3，公式集的一致性和协调性是等价的；但对于只有受限制的演绎定理的系统，比如QC1或基本模态系统，协调性强于一致性。造成这种差异的关键在于｛A1…An｝├⊥⇒├A1→…→An→⊥的推导过程中前者可以运用演绎定理而后者不能。

QC1或基本模态系统中的公式集的一致和协调的区别集中体现在这些系统的强完全性证明过程中。强完全性指：Φ⊨A⇒Φ├A；弱完全性指：⊨A⇒├A。

对于这些系统的强完全性证明有两种版本：一种是基于公式集的一致性，例如通行的模态逻辑的强完全性证明，如Hughe，G.E.and Cresswell，M.J或LI Xiao－wu的证明［8，10］，其特点是证明过程无需运用演绎定理；一种是基于公式集的协调性，汉密尔顿，刘壮虎基于协调性基础上证明了QC1弱完全性［3，5］。笔者尚未看到基于协调性的基本模态系统的强完全性证明。基于协调性的QC1强完全性证明也具有一定难度，本文尝试用亨金方法［9］证明QC1强完全性。

基于协调性的QC1强完全性证明

基于协调性QC1强完全证明要解决如下问题，第一，ΦA⇒Φ∪｛¬A｝协调，是否成立，下文命题1的证明过程展示这个结论是不成立的；第二，Φ协调⇒Φ可满足，是否成立，这是证明完全性的核心问题。第二个问题又分为两个方面：首先，任何一个协调集与亨金公式集的并是否还是协调集；其次，任何一个协调集与亨金公式集的并能否扩充为极大协调集。这三个问题的共同特点是均要牵涉演绎定理。但相对于一致性的证明，在这三种情形中均不需演绎定理。基于协调性QC1强完全性证明要依赖演绎定理，已经知道QC1系统只有受限制的演绎定量。如何化解这个矛盾是解决第二、三个问题的关键。我们的策略是尽量避免使用演绎定理：或者弱化使用演绎定理情形，只用受限制的演绎定理；或者把关于协调性的讨论转化为关于一致性的讨论。

下面开始证明Φ⊨A⇒Φ├∀，从命题1到命题6分成六个步骤。

引理1：对任L协调集Φ和任意L公式A，它的自由变元是x1…xm，Φ├A⇔Φ├∀x1…∀xmA。

证明：“⇒”，对A的自由变元个数进行归纳，当m＝1，A只有一自由变元x，若Φ├A，UG，则Φ├∀x1A；当m＞1，假设对于m－1成立，证对m成立，若Φ├A，由归纳假设有Φ├∀x1…∀xm－1A，再UG，有Φ├∀x1…∀xmA。

“⇐”，若，Φ├∀x1…∀xmA，对m作类似归纳，∵任一变元对自身作代入总是代入自由的，∴再与公理4，MP m次，易得Φ├A。

命题2，任何一个L协调集与L1亨金公式集的并是一致。⑤

引理2，等值置换定理：令B是A的子公式，A［B／C］是用C置换A中的B的某个出现得到的公式，则├B↔C＆├A⇒├A［B／C］

引理3，设Φ是L一致，增加可数无穷个新常元来膨胀原有语言，Φ作为膨胀语言中L1的公式集仍是一致的。

枚举膨胀语言中的每一公式和变元集中的每一变元构成的序对如下：

＜A1，x1＞，…，＜An，xn＞，…

定义亨金公式：B1＝¬∀x1A1→¬A1（c1／x1）。其中，c1是膨胀语言中第一个不在A1中出现的新常元。假设Bn已经构造完毕，令Bn＋1＝¬∀xn＋1An＋1→¬An＋1（cn＋1／xn＋1）。其中cn＋1是L1中第一个不在｛A1，…，An＋1｝中出现的新常元，规定语言L1是可数的，上述构造是能完成的。令Ψ＝｛B1，…，Bn｝，则Ψ称为L1亨金公式集。

引理4，Φ∪｛A｝不一致⇔存在有穷集Θ⊆Φ使得├∧Θ→¬A。

现证命题2：设任一L协调集Φ，如前所证，由Φ是协调的，可知Φ是一致的，据引理3，Φ作为膨胀语言中L1的公式集仍是一致的，下证Φ与L1亨金公式集Ψ的并Φ∪Ψ还是一致的。

证明：假设不一致，则总存在n∈א，使得1≤n且Φ∪｛B1…Bn＋1…｝不一致。

极限情况：Φ∪｛B1｝不一致，由引理4，存在有穷集Ξ⊆Φ使得├¬Ξ→¬B1。据B1的构造和├PCA→B∧C⇒├PCA→B＆├PCA→C有├∧Ξ→¬∀x1A1⑴＆├∧Ξ→A1（c1／x1）⑵，令y1是第一个不在Φ，A1，和∧Ξ→A1（c1／x1）中出现的变元，用y1替换每个c1的出现，则├（∧Ξ→A1（c1／x1））（y1／c1），∵据B1规定，c1不在Φ中出现，则c1肯定不在∧Ξ中出现，∴├∧Ξ→A1（c1／x1）（y1／c1）⑶，据亨金公式构造规定，c1也不在A1中出现，∴A1（c1／x1）（y1／c1）＝A1（y1／x1），再由⑶和引理2有├∧Ξ→A1（y1／x1），UG，得├∀y1（∧Ξ→A1（y1／x1））⑷，∵y1不在∧Ξ中出现，∴再据公理5与⑷，MP，得├∧Ξ→∀y1A1（y1／x1）⑸，∵由约束变元易字定理∀y1A1（y1／x1）↔∀x1A1，∴由⑸和引理2得├∧Ξ→∀x1A1⑹，由⑴⑹和├PCA→B＆├PCA→C⇒├PCA→B∧C得├∧Ξ→¬∀x1A1∀x1A1，再由├PCA→⊥⇒├PC¬A，有├¬∧Ξ矛盾于Φ一致。

一般情况：∵Φ∪｛B1｝一致的，∴总存在某个最小n使得Φ∪｛B1…Bn…｝是一致，现在Φ∪｛B1…Bn＋1…｝不一致，据引理4，存在有穷集Ξ⊆Φ∪｛B1…Bn…｝使得├∧Ξ→¬Bn＋1，据Bn＋1构造规则，得├¬ Ξ→¬∀xn＋1An＋1⑴和├∧Ξ→An＋1（cn＋1／xn＋1），令yn＋1是第一个不在Φ，An＋1和∧Ξ→An＋1（cn＋1／xn＋1）中出现的变元，用yn＋1替换每个cn＋1的出现。据语言L1是可数语言和集合论知识，这是可以做到的，则├（∧Ξ→An＋1（cn＋1／xn＋1））（yn＋1／cn＋1）。类似于上述根据情况证明过程，有├∧Ξ→An＋1（yn＋1／xn＋1）。由UG，得├∀yn＋1（∧Ξ→An＋1（yn＋1／xn＋1）），再由yn＋1不在∧Ξ中出现和公理5，MP，有├∧Ξ→∀yn＋1An＋1（yn＋1／xn＋1）；由易字定理和引理2得├∧Ξ→∀xn＋1An＋1⑵；由⑴⑵易得├¬∧Ξ，矛盾于Φ∪｛B1…Bn…｝一致。

命题3，任何一个协调集与亨金公式集的并能扩充为亨金集。

引理5，紧致性定理：Φ是一致的⇔Φ的所有有穷子集是一致的。

引理6，林登保姆引理：任何一致集都可以扩充为极大一致集。

先证：⑴Ψn是一致的。

据设定条件，已知Φ＝Ψ0是一致的。对任意n＞0，归纳设定Ψn是一致的。下证Ψn＋1是一致的。为此考虑Ψn∪｛An｝的一致性。

情况1 Ψn∪｛An｝是一致的：此时Ψn＋1＝Ψn∪｛An｝，∴Ψn＋1是一致的。

情况2 Ψn∪｛An｝不是一致的：此时Ψn＋1＝Ψn∪｛¬An｝。假设Ψn＋1不是一致的，则据本情况的设定条件和刚才的假设，Ψn∪｛An｝不是一致的，Ψn∪｛¬An｝不是一致的，∴据引理4，存在有穷子集Θ，Ξ⊆Ψn使得├∧Θ→¬An，├∧Ξ→An。易得，├¬（∧Θ∧∧Ξ），∵Θ∪Ξ是Ψn的有穷子集，∴Ψn不是一致的，与归纳设定矛盾。

再证：⑵Σ是极大一致集。

任给A∈L1，总存在n∈א使得A＝An。据Ψn＋1的构造，An或¬An总有一属于Ψn＋1⊆Σ，∴Σ是极大的。假设Σ不是一致的，则据引理5，存在有穷子集Θ⊆Σ使得Θ不是一致的。但Σ的每一有穷子集显然是某个Ψn⊆Σ的子集，∴再据定理5，易见Ψn不是一致的，矛盾于⑴。［10］124－125

令

可以看到，协调集的一致扩充过程中始终未曾用到演绎定理，这也是把关于协调性的讨论转化为关于一致性的讨论根据所在。

命题4，亨金集Σ有典范解释。

定义一致集Σ的解释和指派σ如下：⑴定义D是膨胀一阶语言L1的所有项的集合；⑵对每一常元c，定义c＝c；⑶对n元函数F，Ft1…tn＝Ft1…tn；⑷对n元谓词符号P，〈t1….tn〉∈P⇔Pt1…tn∈Σ；⑸对任意变元，σ（x）＝x

引理7，M⊨A［σ］⇔A∈Σ，对于所有A∈L1，所以有M⊨Σ［σ］。验证从略。

引理8：令L1是L的膨胀语言，令解释M是相对于原语言L的规约，使得⑴DL＝DL1，⑵HL（s）＝HL1（s），对每一特征符号s。则对每一L公式A和每一指派σ，M1⊨A［σ］⇔M⊨A［σ］。

命题5，在亨金集里，Φ∪｛¬∀x1…∀xmA｝可满足⇒Φ∪｛¬A｝可满足。⑥

引理9：对任极大一致集Σ，｛A，A→B｝∈Σ⇒B∈Σ。

引理10，代入自由引理，令t对A中的x自由，任给解释M和σ，使得σ（a／x）（x）＝tM则M⊨A（t／x）［σ］⇔M⊨A［σ（a／x）］。其中σ是任一解释M的指派，σ（a／x）使得对任一变元y，若y≠x，则σ（a／x）（y）＝σ（y）；若y＝x，则σ（a／x）（y）＝a。

现证命题5：设Φ∪｛¬∀x1…∀xmA｝可满足，往证Φ∪｛¬A｝是可满足的。

一方面：由¬∀x1…∀xmA∈Σ⑴，且具有¬∀xA的形式，据亨金公式集的构造，总可以找到一亨金公式¬∀xnAn→¬An（cn／xn）与¬∀x1…∀xmA对应。令x1＝xn，则∀x2…∀xmA＝An，显然¬∀x1…∀xmA→¬∀x2…∀xmA（c1／x1）∈Σ⑵。由⑴⑵和引理9，可得¬∀x2…∀xmA（c1／x1）∈Σ⑶。¬∀x2…∀xmA（c1／x1）又具有¬∀xA形式，不难找到一亨金公式与之对应，使得¬∀x2…∀xmA（c1／x1）→¬∀x3…∀xmA（c1／x1）（c2／x2）∈Σ⑷。再据引理9，⑶⑷，有¬∀x3…∀xmA（c1／x1）（c2／x2）∈Σ。重复上述步骤m次，最终可得¬A（c1／x1）…（cm／xm）∈Σ。据引理7，¬ A（c1／x1）…（cm／xm）是可满足的⑸。

命题6，Φ⊨A⇒Φ├A。

如本文所述，一致和协调的区别主要是指公式集层面上的，且只有在不带演绎定理的系统中讨论二者的区别才是有意义的。对于有演绎定理的公理系统，公式集的协调性和一致性通过演绎定理过渡，从而二者是等价的。在不带演绎定理的系统中，二者的区别主要是体现在强完全性证明过程当中。基于协调性的强完全性证明对演绎定理依赖性比较强，基于一致性的强完全性证明不依赖于演绎定理。还可以看到，协调集不一定能扩充为极大协调集。因为在极大扩充的过程中要受到演绎定理的束缚。只有对于有演绎定理的系统，协调集可以扩充为极大协调集。值得提出的是，任一协调闭式集可以扩充为极大协调闭式集，不论系统是否带演绎定理。原因是在扩充过程中可以运用受限制的演绎定理。但是，本文只是给出了一种基于协调性的QC1强完全性证明，基于协调性的基本模态系统强完全性证明尚待解决。

注 释：

① 为了简洁，本文用“⇔”表示元语言意义上的“…当且仅当…”，用“⇒”表示“若…，则…”，用“∵”表示“因为…”，用“∴”表示“所以…”，用“＆”表示“并且”。

② 在不引起混淆情况下S和下标s均可省略。

③ 定义：∧∅＝⊥。∧Φ＝⊥成立的条件是：如果∧Φ所有的合取枝都为真，那么∧Φ为真。显然当合取枝数目为零时，条件句前件为假，条件句空洞成立。

④ 这个定理和下文中将出现的├PC¬A→A→B以及导出规则├PC¬B→¬A⇒├PCA→B或├PCA→B⇒├PC¬B→¬A等是命题逻辑中定理，用├PC标示，以示区别。在一阶逻辑中或模态逻辑可以使用命题逻辑中的定理或导出规则，而不用考虑演绎定理的束缚，因为命题逻辑中的定理都是一阶逻辑或模态逻辑的定理，而命题逻辑的导出规则是依据定理转化而来的。依据前面的讨论，对定理集作推演不会受到演绎定理的束缚。

⑤ 从这里开始，我们把关于协调集的讨论转化为一致集的讨论，由命题6，再从一致性返回到协调性。

⑥ Φ∪｛¬∀x1…∀xmA｝可满足⇒Φ∪｛¬A｝是可满足，在一般情况下不成立。

⑦ 设σ是任一解释M的指派，定义σ（a／x）使得对任一变元y，若y≠x，则σ（a／x）（y）＝σ（y）；若y＝x，则σ（a／x）（y）＝a。

［1］ 陈慕泽.全称概括规则和受限制的演绎定理——国内数理逻辑教材中的一个问题.浙江社会科学，2002（2）：99－101.

［2］ 陈慕泽，余俊伟.数理逻辑基础.北京：中国人民大学出版社，2003.

［3］ 汉密尔顿.数理逻辑.朱水林，译.上海：华东师范大学出版社，1986.

［4］ 李小五.数理逻辑.广州：中山大学出版社，2005.

［5］ 刘壮虎.逻辑演算.北京：中国社会科学出版社，1993.

［6］ 余俊伟.形式系统的可靠性和完全性问题.湖南科技大学学报：社会科学版，2005，1：25－29.

［7］ 叶峰.一阶逻辑与一阶理论.北京：中国社会科学出版社，1994.

［8］ 胡泽洪.蕴涵刍议.华南师范大学学报：社会科学版，2006（5）：1－6.

［9］ 王健平.实质蕴涵与自然语言中的相关蕴涵命题分析.华南师范大学学报：社会科学版，2005（3）：11－18.

［10］ HUGHE G E，CRESSWELL M J.A New Introduction to Modal Logic.London：Routedge，1996.

［11］ HENKIN L.The Completeness of The First－order Functional Calculus.The Journal of Symbolic Logic，1949，14：159－166.

［12］ LI XIAO－WU.A Course in Modal Logic（Electronic version）.Guangzhou：Institute of Logic and Cognition of Sun Yat－sen University，2008.

【责任编辑：赵小华】

B812.23

A

1000－5455（2010）03－0112－05

2009－11－20

邓雄雁（1979—），男，湖南衡南人，华南师范大学政行学院博士研究生；胡泽洪（1964—），男，湖南双峰人，华南师范大学政行学院教授、博士生导师。