模态系统MV 及其可靠性与完全性

姚从军，徐佳敏

（湘潭大学哲学系，湖南湘潭 411105）

我们考虑有这样一个模型类，它的每个模型中的每个可能世界要么自身是一个死点，要么至少可及一个死点。我们把满足这样性质的模型类记为★模型类。

我们将★模型类刻画的系统称为MV 系统。MV 系统是由K 系统加上MV 公理组成的，其中MV 公理表示为MLp ∨Lp，K 公理表示为L（p→q）→（Lp→Lq）。特别说明：本文用L 表示必然性算子，M 表示可能性算子。［1］60

在证明之前，先了解什么是模型以及如何赋值的问题。模型是一种研究正规命题模态系统的重要工具，由三元组〈W，R，V〉构成，其中W 是一个非空集合，代表可能世界集，R 是W 上的二元关系；V是真值指派，其中真值指派遵循赋值定义。［2］17-34

【赋值定义】

［V～］对于任意合式公式α 和任意w∈W，如果V（～α，w）=1，那么V（α，w）=0；反之，如果V（α，w）=1，则V（～α，w）=0。

［V∨］对于任意合式公式α、β 和任意w∈W，如果V（α，w）＝1 或者V（β，w）＝1，那么V（α∨β，w）＝1；否则V（α∨β，w）＝0。

［V·］对于任意合式公式α、β 和任意w∈W，如果V（α，w）＝1 并且V（β，w）＝1，那么V（α·β，w）＝1；否则（α·β，w）＝0。

［V→］对于任意合式公式α→β 和任意w∈W，如果V（α，w）＝0 或者V（β，w）＝1，那么V（α→β，w）＝1；否则V（α→β，w）＝0。

［VL］对于任意合式公式α 和任意w∈W，如果对于每个w'∈W，wRw' 并且V（α，w'）＝1，那么V（Lα，w）＝1；否则V（Lα，w）＝0。

［VM］对于任意合式公式α 和任意w∈W，如果存在w'∈W，wRw'并且V（α，w'）＝1，那么V（Mα，w）＝1；否则V（Mα，w）＝0。

一、相关定理证明

（一）完全性与一致性

假设现在有一个正规模态系统S 以及一个C模型类。当一个合式公式在C 模型类的每一个模型中都有效，我们称该合式公式是C 有效的。我们要证明系统S 在C 模型类上具有完全性，就是要证明每一个C 有效的合式公式都是系统S 的定理。换句话说，任意合式公式，如果不是系统S 的定理，那么它就不是C 有效的。

关于一致性，如果α 是S 一致的，那么～α 就不是S 的定理；如果α 不是S 一致的，那么～α 就是S 的定理。下面给出完全性定理的两个等价版本，并证明二者等价性。

【定理1】对于任意合式公式α，如果α 不是系统S 的定理，那么必定存在一个C 模型，在这个模型中存在w∈W，V（α，w）＝0。

【定理2】对于任意合式公式α，如果α 是S一致的，那么必定存在C 模型，在这个模型中存在w∈W，V（α，w）＝1。

证明1：当【定理2】成立的时候，【定理1】也成立。假设α 不是S 的定理，这意味着～α 是S 一致的，那么根据【定理2】，必定存在C 模型，在这个模型中存在w∈W，V（～α，w）＝1，根据［V～］，此时V（α，w）＝0，得证。

证明2：当【定理1】成立时，【定理2】也成立。假设α 是S 一致的，那么～α 就不是S 的定理。根据【定理1】，必定存在一个C 模型，在这个模型中存在w∈W，V（～α，w）＝0。根据［V～］，此时V（α，w）＝1，得证。

（二）极大一致集

假设存在一个系统S 的极大一致集Γ，这就意味Γ 不仅是极大的也是S 一致的。所谓极大就是说对于任意合式公式α，要么有α∈Γ，要么有～α∈Γ。我们接下来讨论一些关于极大一致集的原则。

假设Γ 是系统S 的任意一个极大一致集，下面给出几个定理：

【定理3】对于任意合式公式α，集合{α，～α}中的元素有且仅有一个在Γ 中。

