栏目导航

形式系统的可靠性和完全性问题

2005-11-30 00:07:17 作者：余俊伟来源：湖南科技大学学报浏览次数：0 网友评论 0 条

【内容提要】语法完全性仅与一个形式系统的语法构造相关，经典命题逻辑的有代入规则的系统是语法完全的，无代入规则的系统不是语法完全的。将全称概括规则作为初始规则的系统是否限制对该规则的使用可导致系统相对于通常的语义解释是否具有强可靠性。对必然化规则和模态逻辑系统来说有类似的结果。

    形式系统一致性通常有古典的、语法的和语义的三种含义。一形式系统是古典一致的当且仅当不存在公式A，A和A的否定都在该系统中可证；一形式系统是语法一致的当且仅当并非任何公式都在该系统中可证；一形式系统是语义一致的当且仅当凡有效公式都是在该系统中可证的。语义一致性也称可靠性。
    完全性也有三种含义。一形式系统具有古典完全性，是指对任一公式，或者A是可证的，或者A的否定是可证的；一形式系统具有语法完全性，是指如果将任一个不可证的公式作为公理加到该系统中，则所得的系统就不一致；一形式系统具有语义完全性，一般是指凡是在该系统中可证的公式都是有效的[1]。
    本文着重考察语法完全性和语义一致性，即可靠性。
    一般来说，一个值得研究的有意义的系统都会具有古典的和语法的一致性。常见的系统因为其语言含变元，故一般也不具有古典的完全性。但是对于语法和语义完全性及语义一致性，由于形式系统的构造可能会有不同的结果。我们先考察经典命题逻辑演算。以下给出两个形式系统PC1和PC2，它们的语言都为L1。L1的符号如下：
    可数无穷多个命题变元符号：p[,1]，p[,2]，…，p[,n]，…；
    联结词：～，→；
    另外为便于阅读再加两个辅助符号：(，)。
    公式的形成规则如常。全体公式集记为Form(L1)。
    语义完全性涉及到一个语言的解释。下面我们给出语言L1的经典语义解释。一个L1真值赋值π是一个从Form(L1)到｛1，0｝中的映射并且满足条件：
    (1)π(A) = 1当且仅当π(～A) = 0。
    (2)π(A→B) = 1当且仅当π(A) = 0或者π(B) = 1。
    定义1　π是一真值赋值，A是一公式，Γ是一公式集。
    如果π(A) = 1，则称π是A的一个单赋值模
    附图
    如果任一真值赋值都是A的单赋值模型，称A是有效式(永真式)。如果任一真值赋值都　不是A的单赋值模型，称A是矛盾式(永假式)。
    定义2　Γ语义后承A指：Γ的单赋值模型都
    附图
    系统PC1有无穷多条公理，任一公理都具有下列三种结构之一：
    (1)A→(B→A)；
    (2)(A→(B→C))→((A→B)→(A→C))；
    (3)(～A→B)→((～A→～B)→A)。
    (1)、(2)和(3)也叫做公理模式。
    PC1有一条推导规则：从A和A→B可得到B，叫做分离规则，记为MP[3]。
    附图
    系统PC2有三条公理：
    (1)p[,1]→(p[,2]→p[,1])
    (2)(p[,1]→(p[,2]→p[,3]))→((p[,1]→p[,2])→(p[,1]→p[,3]))
    (3)(～p[,1]→p[,2])→((～p[,1]→～p[,2])→p[,1])
    PC2有两条推导规则：
    R1：分离规则；
    R2：代入规则：从A可得A(B/p1)，记为Sub。
    定义4　指：存在一个公式序列A[,1]，…，A[,n]使得：A = A[,n]并且对每一A[,i](1≤i≤n)都满足下列条件：A[,i]或者为公理，或者属于Γ，或者为由在其前的公式A[,j]和A[,k]运用分离规则所得，或者为由在其前的公理运用代入规则所得。亦称A是Γ的PC2语法后承。当Γ为空集时，称A为定理，亦称A在PC2中可证。定理集记为Th(PC2)[1]。
    PC2亦有演绎定理成立。
    可靠性又分弱的与强的两种。强的是指语法后承都是语义后承。当语法后承定义中的Γ为空集时即为弱的可靠性定义，也即为文章开头所述。完全性亦有类似的划分。
    附图
    为由在其前的公式运用代入规则所得。此公式序列称为从Γ到A的一个PC2[C]推导。称A是Γ的PC2[C]语法后承。当Γ为空集时，称A为定理。定理集记为Th(PC2[C])。
    附图
    因为规则通常要具有保真性。另外代入规则不是必需的，所以为了简化元理论的讨论，现在一般都采用公理模式给出形式系统，不再使用代入规则。
    接下来我们讨论语法完全性。首先明确一下语法完全性定义中所指的导致不一致应该是语法上的不一致。先看PC1的语法完全性问题。
    显然p[,1]不是PC1可证的，将之作为公理添加到PC1中，假设所得系统不一致，则存在公式
    附图
    PC1中不可证。所以将p[,1]作为公理添加到PC1中，不会导致不一致，因此PC1不具有语法完全性。
    对于PC2，情况很不相同。任取一在PC2中不可证的公式A，现将之作为公理添加到PC2 中。据(弱)完全性知有一A不是有效式，于是存在一个代入，对A实施该代入会推导出一个矛盾式B，进而可导致任一公式都在系统中可证，即导致系统不一致。因此PC2具有语法完全性。
    可以看到同样是经典命题演算系统，P1不具有语法完全性，而P2具有。因此命题演算系统是否具有语法完全性与该系统的语法构造有关，而与语言的解释无关。
    一般地，对于一个演算系统，如果它有代入规则，则由上可知该系统具有语法完全性。对于经典命题逻辑而言，如果一系统是如PC1那样以公理模式方式构造的，由于语法完全性的定义要求添加的是公式，而不是公式模式，所以，该形式系统不具有语法完全性。当然，如果把一个不可证的公式模式，作为公理模式，则所得到的系统肯定是不一致的，但不能据此认为该系统就具有语法完全性，因为语法完全性要求添加的是公式，而不是公式模式或公理模式。
    下面讨论经典谓词演算的语义完全性问题。
    对于代入规则造成的影响如命题逻辑，不再赘述。下面就全称概括规则造成的影响作分析。先给出一个一阶语言L2。两个以公理模式构造的谓词逻辑演算系统QC1和QC2。
    QC1和QC2都是建立在同一语言L2之上。L2的符号如下：
    (1)可数无穷多个个体变元：v[,1]，v[,2]，…，v[,n]，…；
    (2)联结词：～，→；
    (3)量词：；
    (4)对每一正整数n，有可数无穷多个n元谓词符号；
    (5)对每一正整数n，有可数无穷多个n元函数符号；
    (6)有可数无穷多个常元符号。
    另外为便于阅读再加两个辅助符号：(，)。
    (1)—(3)是逻辑符号；(4)—(6)是非逻辑符号。
    项与公式的形成规则如常。
    下面是对L2的语义解释。
    定义8　一个L2结构是一个有序对Str = (S，ι)，其中S是一非空集合，称为结构的( 个体)域；L是定义在L2的非逻辑符号上的一个映射，满足：
    对L2的常元符号c，ι(c)S
    对L2的n元函数符号f，ι(f)是S上的一个n元函数
    对L2的n元谓词符号P，ι(P)是S上的一个n元关系
    ι(c)(ι(f)，ι(P))称为常元符号(函数符号，谓词符号)在结构Str中的解释，也记为c[Str](f[Str]，P[Str])。
    定义9　结构Str的一个变元赋值π为一个从个体变元集到Str的个体域中的映射，即：
    π：｛v[,1]，v[,2]，…，v[,n]，…｝→S
    定义10　一个L2解释是一个有序对η = (Str,π)，其中Str是一个L2结构，该结构的域也称为解释η的域，记为｜η｜，π是Str的一个变元赋值。也称π为解释η的变元赋值；c[Str]、f[Str]，P[Str]也记为c[η]、f[η]，P[η]
    令η = (Str，π)是一个L2解释。为定义η满足一公式，先定义项t在η下的意义，即t在η下的所指η(t)。
    t是变元v[,1]，η(v[,1]) = π(v[,1])，
    t是常元c，η(c) = c[η]，
    t是ft[,1]…t[,n]，η(f t[,1]…t[,n]) = f[η](η(t[,1])，…，η(t[,n]))。
    η为一解释，π是它的一个变元赋值。a为其域的一元素，定义η的一个(新的)变元赋值π(a/x)如下：如y≠x，则π(a/x)(y) = π(y)；如y = x，则π(a/x)(y) = a。
    η = (Str,π)，则η(a/x) = (Str,π(a/x))。
    定义11　A是一公式，递归定义η满足A(记
    附图
    A[,1]，…，A[,n]使得：A = A[,n]并且对每一A[,i](1≤i≤n)都满足下列条件：A[,i ]或者为QC1公理，或者属于Γ，或者为由在其前的公式A[,j]和A[,k]运用分离规则所得。称A是Γ的QC1语法后承。当Γ为空集时，称A为定理，亦称A在QC1中可证。
    QC1有演绎定理成立。
    系统QC2的构造如下：
    公理是QC1的(1)—(6)
    推理规则有两条：
    (1)分离规则；
    附图
    A[,1]，…，A[,n]使得：A = A[,n]并且对每一A[,i](1≤i≤n)
    都满足下列条件：A[,i]或者为QC2公理，或者属于Γ，或者为由在其前的公式A[,j]和A[,k]运用分离规则所得，或者为由在其前的公式A[,j]运用全称概括规则所得。当Γ非空时称该公式系列为有前提的推导。称A是Γ的QC2语法后承。当Γ为空集时，称A为定理，亦称A在QC2中可证。
    QC2亦仅有如定理1那样的平凡的演绎定理成立，只是要将依赖的定义中的代入规则换为全称概括规则。
    我们通常说的经典谓词演算具有可靠性也是指弱的语义可靠性，QC1和QC2都具有弱的语义可靠性。而对于强可靠性这两个系统有不同的结果：QC1具有强可靠性，而QC2不具有强可靠性。如
    附图
    当然也有强完全性。
    易见广语义后承使得全称量词失去意义。因此一般采用前一种方法，而不采用后一种修改语义后承的方法。
    下面讨论模态逻辑系统的语义完全性问题。对作用于量词的全称概括规则上文已作讨论，以下仅讨论必然化规则对语义完全性带来的问题。我们将讨论仅限于模态命题逻辑系统K，所得结果对一般正规模态逻辑系统都成立。
    K建立在模态语言LM之上。LM的语言较L1增加了一个一元联结词□，公式形成规则如常。全体公式记为Form(LM)。
    LM的语义解释如下。一个框架F是一二元组，＜W，R＞，W是一非空集，R是W上的一个二元关系。一个模型M是一二元组＜F，V＞，其中F是一框架，V是一从Form(LM)×W到｛1，0 ｝中的一个映射并满足：
    (1)V(A，w) = 1当且仅当V(～A，w) = 0；
    (2)V(A∧B，w) = 1当且仅当V(A，w) = V(B，w) = 1；
    (3)V(A∨B，w) = 1当且仅当V(A，w) = 1或V(B，w) = 1；
    (4)V(A→B，w) = 1当且仅当V(A，w) = 0或V(B，w) = 1；
    (5)如果V(□A，w) = 1当且仅当对任一
    附图
    系统K的公理：
    (1)—(3)分别为PC1的公理模式(1)—(3)，只是其中的公式为LM公式
    (4)□(A→B)→(□A→□B)
    K的推理规则有两条：
    R1：分离规则：MP
    R2：必然化规则：由A可得□A。也称为N规则，记为RN[10]。
    附图
    附图
    逻辑是刻画我们常用的推理中的一些概念的，例如，所有，必然等。因此一般总是先有语义概念来描述我们头脑中关于这些概念的直观想法，然后再去构造与这些语义概念相匹配的形式系统。所以一般不会采用修改语义的方法。
    弱可靠性和弱完全性是仅针对系统来说的，它们是仅从公理出发，根据推导规则所得的公式集(定理集)与一语义解释下的有效性是否匹配的问题。一般常见的系统都具有弱的可靠性和弱的完全性。而对于强可靠性与强完全性，它不仅仅是就某个系统而言的，还牵涉到语法后承。如果系统的初始规则仅有分离规则，由于分离规则具有保真性，那么一般可将弱的可靠性较自然地推广到强的可靠性；但是，如果除了分离规则外还有其他的初始推导规则，那么在同一个系统上由于对这些规则是否可运用于公理以外的公式而会得到不同的语法后承。相对语法后承来说，语义关系一般有更为固定的含义，而且由于上面所述的逻辑研究步骤，一般是先有直观语义，再有形式语义，最后有语法，因此一般来说无论怎样定义语法后承，总是朝着让语法后承跟这种先有的语义后承关系相匹配的目标出发的。
    收稿日期：2004-09-05
【参考文献】
    [1]王宪钧.数理逻辑引论[M].北京：北京大学出版社，1982.
    [2]张尚水.数理逻辑导引[M].北京：中国社会科学出版社，1990.
    [3]宋文淦.符号逻辑基础[M].北京：北京师范大学出版社，1993.
    [4]H.B.Enderton.A Mathematical Introduction to Logic[M].Academic Press,1972 .
    [5]H.D.Ebbinghaus,J.Flum,W.Thomas.Mathematical Lgoic(2nd editon)[M].Springer-Verlag New York,Inc,1994.
    [6]叶峰.一阶逻辑与一阶理论[M].北京：中国社会科学出版社，1994.
    [7]陈慕泽.数理逻辑教程[M].上海：上海人民大学出版社，2001.
    [8]陈慕泽，余俊伟.数理逻辑基础[M].北京：中国人民大学出版社，2003.
    [9]陈慕泽.全称概括规则和受限制的演绎定理——国内数理逻辑教材中的一个问题[J] .浙江社会科学，2001，(2)：99-101.
    [10]周北海.模态逻辑导论[M].北京：北京大学出版社，1997.
    [11]C.Alexander and Z.Michael.Modal Logic[M].Oxford Univwrsity Press,Inc.,New York.1997.