模态逻辑是由命题逻辑或谓词逻辑加上模态词而形成的扩张^[1].在模态逻辑中,框架F被定义为二元组〈W,R〉^[1,2],其中,W是非空的可能世界集合,R是W上的一种可达关系;模型M被定义为三元组〈W,R,I〉,其中,〈W,R〉是框架,I对命题符号进行解释并赋予真假值.模态逻辑根据可达关系R分为公理系统K,D,T,B,S4与S5等等^[1].在模态逻辑中,任给一个模型〈W,R,I〉,对于任意的可能世界w与公式φ,M,w|=φ当且仅当对于任意的可能世界w'∈W,如果wRw',那么M,w'|=φ.在多模态逻辑^{[3, 4, 5, 6]}中,其框架与模型的定义与在模态逻辑中的定义相似.

既然公理系统S5可以用所有的等价框架刻画^[1],那么粗糙集理论中的近似空间(U,R)可以用作S5的可能世界语义^[7].给定任意的近似空间(U,R),(U,R)可以对应S5的框架〈W,R〉,即:U=W,并且R既是U上的等价关系又是W上的可达关系.当使用S5形式化粗糙集理论时,对于任意的公式φ,φ的解释对应论域U的某个子集X;上近似集R^*(X)与下近似集R_*(X)则分别对应◊φ与□φ的解释^[7];模态词对应某个等价类,但不能用于表达粗糙集理论中精确或模糊的特点^[7],其主要原因在于模态词只有单一的解释.如果有两种不同的解释,那么不仅能用于表达粗糙集理论中精确或模糊的特点,而且能够诱导出一种新的公理化系统.考虑给定近似空间(U,R₁)与(U,R₂),那么R₁$ cap$R₂必是等价关系,其中,$ cap$是关系的交运算.既然R₁$ cap$R₂对应模态词的可达关系,那么对于任意的公式φ:

M,w|=φ iff对于任意的w'∈W,如果w(R₁$ cap$R₂)w',那么M,w'|=φ;

                  Iff对于任意的w'∈W,如果wR₁w'且wR₂w',那么M,w'|=φ.

既然对于任意的w'∈W,如果wR₁w',那么M,w'|=φ;或对于任意的w'∈W,如果wR₂w',那么M,w'|=φ,蕴含对于任意的w'∈W,如果wR₁w'且wR₂w',那么M,w'|=φ.

则有:M,w|=₁φ或M,w|=₂φ蕴含M,w|=φ.

而M,w|=φ不能蕴含M,w|=₁φ或M,w|=₂φ,其中,R_i对应模态词□_i的可达关系且i=1,2.

如果令M,w|=φ蕴含M,w|=₁φ或M,w|=₂φ,则有M,w|=φ当且仅当M,w|=₁φ或M,w|=₂φ.于是,对于任意的公式φ,φ=₁φ∨₂φ.那么,本文得到一种新的模态词.我们将给出具有模态词φ=₁φ∨₂φ的命题模态逻辑,描述其语言、语法与语义.首先给出该逻辑的语言、公式、框架、模型与可满足关系等定义,然后给出该逻辑的公理化系统的公理模式与推理规则.S5的公理模式K^[1]不是该逻辑的公理化系统的定理,最后证明该公理化系统是可靠且完备的.在证明完备性定理过程中,需要在由所有极大协调集所构成的集合上构造出两个关系并证明这两个关系是等价关系,其典型模型的构建方法与经典典型模型的构建方法^[1]不同.该公理化系统具有与S5不一样的语法与语义.对于任意的公式φ,模态逻辑或多模态逻辑不能判断M,w|=φ与M,w|=¬φ.

本文的主要贡献:提出一种具有模态词φ=₁φ∨₂φ的模态逻辑,描述其语言、语法与语义,并证明其公理化系统是可靠与完备的.与公理系统S5相比,该逻辑的公理化系统具有以下不同:

·对于任意的公式φ,φ=₁φ∨₂φ;

·框架定义为〈W,R₁,R₂〉;

·模型定义为〈W,R₁,R₂,I〉;

·公理模式K(S5的公理模式)不是该公理化系统的定理;

·在证明完备性定理的过程中,我们需要构建出两个等价关系R₁与R₂,如果R₁=R₂,那么该公理化系统变为S5.