证明：关于α 与～α 至少有一个在Γ 中，这是由Γ 的极大性直接给出的。下面再证，α 与～α 不能同时在Γ 中。我们需要用到一致性。假设α 和～α 都在Γ 中，那么｛α，～α｝就是Γ 的子集，根据PC 可得～（α·～α）为系统S 定理，所以α·～α 不是S 的一致的，因为｛α，～α｝是Γ 的子集，所以Γ 也不是S 的一致的，这与题设产生矛盾，所以α 和～α 只能有一个在Γ 中。

【定理4】α∨β∈Γ 当且仅当α∈Γ 或者β∈Γ。

证明：首先假设α∨β 在Γ 中，但是α 和β 都不在其中。由【定理3】可知，～α 和～β 都在Γ 中，因此｛α∨β，～α，～β｝为Γ 的子集。根据PC 可得～（（α∨β）·～α·～β）为S 的定理，所以（（α∨β）·～α·～β）不是S 一致的，即｛α∨β，～α，～β｝不是S 一致的。因为｛α∨β，～α，～β｝是Γ 的子集，所以Γ 也不是S 一致的，这与题设产生矛盾。

接下来再假设α 和β 中有一个在Γ 中，比如α，但是α∨β 不在Γ 中。所以｛α，～（α∨β）｝为Γ 的子集，根据PC 可得～（α，～（α∨β））是S 的定理，所以α，～（α∨β）不是S 一致的。因为｛α，～（α∨β）｝是Γ 的子集，所以Γ 也不是S一致的，这与题设产生矛盾。反方向的证明与此类似，这里略。

【定理5】α·β∈Γ 当且仅当α∈Γ 并且β∈Γ。

证明：假设α·β 在Γ 中，但是α 和β 不在Γ 中。由【定理3】可知～α 和～β 都在Γ 中，因此｛α·β，～α，～β｝为Γ 的子集。根据PC 可得～（（α·β）·～α·～β）为S 的定理，所以（α·β）·～α·～β）不是S 一致的，即｛α·β，～α，～β｝不是S 一致的。因为｛α·β，～α，～β｝是Γ 的子集，所以Γ 也不是S 一致的，这与题设产生矛盾。

假设α·β 和α 在Γ 中，但是β 不在Γ中，由【定理3】可知～β 在Γ 中，因此｛α·β，α，～β｝为Γ 的子集。根据PC 可得～（（α·β）·α·～β）为S 的定理，所以（α·β）·α·～β 不是S 一致的，即｛（α·β）·α·～β｝不是S 一致的，因为｛（α·β）·α·～β｝是Γ 的子集，所以Γ 也不是S 一致的，这与题设产生矛盾。假设α·β 和β在Γ 中，但是α 不在Γ 中，同样会使得Γ 不是S 一致的，因而产生矛盾。证明相同，略。反方向的证明与此类似，这里略。

【定理6】如果α 是S 的定理，那么α∈Γ，即S 的任意极大一致集包含S 的所有定理。

证明：假设合式公式α 是S 的定理，那么～α就不是S 一致的，所以～α 不属于Γ，因此α 必定属于Γ。

【定理7】假设∧是S 一致的公式集，那么存在一个S 的极大一致集Γ，并且∧⊆Γ。这意味着每一个S 一致的公式集都可以扩张成极大的S 一致集。

证明：我们首先假设所有模态逻辑的合式公式都按照一定的顺序排列，并且依次带上下标如α1，α2，α3，…同样地，我们再定义这公式集Γ0，Γ1，Γ2Γ3，…

其中：（1）Γ0就是∧，即S 一致的公式集；（2）给定Γn，如果Γn∪｛αn+1｝为S 一致的话，将其记为Γn+1；如果Γn∪｛αn+1｝ 不是S 一致的话，将Γn∪｛～αn+1｝记为Γn+1。

我们接下来证明对于任意n，如果Γn是S 一致的话，那么Γn+1也是S 一致的。因为如果Γn+1不是S一致的，意味着Γn∪｛αn+1｝和Γn∪｛～αn+1｝都不是S一致的。这意味着在Γn中存在这样一些合式公式β1，β2，…，βm，使得：

并且在Γn中也会存在这样的合式公式γ1，γ2，…，γk，使得：

最后根据式（1）、式（2）通过PC 可得：

├s～（β1·…·βm·γ1·…·γk）。

因为～（β1·…·βm·γ1·…·γk）是S 的定理，所以（β1·…·βm·γ1·…·γk）就不是S 一致的，即｛β1，…，βm，γ1，…，γk｝不是S 一致的，又因为｛β1，…，βm，γ1，…，γk｝是Γn的子集，所以Γn也不是S 一致的，这与题设相矛盾。所以Γn+1是S 一致的。

