基于开放世界预设的3—值逻辑的列表证明系统，本文主要内容关键词为：逻辑论文,列表论文,系统论文,世界论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
中图分类号：B81 文献标识码：A 文章编号：1000-9639(2004)05-
1.概述
鞠实儿（以后简称“鞠”）(1997,2001,2003)在开放世界预设的基础上构造了3—值命题演算系统（简称SLO）。在SLO中，如果v(p)=t，那么v(～p)=f；如果v(p)=f，那么v(～p)=u；如果v(p)=u，那么v(～p)=u。～表示否定。p表示命题。t、f、u分别表示真假和不确定。对于蕴涵词，鞠(2003)定义如下，令p,q为任意命题，那么
这里有序关系f
ut。对否定词和蕴涵词的详细语义证明见鞠(2003)。
2.针对SLO语义的列表证明方法
有关列表证明的一般方法详见Priest(2001)和Fitting(1998)。Priest把其作为研究非经典逻辑的证明工具，但涉及多值逻辑时他未能将此方法贯彻到底。经典的列表证明方法在处理多值逻辑时遇到的主要困难是难以简单表达任意公式取值的多样性。Fitting(1995)扩展了经典的列表方法，他用带有常元的加标蕴涵式
来等价表达任意公式，因为蕴涵词的性质可以限制任意公式的取值范围。不过Fitting的方法在某些方面仍有缺陷，例如，在把3—值命题逻辑作为例子时，他构造了8条转换规则，这些规则虽然可以随意地转换任意的加标形式，却导致了可以循环使用转换规则，从而使证明无法停止。比如(F half
X)/(T Xfalse)和(T Xfalse)/(F halfX)(half、false、true表示真值常元），由于相互首尾相接，可以不断重复上述规则。这样的构造对于机器证明有很大局限性。而且Fitting构造转换规则并没有针对某个目标，也没考虑标准形式，他只是把能够转换的规则全部列出，所以由此构造起来的证明就显得不够规范。相应地，Fitting给出的转换规则比较多，比如F falseX也是其中的一条，这也使得整个列表系统过于繁杂；另外他也没有说明给出的封闭条件对整个列表证明系统是足够的。对于SLO系统，由于SLO语义的特殊3—值性，经典的列表方法已经难以处理相关的规则，因此有必要在经典方法的基础上，针对3—值特点扩展构造出一种新的列表证明系统。本文借鉴Fitting(1995)有关多值逻辑的列表证明的实质，克服相关的缺点，在考察SLO的等价系统SLO*（见3.1）中，采用公式的加标形式A＋和A－来表示列表中的节点。
为了克服Fitting的不足，我们把初始部分后的节点形式统一成标准形式a→A＋和a→A-(a为命题常元且a≠f)，直观地表示a→A为真和a→A不为真。这样可以把任意公式A的取值限制在某个范围内，在列表变得相当简单的同时并没有损失任意公式的3种取值可能。由此我们给出以下2条转换规则：
A+
A-
↓↓
t→A+t→A-
上述规则可以把任意公式的加标形式都转换成标准形式。在用转换规则把初始部分转换成标准形式以后，再采用SLO*中相应的联结词规则。由于我们给出的所有联结词规则保持从标准形式到标准形式的转换，于是，在标准形式的范围内，我们给出封闭条件（共9条）：u→f+,u→u-,u→t-,t→f+,t→u+,t→t-,u→A十且u→A-,t→A+且t→A-,t→A+且u→A-。
3.SLO*及其列表证明
3.1 SLO*的语言
SLO*在SLO的基础上引入联结词∧、∨以及命题常元f、u、t。初始符号集L：～，∧，∨，→；(,);f,u,t;p,q,r,...。分别为联结词、技术符号、命题常元和命题变元。合式公式（简称公式）：命题常元和命题变元是公式（它们组成的集合简称原子公式集At）；如果A是公式，那么～A也是公式；如果A和B是公式，那么A∧B，A∨B，A→B也是公式；没有其他公式。为了方便，用A←→B表示(A→B)∧(B→A)的缩写。在SLO中，鞠(2003)已经证明了～和→组成的集合是联结词完备集，并且对于命题常元：t←→(p→p)，f←→t，u←→f，所以SLO*跟SLO等价。
3.2 SLO*的列表证明规则
各类联结词的规则都以标准形式出现。具体规则如下：
否定规则（共4条）：
析取规则（共4条）：
从上述规则易得，在任意的SLO*列表证明中，除了初始部分，其他节点的形式都是标准形式。转换规则把初始部分转成标准形式后的各种扩展都保持标准形式之间的转换。
定义2：在列表证明中，对任意的有限公式集∑和公式A，∑
A表示对∑中的每个
，以＋和A－为初始部分通过转换规则及各联结词规则展开的列表是封闭的；∑A表示同样产生的完全列表是开的。如果有A，那么称A为SLO*的内定理。在证明过程中，当列表中的某支封闭时，在其下方我们用记号*表示。
列表总共有3个分支，左支6中的u→A－和3中u→A＋构成封闭条件；右支6中的t→A－和3中的t→A＋构成封闭条件；中间一支的u→A－和t→A＋也构成封闭。所有的分支都是封闭的，所以整个列表是封闭的，即A→(B→A)是SLO*的内定理。
3.3证明规则的语义说明
定义3：令真值集T=[f,u,t]，满足序关系：fut。令命题解释v是从At到T的映射，对每一个命题常元a，有v(a)=a(a∈T)；对每一命题常元p，在T中取某个确定的值v(p)；对SLO*中的任意联结词：v(p∧q)=min(v(p),v(q)),v(p∨q)=max(v(p),v(q))(min和max相对分别取极小和极大），*v(～p)=～v(p),v(p→q)=v(p)→v(q)。～和→的取值同SLO。对公式的结构作归纳，对任意公式A,B和任意解释v，有v(A)∈T，且v(A∧B)=min(V(A),V(B)),v(A∨B)=max(v(A),v(B)),v(～A)=～v(A),v(A→B)=v(A)→v(B)。
命题1：对于任意的公式A，没有v使得v(～A)=t。
证明：据定义3，V(～A)=～v(A)，而v(A)∈T，再据1中“～”的定义，～v(A)≠t。
命题2：已经列出的9种封闭条件相对标准形式的SLO*是完备的。
证明：我们根据赋值把矛盾的情况找出来。分两种情况考虑。第一种A是命题常元，加标后的标准式总共有12种。其中根据赋值和加标的定义，t→f+,t→u+,t→t-,u→u-,u→f+,u→t－会导致矛盾，因此我们把它们作为封闭条件的一部分。第二种A是任意的公式，那么组合后加标的标准式只有4种。由于A的取值尚不确定，就单个而言都不导致矛盾，但如果有其中的2个同时出现在列表的同一分支中就有可能导致矛盾。上述4种两两组合后总共有6种，不难发现其中t→A＋和t→A-,u→A＋和u→A-,t→A＋和u→A－在一支中的同时出现都会导致矛盾，因此把它们也作为封闭条件的一部分。对于上述标准式的3种组合，如果出现矛盾的情形，那么一定在于其中的两种，所以只需把导致矛盾的2种选出作为封闭条件，而没有必要把3种作为整体列进去。4种以上的组合也同样。
定义4：∑为任意的合式公式集（前提）；那么称A（结论）是∑的语义后承（∑
A）当且仅当不存在解释v使得每一个∑中的成员为真而A不为真，也就是说每一个使得∑中的成员为真的解释也使得A为真；∑A表示不是∑A。
3.4 SLO*的可靠性与完全性
定义5：令v是任意的命题解释，b是某个列表中的任意一支.我们说v对b是忠实的(faithful)当且仅当对任意的公式A，如果A＋在b上，那么v(A)=t；果A－在b上，那么v(A)=f或v(A)=u，也就是说v(A)≠t。
引理1（可靠性引理）：如果v对某个列表的某个分支b是忠实的并且对b采用列表规则直至完全，那么v至少对b产生的一个分支是忠实的。
证明：分类考察列表规则。
(1)转换规则。据定义3，定义5和蕴涵词性质易证。
(2)“～”。有4种情况，这里只证其中2种。如果t→～A＋在b中，那么据命题1，没有v使得v(～A)=t，所以没有v使得v(t→～A)=t。这表明没有v可以对b忠实，也说明引理成立。如果u→～A＋在b中，那么采用“～u+”规则仅产生一个分支t→A-。因为v对b是忠实的，所以v(u→～A)＝t，根据蕴涵词的定义和否定词的性质有v(～A)=u，所以v(A)=f或v(A)=u，即v(t→A)≠t。其他2种证明类似。
(3)“→”。有4种情况：如果u→(A→B)－在b中，那么采用“→u-”规则产生惟一分支，分支中有t→A+和u→B-。因为v对b是忠实的，所以有v(u→(A→B))=f或v(u→(A→B))=u。而根据蕴涵词的定义前者不可能，所以v(u→(A→B))=u。于是可得v(A→B)=f，所以v(A)=t并且v(B)=f，于是有v(t→A)=t和v(u→B)≠t，满足忠实性条件。如果u→(A→B)＋或t→(A→B)－或t→(A→B)＋在b中，相应的证明类似u→(A→B)-。
(4)“∧”和“∨”。证明类似“～”和“→”，故略去。
命题3：如果列表的某支b是封闭的，那么找不到这样的v使得v对b是忠实的。
证明：逐一考察封闭条件，根据忠实的定义易证。
定理1（可靠性定理）：对有限合式公式集2，如果∑A，那么∑A。
证明：证其逆否。设∑A，也就是说至少有一个解释v使得∑中的每个成员为t，但v(A)≠t。现在考虑证明∑A的完全列表，它的初始部分由B1+,…,Bn+(Bi∈∑)和A－组成，v对初始部分是忠实的。根据可靠性引理1，v至少对b的一个扩展分支是忠实的，把初始部分和这一分支记作b'。如果∑A，那么整个列表是封闭的，封闭条件会出现在b'中，据命题3,v不可能相对b'是忠实的，矛盾。所以列表只能是开的，也即∑A。
定义6：令b是某个列表中的开支，b产生的解释v使得对每一个命题变元p，如果t→p＋是b中的节点，那么v(p)=t；如果t→p－是b中的节点，那么v(p)≠t；如果u→p＋是b中的节点，那么v(p)≠f；如果u→p－是b中的节点，那么v(p)=f。
引理2（完全性引理1）：令b是某个列表中的开支，v由b产生的解释。那么，对任意的A，如果t→A＋是b中的节点，那么v(A)=t；如果t→A－是b中的节点，那么v(A)≠t；如果u→A+是b中的节点，那么v(A)≠f；如果u→A－是b中的节点，那么v(A)=f。
证明：施归纳于A的结构。如果A是命题变元，那么根据定义6易得。如果A是命题常元，根据定义3和蕴涵词性质易得。如果A是复合公式，我们只考察形如～B和B→C的公式，其他的证明类似。
先设A形如～B。如果t→～B＋在b中，采用“～t＋”规则得t→u＋在b中，这已经满足了封闭条件，矛盾于b是开的条件，即说明引理成立。如果u→～B＋在b中，那么采用“～u+”规则，t→B－也在b中；据归纳假设，v(B)≠t，所以v(～B)≠f。另外两种证明类似。
再考察A形如B→C。如果t→(B→C)＋是b中节点，那么根据“→t+”,u→B-,t→C+,t→B－且u→C＋也是b中节点；根据归纳假设，有v(B)=f，或v(C)=t，或v(B)≠t且v(C)≠f；在上述三种情况下，均有v(B→C)=t，满足引理要求。如果t→(B→C)－或u→(B→C)＋或u→(B→C)－是b中节点，相应证明类似。
引理3（完全性引理2）：令b是某个列表中的开支，v由b产生的解释．那么，对任意的A，如果A＋是b中的节点，那么v(A)=t；如果A－是b中的节点，那么v(A)≠t。
证明：任意列表中除了初始部分，只有4种标准形式。如果t→A＋在b中，那么根据引理2，有v(A)=t，所以v(t→A)=t；如果t→A－在b中，同理有v(A)≠t，于是v(t→A)≠t；同理可证u→A＋和u→A－在b中，有v(u→A)=t和v(u→A)≠t。如果A＋或A－是b的初始部分，据转换规则有t→A＋或t→A－也在b中，再据引理2，有v(A)=t或v(A)≠t。
定理2（完全性定理）：对有限合式公式集∑，如果∑A，那么∑A。
证明：设∑A，那么证明过程形成的表是开表，选择其中的一个开支b，令v为由b产生的解释。据引理3，对于每一个∑中成员Bi，Bi＋在b上，于是有v(Bi)=t；而A－也在这个开支上，所以v(A)≠t。这说明存在解释v使得∑中的每一个成员为真而A不真，因此据定义4有∑A。
4.结语
由于开放世界信息的不完备性，主体在现实中进行否定判断时，整个过程体现出真值不对称的性质，在此基础上形成的3—值句子逻辑具有某些非经典的性质，SLO就是用来刻画这一性质的形式系统。列表证明是一种常用的证明方法，本文采用改良的列表方法构造了SLO的等价系统SLO*，并证明了刻画定理。关于基于开放世界预设的逻辑，我们可以进一步研究相关的谓词逻辑、模态逻辑以及动态更新逻辑等内容。
收稿日期：2004-04-12