本文第1节介绍公理系统S5.第2节给出具有模态词φ=₁φ∨₂φ的模态逻辑,描述其语言、语法与语义;同时,给出可靠性定理与完备性定理的详细证明.第3节总结全文并给出相关讨论.

本节主要介绍公理系统S5的语言、语法与语义,并简单阐述其可靠性定理与完备性定理.

公理系统S5的语言如下所示:

定义1.1.

·语言:

命题变量符号:p₁,p₂,...;

逻辑连接符:¬,→;

模态词:;

标点符号:(,).

·公式:

φ=p|¬φ₁|φ₁→φ₂|φ₁.

其中,p是任意的命题变量符号.

定义 1.2(框架^[1]).框架F是一个有序的二元组〈W,R〉,其中,W是可能世界的集合,R是W上的二元关系.

公理系统S5的公理模式与推理规则:

·公理模式:

(A1)φ₁→(φ₂→φ₁);

(A2)(φ₁→(φ₂→φ₃))→((φ₁→φ₂)→(φ₁→φ₃));

(A3)(¬φ₁→¬φ₂)→(φ₂→φ₁);

(A4)(φ→ψ)→(φ→□ψ);

(A5)φ→φ;

(A6)φ→φ;

(A7)φ→◊φ.

每一个公理模式对应可数无穷多个实例.

·推理规则:

分离规则:$\frac{{\varphi ,\varphi \to \psi }}{\psi }$;

必然规则:$\frac{\varphi }{{\Box\varphi }}$.

定理1.1(可靠性定理).对于任意的公式集∑与公式φ,如果∑|-φ,则∑|=φ.

定理1.2(完备性定理).对于任意的公式集∑与公式φ,如果∑|=φ,则∑|-φ.

2 具有模态词φ=₁φ∨₂φ的模态逻辑

本节将给出具有模态词φ=₁φ∨₂φ的模态逻辑,描述其语言、语法与语义,其公理化系统记为^S51∨^S52;然后,我们证明^S51∨^S52的可靠性定理与完备性定理.

公理系统^S51∨^S52的语言如下:

定义2.1.

·语言:

命题变量符号:p₁,p₂,...;

逻辑连接符:¬,→;

模态词:,₁,₂;

标点符号:(,).

·公式:

φ=p|¬φ₁|φ₁→φ₂|φ₁;

φ₁=₁φ₁∨₂φ₁.

·其他联结词:

(φ₁∨φ₂)=_def(¬φ₁→φ₂);

(φ₁↔φ₂)=_def¬(φ₁→¬φ₂);

(φ₁↔φ₂)=_def((φ₁→φ₂)↔(φ₂→φ₁));

(◊φ₁)=_def(¬¬φ₁).

定义 2.2(框架).框架F定义为有序三元组〈W,R₁,R₂〉,其中,W是非空的可能世界集合,R_i⊆W²是可能世界集W上的等价关系,R_i对应_i的可达关系并且i=1,2.

定义 2.3(模型).模型M定义为有序四元组M=〈W,R₁,R₂,I〉,其中:

· 〈W,R₁,R₂〉是框架;

· I是一个解释,使得对于任意命题变量p,I(p)⊆W;并且对于任意w∈I(p),p在w中为真.

对于任意的公式φ与可能世界w,可满足关系定义如下:

定义 2.4(可满足关系).给定任意模型M=〈W,R₁,R₂,I〉与公式φ,则有:

在下文,由可满足关系的定义,我们将分别给出公式在模型中有效的定义、在框架中有效的定义、在框架类中有效的定义.

定义 2.5(有效公式):

·公式φ在模型中有效当且仅当对于任意的可能世界w∈W,M,w|=φ,记为M|=φ;

·公式φ在框架中有效当且仅当对于基于框架F的任意的模型M,M|=φ,记为F|=φ;

·令C表示为框架类,公式φ在框架类C中有效当且仅当对于任意的框架F∈C,F|=φ;

· ∑|=_Cφ当且仅当对于任意框架F∈C:如果F|=∑,则F|=φ;如果∑=Ø,那么|=_Cφ.

公理系统^S51∨^S52的公理模式与推理规则如下所示:

·公理模式:

L1 φ₁→(φ₂→φ₁);

L2(φ₁→(φ₂→φ₃))→((φ₁→φ₂)→(φ₁→φ₃));