现在我们使Γ 为所有Γn的并集，那么可以得到（a）Γ 是S 一致的。因为如果Γ 不是S 一致的，那么必定存在Γ 的子集不是S 一致的。可是我们知道Γ 的所有有限子集都是某个Γn的子集，那么就意味着存在Γn不是S 一致的，与题设相矛盾，所以Γ 为S 一致的。（b）Γ 是极大的。我们考虑，对于任意合式公式αi可以构造出Γi，在Γi中要么αi∈Γi，要么～αi∈Γi。因为Γi是Γ 的子集，所以有要么αi∈Γ，要么～αi∈Γ，由此可知Γ 是极大的。（c）∧⊆Γ，从上述题设可知，因为∧就是Γ0，且Γ0⊆Γ，所以∧⊆Γ。

（三）典范模型

我们现在要讨论的是一种名为典范模型［3］22的特殊模型。和其他正规模态系统的模型一样，典范模型是一个三元组，对于任意正规模态系统S，我们对于其典范模型的定义如下所示：（1）W＝｛w:w 是S 的极大一致集｝；（2）对于任意w∈W，w'∈W，有wRw'当且仅当L-（w）⊆w'；（3）对于任意变元p 和任意w∈W，如果有p∈w，那么V（p，w）＝1，否则V（p，w）＝0。像［V～］、［VL］、［VM］之类的赋值规则还是和以前一样，因为这些规则在正规模态系统理论中是固定的元素。

在S 的典范模型中，S 的所有定理在该模型有效，即S 的所有定理在该模型的所有可能世界为真，即S 的定理是每个可能世界中的元素。同样的，每一个非S 定理在该模型的某个可能世界为假，即非S 定理就不是每个可能世界的元素。

【定理8】设是正规命题模态系统S 的典范模型，那么对于任意合式公式α 且任意w ∈W，如果α ∈w，那么V（α，w）＝1，否则V（α，w）＝0。

【定理9】令α 是任一合式公式，α 在系统S的典范模型上有效当且仅当α 是系统S 的定理。

证明：是系统S 的典范模型，假设α 是系统S 的定理。通过【定理6】，可知α 在S 的任意极大一致集中，所以对于任意w∈W，有α∈w，并且通过【定理8】我们可以知道，对于任意w∈W，有V（α，w）＝1，也就是说α 在模型中有效。

（四）死点

现在我们介绍一下什么是死点，如果一个模型包含这样的可能世界——这些可能世界不可及任意其他可能世界甚至不可及他们自身，我们把这样的可能世界称为死点。在任意模型中，如果可能世界w 是一个死点，那么对于任意合式公式α 有V（Lα，w）＝1，并且V（Mα，w）＝0。

【定理10】对于任意模型和任意w∈W，有V（L（p·～p），w）＝1 当且仅当w 是一个死点。

证明：在这里我们用反证法。假设v（L（p·～p），w）＝1，但是w 不是死点，因此就会存在w'有wRw'。通过赋值定义［VL］，有v（p·～p，w'）＝1，但这是不可能的。因为对于任意模型中的可能世界w'，都有V（p·～p，w'）＝0。这与上文产生矛盾，所以w 一定为死点。

【定理11】对于任意模型和任意w∈W，V（ML（p·～p），w）＝1 当且仅当存在一个可能世界w’∈W，有wRw'并且w'是一个死点。

证明：根据模态逻辑的赋值定义，V（ML（p·～p），w）＝1 当且仅当存在可能世界w’∈W，有wRw'并且V（L（p·～p），w'）＝1。又根据【定理10】，当且仅当w'是一个死点。

二、证明MV 系统可靠性

我们要证明MV 系统在★模型类上具有可靠性，也就是要证明MV 系统的每一个定理在★模型类上都有效。为了达到这个目的我们只需要证明两点，其一，我们需要证明MV 系统的公理在★模型类上有效；其二，我们要证明三大转换规则也在★模型类上保持有效。

（一）公理有效

我们已知K 系统中的公理在每个模型上都是有效的，那么可以知道K 系统的公理在★中的所有模型上也是有效的。证明如下：

我们已知K 公理为L（p→q）→（Lp→Lq），考虑在任意模型中的任意可能世界w，假设K 公理在w 上为假，那么就有V（L（p→q），w）＝1、V（（Lp→Lq），w）＝0，也就是说V（Lp，w）＝1 且V（Lq，w）＝0。根据赋值定义［VL］，对于任意w'∈W，并且wRw'，V（p→q，w'）＝1、V（p，w'）＝1、V（q，w'）＝0。其中V（p→q，w'）＝1 与V（p，w'）＝1 且V（q，w'）＝0相矛盾，所以K 公理在任意可能世界w 上一定为真。那么［4］K 公理在所有模型上都是有效的。

接下来证明MV 公理在★中的所有模型上也是有效的。首先，如果可能世界w 是一个死点，那么在w 上Lp 为真，因此MLp ∨Lp 也为真。再如果w可及一个死点w'，那么Lp 在w'上为真，所以MLp在w 上为真，因此MLp ∨Lp 在w 上也为真。综上所述MV 公理是★有效的。

（二）三大转换规则保持有效

分离规则MP 对任意模型保持有效性。用反证法证明。

假设存在模型，MP 对该模型不保持有效性，也就是说，存在公式α→β 和公式α，他们在上有效。但是β 在上不有效，这意味着存在w∈W，V（β，w）＝0。根据赋值定义［V→］，我们可以知道此时V（α→β，w）＝1与V（α，w）＝1 不能同时成立，这与公式α→β和公式α 在上有效相矛盾。由此可知分离规则对任意模型保持有效，当然也对★模型类保持有效性。

必然化规则N 对任意模型保持有效性。

证明：假设存在模型以及合式公式α，α 在模型上有效。这意味着对于任意w∈W，有V（α，w）＝1，此时对于任意w'∈W 且wRw'有V（α，w'）＝1。根据赋值定义［VL］，此时对于任意w∈W，有V（Lα，w）＝1。因此Lα 在上有效。由此可知必然化规则对任意模型有效，当然也对★模型类保持有效性。

代入规则US 对★模型保持有效性。此证明见相关文献，证明略。

综上所述，我们证明了MV 系统的所有公理以及MV 系统的三大转换规则都在★模型类中有效或保持有效，所以我们说MV 系统相对于★模型类具有可靠性。

三、证明MV 系统的完全性

我们要证明MV 系统具有完全性，也就是要证明每个★有效的合式公式是MV 的定理，也就是说所有不是MV 定理的公式在某个★模型中不有效。通过【定理9】我们知道，如果一个合式公式α 不是MV 定理，那么这个合式公式α 在MV 的典范模型中不有效。因此如果MV 的典范模型是一个★模型，那么必定存在一个被称作典范模型的★模型，在这个典范模型中公式α 不有效。很显然，现在我们需要证明MV 系统的完全性，也就是要证明MV 的典范模型是★模型，也就是说我们需要证明：在MV 系统的典范模型中，所有w∈W 要么是死点，要么可及某个死点。

根据【定理2】我们可以知道，对于任意合式公式α，如果α 是MV 一致的，那么必定会存在一个模型，在这个模型中有w∈W，V（α，w）＝1。由于α 是MV 一致的，那么｛α｝就是MV 一致的公式集，根据【定理7】，此时存在一个MV 系统的极大一致集，我们将其记为w'，有｛α｝⊆w'，由此我们可以构造出MV 系统的典范模型，在这个模型中存在w∈W'，V（α，w）＝1。接下来我们只需要证明该典范模型是★模型。

首先我们用p·～p 代替MV 公理中的p，因此得到了新的公式（1）ML（p·～p）∨L（p·～p），对于公式（1）来讲，在MV 系统的典范模型中，存在w∈W'，有V（ML（p·～p）∨L（p·～p），w）＝1，即ML（p·～p）∨L（p·～p）∈w。通过【定理4】，有ML（p·～p）∈w 或者L（p·～p）∈w。如果前者为真的话，有V（ML（p·～p），w）＝1，那么通过【定理11】，可知w 至少可及一个死点，如果后者为真的话，有V（L（p·～p），w）＝1，通过【定理10】，可知w 自身为一个死点。

由此可知，MV 的典范模型是★模型，即所有可能世界w∈W 要么是死点，要么可及某个死点。所以MV 系统具有完全性。

综上所述，MV 系统在★模型类上既可靠又完全。