L3(¬φ₁→¬φ₂)→(φ₂→φ₁);

L4(φ∨ψ)→(φ∨ψ);

L5 φ→φ;

L6 φ→φ;

L7 (φ∨ψ)→(φ∨ψ);

L8 ◊(φ∨ψ)→(φ∨◊ψ).

每一个公理模式对应可数无穷多个实例.

·推理规则:

分离规则(MP):$\frac{{\varphi ,\varphi \to \psi }}{\psi }$;

必然规则(N):$\frac{\varphi }{{\Box\varphi }}$.

定义 2.6.设∑是一个公式集合,∑上的一个证明是公式的序列φ₁,φ₂,…,φ_n使得对于每一个i:1≤i≤n:

·要么φ_i是一个公理;

·要么φ_i∈∑;

·要么存在j,k<i使得φ_i由φ_j,φ_k与分离规则推出;

·要么存在j<i使得φ_i由φ_j与必然规则推出.

公式φ是∑的定理,记为∑|-φ,如果存在∑上的一个证明φ₁,φ₂,…,φ_n使得φ=φ_n.

本节主要阐述公理系统^S51∨^S52的可靠性定理证明.在证明之前,先证明各个公理模式的有效性:

· L4(φ∨ψ)→(φ∨ψ)

证明:对于任意框架〈W,R₁,R₂〉的任意模型M=〈W,R₁,R₂,I〉与任意的可能世界w∈W,如果M,w|=φ∨ψ,那么M,w|=φ或M,w|=ψ.

由定义2.4可知:如果M,w|=φ,则有M,w|=(φ∨ψ);

由定义2.4可知:如果M,w|=ψ,则有M,w|=(φ∨ψ).

因此可以判定:对于任意框架〈W,R₁,R₂〉的任意模型M=〈W,R₁,R₂,I〉与任意的可能世界w∈W,如果M,w|=φ∨ ψ,那么M,w|=(φ∨ψ).□

· L5 φ→φ

证明:由定义2.4可以证明.□

· L6 φ→φ

证明:假设对于某框架〈W,R₁,R₂〉的某个模型M=〈W,R₁,R₂,I〉与某个可能世界w∈W,M,w|=φ且M,w|≠φ.

既然M,w|=φ,那么对于任意的可能世界w'∈W,如果wR₁w',那么M,w'|=φ;或对于任意的可能世界w'∈W,如果wR₂w',那么M,w'|=φ;

既然M,w|≠φ,那么存在可能世界w₁与w₂使得wR₁w₁且M,w₁|=¬φ且wR₂w₂且M,w₂|=¬φ.

因为M,w₁|=¬φ,由可满足关系的定义,存在w₃与w₄使得w₁R₁w₃且M,w₃|=¬φ且w₁R₂w₄且M,w₄|=¬φ.

因为关系R₁与R₂是等价关系且wR₁w₁且w₁R₁w₃,则有wR₁w₃且M,w₃|=¬φ,这与M,w|=φ矛盾.同理,有wR₂w₄且M,w₄|=¬φ,这与M,w|=φ矛盾.

至于M,w₂|=¬φ,与M,w₁|=¬φ的证明类似,也存在矛盾.□

· L7 (φ∨ψ)→(φ∨ψ)

证明:证明过程与(L6)的证明过程类似,我们省略其证明过程.□

· L8 ◊(φ∨ψ)→(φ∨◊ψ)

证明:证明过程与(L6)的证明类似,我们省略其具体的证明.□

对于公理系统S5的公理模式K,容易证明K不是公理系统^S51∨^S52的定理.

对于MP规则见文献[1,8,9].我们仅仅给出N规则的证明:

既然对于任意的框架〈W,R₁,R₂〉的任意模型M=〈W,R₁,R₂,I〉与任意可能世界w∈W,M,w|=φ.令w'为任意一个可能世界,则有:对于任意可能世界w"∈W,如果w'R₁w",那么M,w"|=φ;或对于任意可能世界w"∈W,如果w'R₂w",那么M,w"|=φ.于是,M,w'|=φ.

既然对于任意框架〈W,R₁,R₂〉的任意模型M=〈W,R₁,R₂,I〉与任意可能世界w'∈W,M,w'|=φ,可以断定|=φ.□

由^S51∨^S52的公理,我们可以获得以下的定理:

(1) L7' (φ₁∨...∨φ_n∨ψ)→(φ₁∨...∨φ_n∨ψ);

(2) L8' ◊(φ₁∨...∨φ_n∨ψ)→(φ₁∨...∨φ_n∨◊ψ);

(3) L4' (φ↔ψ)→(φ↔ψ).

证明:

(1)重复应用公理L7即可证明;

(2)重复应用公理L8即可证明;

(3)既然(φ↔ψ)→(φ↔ψ)∨(φ↔¬ψ),由公理L4,(φ↔ψ)∨(φ↔¬ψ)→((φ↔ψ)∨(φ↔¬ψ));既然(φ↔ψ)∨(φ↔ ¬ψ)↔φ,因此(φ↔ψ)∨(φ↔¬ψ)↔φ.于是,(φ↔ψ)→φ.

与(φ↔ψ)→φ的证明类似,我们可以证明(φ↔ψ)→ψ.则有(φ↔ψ)→(φ↔ψ).□

定理 2.1(可靠性定理).对于任意的公式集∑与公式φ,如果∑|-φ,则∑|=φ.

证明:∑|-φ,则说明存在一个证明序列φ₁,φ₂,...,φ_n使得φ_n=φ.因此,对∑|-φ的证明序列长度n进行归纳证明:

·归纳基础n=1:证明序列中只有一个公式φ.因此,这个公式要么是一个公理,要么φ∈∑,则有∑|=φ;

·当n≥1时:假设对于所有由∑用小于n步推出的公式此定理成立,那么有以下几种情形:

情形1:如果φ是一个公理,则有|=φ,于是∑|=φ;

情形2:如果φ∈∑,则有∑|=φ;

情形3:如果φ是由证明序列中一个公式应用必然规则N得到的,则φ必然是□ψ这种形式,且ψ可由∑在小于n步内推出,即为∑ψ.由归纳假设可知,∑|=ψ.既然对于任意的框架〈W,R₁,R₂〉的任意模型M=〈W,R₁,R₂,I〉与任意的可能世界w∈W,M,w|=ψ,则对于任意的框架〈W,R₁,R₂〉的任意模型M=〈W,R₁,R₂,I〉与任意的可能世界w∈W,M,w|=ψ.因此,对于任意的框架〈W,R₁,R₂〉的任意模型M=〈W, R₁,R₂,I〉与任意的可能世界w∈W,M,w|=∑蕴含M,w|=φ;

情形4:如果φ是由证明序列中的两个公式使用分离规则MP得到,则证明序列中必有ψ和ψ→φ这两种形式公式,且这两个公式均可由小于n步的序列推出,即为∑ψ与∑ψ→φ.由归纳假设可知∑|=ψ与∑|=ψ→φ,于是可得∑|=φ.□

本节主要证明公理系统^S51∨^S52的完备性定理,其典型模型构建方法与经典的典型模型构建方法不同^[1].

定义 2.7(协调性).一个公式集合∑是协调的当且仅当不存在公式φ使得∑|-φ并且∑|-¬φ^[9].

由上述协调性定义,我们有:

公式集合∑是不协调的当且仅当存在公式φ₁,...,φ_n∈∑使得:

├¬(φ₁↔...↔φ_n).

定理 2.2.给定任意一个协调的公式集∑,该公式集可以扩充为极大协调集合∑^*.

证明:假定所有的公式按照α₀,α₁,...排成一列,归纳定义∑_n:

现在我们需要证明:对于任意的n,如果∑_n是协调的,那么∑_n+1也是协调的,则由归纳定义可知,∑_n+1是协调的.

令∑*=$\bigcup$∑n,那么,

(1)∑^*是协调的.

假设∑^*不协调,存在一个公式φ使得:

∑^*├φ并且∑^*├¬φ.

于是,存在有限子集∑⁰,∑¹⊆∑^*使得∑⁰φ并且∑¹├¬φ.

既然∑⁰$ cup $∑¹是有限公式集合,那么存在n使得∑⁰$ cup $∑¹⊆∑_n且∑_n不协调.但我们已经证明∑_n是协调的,因此矛盾.所以,∑^*协调.

(2)对于任意公式φ_n,要么φ_n∈∑^*,要么¬φ_n∈∑^*.

对于任意公式φ_n,由∑_n的定义可知:要么φ_n∈∑_n要么¬φ_n∈∑_n.既然∑_n⊆∑^*,可以断言:要么φ_n∈∑^*要么¬φ_n∈∑^*.□

构造模型M=〈W,R₁,R₂,I〉使得对于任意的可能世界w∈W是一个极大协调集,而在可能世界集合W上的可达关系R₁,R₂被定义为:

定义 2.8.令Γ={∑₀,∑₁,...}是由所有极大协调集构成的集合,对于任意的∑_i,∑_j∈Γ,令:

· S^-(∑_i)={φ:φ∈∑_i};

· S(∑_i)={φ:φ∈∑_i}.

定义在Γ上的关系R₁与R₂:

· ∑_iR₁∑_j当且仅当S^-(∑_i)⊆∑_j;

· ∑_iR₂∑_j当且仅当S(∑_i)⊆∑_j.

定理 2.3.令Γ={∑₀,∑₁,...}是由所有极大协调集构成的集合,如果对于任意的∑_i,∑_j∈Γ:

· ∑_iR₁∑_j当且仅当S^-(∑_i)⊆∑_j;

· ∑_iR₂∑_j当且仅当S(∑_i)⊆∑_j.

那么,关系R₁与R₂均是Γ上的等价关系.

证明:

1.我们需要证明R₁满足以下3个条件:

(i)R₁具有自反性:对于任意∑_i∈Γ,∑_iR₁∑_i;

(ii)R₁具有对称性:对于任意∑_i,∑_j∈Γ,如果∑_iR₁∑_j,则∑_jR₁∑_i;

(iii)R₁具有传递性:对于任意∑₁,∑₂,∑₃∈Γ,如果∑₁R₁∑₂且∑₂R₁∑₃,则∑₁R₁∑₃.

·条件(i)的证明.

对于任意的iÎN,需要证明S^-(∑_i)⊆∑_i,其证明过程如下所示:

对于任意的公式φ,如果φ∈∑_i,那么φ∈S^-(∑_i).既然φ→φ(L5)与φ∈∑_i,那么φ∈∑_i,于是S^-(∑_i)⊆∑_i.

·条件(ii)的证明.

我们需要证明:如果S^-(∑_i)⊆∑_j,那么S^-(∑_j)⊆∑_i.也就是说:对于任意公式β,如果β∈∑_j,那么β∈∑_i.

假定β$ otin$∑_i,¬β∈∑_i.因为β→β(L5)与¬β∈∑_i,可以断定¬β∈∑_i.既然S^-(∑_i)⊆∑_j,那么对于任意公式α:如果α∈∑_i,那么α∈∑_i.因¬β∈∑_i与α∈∑_i,则有α↔¬β∈∑_i.

因α↔¬β∈∑_i,则根据(α↔¬β)→(α↔¬β),(α↔¬β)∈∑_i.而(α↔¬β)→(α↔¬β)由公理L8的逆反律获得.

由(α↔¬β)∈∑_i与公理L6,有(α↔¬β)∈∑_i.既然S^-(∑_i)⊆∑_j,那么(α↔¬β)∈∑_j.由(α↔¬β)∈∑_j与公理L5,则有α↔¬β∈∑_j.因此,α∈∑_j与¬β∈∑_j.既然¬β∈∑_j与β∈∑_j,那么∑_j不协调,这与该定理的前提条件矛盾.

·条件(iii)的证明.

我们需要证明:如果S^-(∑₁)⊆∑₂与S^-(∑₂)⊆∑₃,那么S^-(∑₁)⊆∑₃.也就是说:对于任意公式β,如果β∈∑₁,那么β∈∑₃.其证明过程如下所示:

由β∈∑₁与β→β(L6),则有β∈∑₁.根据∑₁R₁∑₂与关系R₁的定义,则有φ∈∑₂.由∑₂R₁∑₃与β∈∑₂,则有β∈∑₃.因此对于任意公式β,如果β∈∑₁,那么β∈∑₃.因此,S^-(∑₁)⊆∑₃.

2.现在,我们需要证明关系R₂是等价关系,下面3个条件需要被证明:

(i)对于任意∑_i∈Γ,∑_iR₂∑_i;

(ii)对于任意∑_i,∑_j∈Γ,如果∑_iR₂∑_j,则∑_jR₂∑_i;

(iii)对于任意∑₁,∑₂,∑₃∈Γ,如果∑₁R₂∑₂且∑₂R₂∑₃,则∑₁R₂∑₃.

条件(i)与条件(iii)比较容易证明,在此省略它们的证明过程.本文只给出条件(ii)的证明:

对于条件(ii),我们需要证明:对于任意公式β,如果β∈∑_j,那么β∈∑_i.其证明过程如下所示:

假定β$ otin$∑_i,于是¬β∈∑_i.既然∑_iR₂∑_j,则有:对于任意公式α,如果α∈∑_i,那么α∈∑_j.由¬β∈∑_i与α∈∑_i,则有α↔¬β∈∑_i.

根据公理L8的逆反律,则有(φ↔¬ψ)→(φ↔¬ψ),然后有(α↔¬β)→(α↔¬β).

因¬φ↔α∈∑_i与(α↔¬β)→(α↔¬β),则有(α↔¬β)∈∑_i.

由(α↔¬β)∈∑_i与公理L4',则有α↔¬β∈∑_i,于是¬β∈∑_i.既然∑_iR₂∑_j,那么¬β∈∑_j.由¬β∈∑_j与L5,我们有¬β∈∑_j.既然¬β∈∑_j且β∈∑_j,可以断定∑_j不协调,这与该定理的前提条件矛盾.□

定理 2.4.令Γ是包含公式¬ψ的极大协调公式集合,S^-(Γ)$ cup ${¬ψ}是协调的且¬ψ∈Γ,其中,S^-(Γ)={φ:φ∈Γ}.

证明:

1.我们需要证明S^-(Γ)$ cup ${¬ψ}是协调的,其证明过程如下所示:

对于S^-(Γ),有以下两种情况:

·情形1.S^-(Γ)≠Ø.

于是,Γ至少包含一个φ这种形式公式,比如令φ∈Γ,则:

首先,本文需要证明¬ψ∈S^-(Γ),其证明过程如下所示:

由¬ψ∈Γ与φ∈Γ,可以断定φ↔¬ψ∈Γ.根据公理L8的逆反律,可以得到φ↔¬ψ→(φ↔¬ψ),然后有(φ↔¬ψ)∈Γ.

根据定理L4'与(φ↔¬ψ)∈Γ,φ↔¬ψ∈Γ,然后¬ψ∈Γ.

由S^-(Γ)的定义,则有¬ψ∈Γ.

其次,利用反证法证明S^-(Γ)$ cup ${¬ψ}是协调的,其证明过程如下所示:

假定S^-(Γ)$ cup ${¬ψ}不协调,则意味着存在S^-(Γ)的有限子集{¬β₁,...,¬β_n},使得:

├¬(¬□β₁↔...↔¬β_n↔¬ψ),

其中,n≥1.

对于n,我们有以下两种情况:

情形1.1.n≥2.

于是,

├¬(¬β₁↔...↔¬β_n↔¬ψ) iff ├β₁∨...∨β_n∨ψ

iff ├(β₁∨...∨β_n∨ψ)(根据N)

iff ├β₁∨...∨β_n∨ψ(根据L7)

iff ├¬(¬β₁↔...↔¬β_n↔¬ψ)

于是,{¬β₁,...,¬β_n,¬ψ}不协调.

对于任意¬β_i∈S^-(Γ),由S^-(Γ)的定义可知,¬β_i∈Γ.既然¬β_i→¬β_i且¬β_i∈Γ,那么则有¬β_i∈Γ,其中,i=1,...,n.因此,{¬β₁,...,¬β_n}⊆Γ.于是,{¬β₁,...,¬β_n,¬ψ}⊆Γ.既然{¬β₁,...,¬β_n,¬ψ}不协调,那么Γ也不协调,这与该定理的前提条件矛盾.

情形1.2.n=1.

易知S^-(Γ)仅仅包含一个¬α这种形式的公式,也就是¬ψ,

因此,

├¬(¬ψ↔¬ψ).

于是,

├¬(¬ψ↔¬ψ) iff ├ψ∨ψ

                          iff ├(ψ∨ψ)(根据N)

                          iff ├ψ∨ψ(根据L7)

                          iff ├ψ

                          iff ├¬(¬ψ)

于是,{¬ψ}不协调.

因为¬ψ∈S^-(Γ),根据S^-(Γ)的定义可知,¬ψ∈Γ.既然¬ψ→¬ψ且¬ψ∈Γ,则有¬ψ∈Γ.因为¬ψ∈Γ,所以{¬ψ}⊆Γ.既然{¬ψ}不协调,那么Γ也不协调,这与该定理的前提条件矛盾.

·情形2.S^-(Γ)=Ø.

假定{¬ψ}不协调,则有ψ.由推演规则N,可以断定├ψ.

因为├ψ,则有ψ∈Γ.

由ψ∈Γ与¬ψ∈Γ,可知Γ不协调,这与该定理的前提条件矛盾.

2.本文需要证明¬ψ∈Γ,其证明过程是:

既然Γ是某个极大协调集合,由极大协调集的生成过程可知,应该证明:存在公式集合Γ_k+1,使得Γ_k+1=Γ_k$cup ${¬ψ}协调,其中,¬ψ∈Γ_k且Γ_k协调的.

假定Γ_k$cup ${¬ψ}不协调,这意味着存在某一有限子集{¬β₁,...,¬β_n,¬ψ}⊆Γ_k,使得:

├¬(¬β₁↔...↔¬β_n↔¬ψ↔¬ψ),

情形2.1.n≥2.

├¬(¬β₁↔...↔¬β_n↔¬ψ↔¬ψ) iff ├β₁∨...∨β_n∨ψ∨ψ

                                                             iff ├(β₁∨...∨β_n∨ψ∨ψ)(根据N)

                                                             iff ├β₁∨...∨β_n∨ψ∨ψ(根据L7)

                                                             iff ├¬(¬β₁↔...↔¬β_n↔¬ψ)

于是,{¬β₁,...,¬β_n,¬ψ}不协调.既然{¬β₁,...,¬β_n,¬ψ}⊆Γ_k,那么Γ_k也不协调,这与前提假设矛盾.

情形2.2.n=1.

除了¬ψ,Γ_k不再包含任意其他¬β形式的公式,于是:

¬(¬ψ↔¬ψ).

于是,

¬(¬ψ↔¬ψ) iff ψ∨ψ

                        iff (ψ∨ψ)(根据N)

                        iff ψ∨ψ(根据L7)

                        iff ψ

                        iff ¬(¬ψ)

于是,{¬ψ}不协调,而{¬ψ}⊆Γ_k.因此Γ_k也不协调,这与前提假设矛盾.□

^S51∨^S52的典型模型M与其他模型类似也是四元组〈W,R₁,R₂,I〉,其中,W是由所有极大协调集构成的集合,也就是:w∈W当且仅当w是一个极大协调集;如果w与w'都是W的元素,那么wR₁w'当且仅当S^-(w)⊆w';并且如果w与w'都是W的元素,那么wR₂w'当且仅当S(w)⊆w';对于任意命题变量p,I(p)⊆W且对于任意w∈I(p),p在w为真当且仅当p∈w.对于其他公式,则有以下定理成立:

定理 2.5.令M=〈W,R₁,R₂,I〉是^S51∨^S52的典型模型,则对于任意的公式φ,M,w|=φ当且仅当φ∈w.

证明:对公式的结构进行归纳证明,其证明过程如下所示:

·情形1.φ:=p:

由典型模型的构造可知,成立.

·情形2.φ:=¬α:

M,w|=¬α iff M,w|≠α

iff α$ otin$w

iff ¬α∈w

·情形3.φ:=α→β:

α→β$ otin$w iff ¬(α→β)∈w

iff α∈w且¬β∈w

iff M,w|=α且M,w|=¬β

iff M,w|≠(α→β)

·情形4.φ:=ψ:

($ \Rightarrow $)

情形4.1.M,w|=ψ.

M,w|=ψ iff对于任意的可能世界w'∈W,如果wR₁w',则M,w'|=ψ;或

对于任意的可能世界w'∈W,如果wR₂w',则M,w'|=ψ

由归纳假设可知:对于任意的可能世界w'∈W,如果wR₁w',则ψ∈w';或对于任意的可能世界w'∈W,如果wR₂w',则ψ∈w'.

假设ψ$ otin$w,则由定理2.4可知:S^-(w)$ cup ${¬ψ}是协调的,且¬ψ∈w.那么,我们可以把S^-(w)$ cup ${¬ψ}扩充为极大协调集w₁.既然S^-(w)⊆w₁与S(w)⊆w,那么wR₁w₁且wR₂w且¬ψ∈w₁且¬ψ∈w.这与对于任意的可能世界w'∈W,如果wR₁w'则ψ∈w'矛盾;或与对于任意的可能世界w'∈W,如果wR₂w'则ψ∈w'矛盾.因此,ψ∈w.

情形4.2.M,w|≠ψ.

M,w|≠ψ iff存在可能世界w₁∈W,使得wR₁w₁且M,w₁|≠ψ,并且存在可能世界w₂∈W,使得wR₂w₁且M,w₂|≠ψ.

由归纳假设可知:存在可能世界w₁∈W,使得wR₁w₁且ψ$ otin$w₁,并且存在可能世界w₂∈W,使得wR₂w₂且ψ$ otin$w₂.

假设ψ∈w,由R₁与R₂的定义可知:对于任意的可能世界w'∈W,如果wR₁w',则ψ∈w';或对于任意的可能世界w'∈W,如果wR₂w',则ψ∈w'.这与存在可能世界w₁∈W,使得wR₁w₁且ψ$ otin$w₁,并且存在可能世界w₂∈W,使得wR₂w₂且ψ$ otin$w₂矛盾.因此,ψ$ otin$w.

($ \Rightarrow $)

情形4.3.ψ∈w.

由R₁与R₂的定义可知:对于任意的可能世界w'∈W,如果wR₁w',则ψ∈w';或对于任意的可能世界w'∈W,如果wR₂w',则ψ∈w'.由归纳假设可知:对于任意的可能世界w'∈W,如果wR₁w',则M,w'|=ψ;或对于任意的可能世界w'∈W,如果wR₂w',则M,w'|=ψ.于是,M,w|=□ψ.

情形4.4.ψ$otin$w.

既然ψ$otin$w,则S^-(w)$ cup ${¬ψ}是协调的,且¬ψ∈w.于是,我们可以把S^-(w)$ cup ${¬ψ}扩充为极大协调集w₁.既然¬ψ∈w₁且¬ψ∈w,由归纳假设可知,M,w₁|≠ψ且M,w|≠ψ.既然存在可能世界w₁,w∈W,使得wR₁w₁且wR₂w且M,w₁|≠ψ且M,w₁|≠ψ,于是,M,w|≠ψ.□

定理 2.6(完备性定理).对于任意的公式集合Γ与公式φ,如果Γ|=φ,则Γφ.

证明:假设Γφ不成立,于是Γ$ cup ${¬φ}协调.由定理2.2可知,我们可以把Γ$ cup ${¬φ}扩展为极大协调集合w'.

令M=〈W,R₁,R₂,I〉是其典型模型,其中,可能世界集合W是由所有的极大协调集构成.对于任意的可能世界w_i,w_j∈W(w_i与w_j均是极大协调集),w_iR₁w_j当且仅当S^-(w_i)⊆w_j,或w_iR₂w_j当且仅当S(w_i)⊆w_j;对于任意命题变量p,I(p)⊆W且对于任意w∈I(p),p在w为真当且仅当p∈w.

于是,由定理2.5可知:对于任意公式ψ∈Γ$ cup ${¬φ},M,w'|=ψ当且仅当ψ∈w'.因此,M,w'|=Γ且M,w'|=¬φ.这与Γ|=φ矛盾,因此,Γφ.□

在完备性定理证明过程中,我们需要构造出^S51∨^S52的典型模型,并在W上构建出两个等价关系.这与S5的典型模型不同.至此,我们已经证明了^S51∨^S52的完备性定理.

本文提出了具有模态词φ=₁φ∨₂φ的模态逻辑,我们给出其语言、语法与语义,其公理化系统记为^S51∨^S52,该公理化系统是可靠且完备的.^S51∨^S52有与S5类似的语言,但具有不同的语法与语义.如果₁的可达关系等于₂的可达关系,那么^S51∨^S52变为S5.^S51∨^S52可以看做是一种由两个模态词通过析取方式共同作用而形成的一种模态逻辑.

我们下一步的工作是:在模态谓词逻辑中扩展^S51∨^¬S52,并证明其可靠性与完备性;利用本文的公理化系统形式化粗糙集理论并讨论相关性质.

致谢 在此,我们向对本文的工作给予支持和建议的同行表示感谢.