（逻辑学专业论文）表列演算探究.pdf

m a s t e r sd i s s e r t a t i o no f2 0 1 1s c h o o lc o d e ：1 0 2 6 9 i 小i i l m ：5 1 0 8 2 9 0 3 0 4 4 e a s tc h i n an o r m a lu n i v e r s i a n i n q u i r y i n t ot a b l e a uc a l c u l u s d e p a r t m e n t ：坠星巳璺丛堡曼坠! q ! 呈塾i ! q 墨q 乜塾y s p e c i a l t y ：坠g 迪 r e s e a r c hd i r e c t i o n ：m o d e r n l o g i ca n dl o g i cp h i l o s o p h y s u p e r v i s i n gt e a c h e r ：鱼臣墨q i 垒! 呈q ! 垒苎璺q 曼i 垒g 坠q 塾宝望g t h ea u t h o ro f t h e s i s ：圣塾垒塾g 堡垒q ! 宝i c o m p l e t e di na p r i l ，2 0 1 1 吣54 洲050叭9iiiii哪y 华东师范大学学位论文原刨性声明 郑重声明：本人呈交的学位论文思想政治课学生课程资源的开发和利用， 是在华东师范大学攻读硕土博士( 请勾选) 学位期间，在导师的指导下进行的 研究工作及取得的研究成果。除文中已经注明引用的内容外，本论文不包含其他 个人已经发表或撰写过的研究成果。对本文的研究做出重要贡献的个人和集体， 均已在文中作了明确说明并表示谢意。 作者签名： 日期：2 0 d 年6 月f e l 华东师范大学学位论文著作权使用声明 思想政治课学生课程资源的开发和利用系本人在华东师范大学攻读学位 期间在导师指导下完成的硕拶博士( 请勾选) 学位论文，本文的研究成果归华 东师范大学所有。本人同意华东师范大学根据相关规定保留和使用此学位论文， 并向主管部门和相关机构如国家图书馆、中信所和“知网 送交学位论文的印刷 版和电子版；允许学位论文进入华东师范大学图书馆及数据库被查阅、借阅；同 意学校将学位论文加入全国博士、硕士学位论文共建单位数据库进行检索，将学 位论文的标题和摘要汇编出版，采用影印、缩印或者其它方式合理复制学位论文。 本学位论文属于( 请勾选) ( ) 1 经华东师范大学相关部f l m 查核定的“内部 或“涉密 学位论文， 于年月日解密，解密后适用上述授权。 ( 2 不保密，适用上述授权。 翮签名张啦 本人签名醚竺 2 0 1 1 年月1 日 木“涉密”学位论文应是已经华东师范大学学位评定委员会办公室或保密委 员会审定过的学位论文( 需附获批的华东师范大学研究生申请学位论文“涉 密 审批表方为有效) ，未经上述部门审定的学位论文均为公开学位论文。 此声明栏不填写的，默认为公开学位论文，均适用上述授权) 。 韭堡垒硕士学位论文答辩委员会成员名单 姓名职称单位备注 贺善侃教授东华大学主席 冯棉教授华东师范大学 晋荣东教授华东师范大学 论文摘要 表列演算是一种逻辑样式，它非常符合人的直观，并且能够很好地将逻辑 系统的证明论和语义学结合在一起，正引起人们越来越多的关注。 首先，本文对表列演算的历史发展做出简要梳理。表列演算的内定理证明 方法叫做表列方法，前者从后者发展而来，表列方法思想则来源于根岑，经过 贝特、欣迪卡等人的发展，最后在斯穆里安那里达到成熟，并逐步应用到许多 逻辑分支。 其次，本文对经典逻辑和非经典逻辑的几个表列系统做出详细的阐述，并 对它们的元逻辑性质进行一定探讨。一阶逻辑表列演算完全性的证明显示，表 列系统与公理系统完全性的证明有着重要区别。另外，某表列系统是否具有汇 合性对于其完全性证明也有重要影响。 最后，本文对表列演算与矢列演算和自然演绎等做出比较，以揭示它们的 各自优劣。鉴于表列演算具有良好的通用性等其他逻辑样式所没有的优点，新 的表列系统必将不断产生。此外，人们对非经典逻辑定理自动证明的兴趣正促 使表列方法成为一种重要工具，相信对某个逻辑分支的表列演算研究将会成为 与该逻辑分支本身的研究同样重要的一环。 关键词：表列演算；表列规则；节点；封闭 a b s t r c a t t a b l e uc a l c u l u si sal o g i cs t y l e i ti sv e r yc o n s i s t e n tw i t ht h ei n t u i t i o n , a n dj o i n s t h ep r o o ft h e o r ya n ds e m a n t i c so fal o g i cs y s t e mt o g e t h e rv e r yw e l l n o wi ti s c a u s i n gp e o p l em o l ea n di i l o r ea t t e n t i o n t h ed i s s e r t a t i o nc o b r n sa n ds t a t e sb r i c n yt h eh i s t o r yo f t a b l e a uc a l c u l u sf i r s t 虹 t h em o t h e do f t h e r o m - p r o v i n gi nt a b l e a uc a l c u l u sc a l l st a b l e a um e t h o d t h ei d e ao f t h et a b l e a um e t h o dd e r i v e s 舫mg e n t z e n , g r o w i n gt h r o u g hb e t h , h i n t i k k aa n d o t h e r s ，a n db e i n gm a t u r e db ys m u l l y a na tl a s t n o wt h i sm e t h o di su s e di nm a n y b 盛s t h e nt h ed i s s e r t a t i o ng i v e ss o m es y s t e m sc h s s i e a la n dm n - c h s s i c a ll o g i c ，a t t h es a m et i m ed i s c u s st h em e t a l o g i cp r o p e r t yo fe v e r ys y s t e m , t h ep r o o fo ft h e t a b l e a us y s t e mo ff i r s to r d e r1 0 9 i cs h o w st h a tt h e r ea r ei m p o r t a md i f f e r e n c e s b e t w e e nt h ep r o o fo ft a b l e a us y s t e m sa n da x i o m a t i cs y s t e m s ，f o rt a b l e a us y s t e m s ， w h e t h e rt h e yh a v ec o n f l u e m ep r o p e r t yc a r la l s oi n f l u e m et h ec o m p l e t e n e s s p r o o f a tl a s tw ec o m p a r et h et a b l e a uc a l c u l u sw i t hs e q u e n tc a l c u l u s ，n a t u r a l d e d u c t i o na n do t h e r s ，r e v e a l st h ea d v a n t a g e sa n dd i s a d v a n t a g e so fe a c hs t y l e t h e i n v e n t i o no ft a b l e a us y s t e m sw i l lc o n t i n u e ，b e c a u s et h e ya 】呛e a s i e rt ot h i n kt h a n o t h e rf o r m u l a t i o m t h ei n c r e a s i n gi n t e r e s ti nn o n - c h s s i c a lt h e o r e m - p r o v i n gh a s b r o u g h tt a b l e a u st oap o s i t i o no fp r o m i n e n e e ，b e c a u s et h e ye x i s tf o rm a n yb g i c s t h ed e v e l o p m e n to ft a b l e a us y s t e m sw i l la s 呻o r t a ma st h er e s e a r c ho f b g i ci t s e l f k e yw o r d s ：t a b l e a ue a l c u h s ；t a b l e a ur u l e s ；n o d e ；c l o s e 渭 目录 序论表列演算的历史发展1 第1 章经典命题逻辑的表列演算4 1 1 表列演算系统s o 4 1 2s o 的可靠性和完全性9 1 3 优先策略1 0 第2 章经典一阶逻辑的表列演算“1 3 2 1 语句表列1 3 2 2 语句表列的可靠性与完全性1 6 2 3 自由变元表列2 1 2 4 子句表列2 5 第3 章模态命题逻辑的表列演算一2 8 3 1 隐式表列演算2 8 3 2 显式表列演算3 0 第4 章直觉主义逻辑的表列演算一3 5 第5 章几种演算系统的比较一3 7 参考文献4 1 j 舌记”4 3 序论表列演算的历史发展 从语法上讲，一个逻辑系统主要有两方面的内容：它的定理集和得到其定理 集的方式，后者即此系统的定理证明方式，又可称作此系统的逻辑样式( 1 0 9 i c s t y l e ) 。1 给出一个逻辑系统，可采取的逻辑样式不是唯一的，具有相同定理集但 逻辑样式不同的逻辑系统，其特性往往具有很大的区别。表列演算便是一种逻辑 样式，表列演算系统的内定理的证明方法称作表列方法( t a b l e a um e t h o d s ) 。本部 分将对表列演算的历史发展做出梳理，以便为后续内容做好准备。 表列方法实质上是一种反证方法，其基本思想来源于根岑( qg e n t z e n ) 于 1 9 3 4 年在逻辑演绎研究( i n v e s t i g a t i o mi n t ol o g i c a ld e d u c t i o n s ) 一文中建立 的矢列演算( s e q u e n tc a l c u l u s ) 。2 比矢列演算建立更早的公理演算突出逻辑系统 的整体性，但矢列演算将结构规则、联结词规则、量词规则区分开来，为单独研 究单个联结词和量词提供了便利。实际上，由于除切割规则外其余规则都具有子 公式性，所以矢列演算可以为表列方法提供一定的思想启示：“消去定理 ( h a u p t s a t z ) 与根岑的另一个想法一即像一棵树一样构造一个证明结合起 来，影响了一种非常有效的证明方法，它称之为表方法。3 其中的表方法即所 谓的表列方法。 根岑建立矢列演算的动机是证明论方面的，其工作在证明论领域也占据重要 位置。贝特( e w b e t h ) 则出于语义学的考虑，于1 9 5 5 年在其论文语义衍推 1 这里姑且将一个逻辑系统看作其定理集与逻辑样式的结合。至于采取何种视角看待一个逻辑系统更为合 理，请参见：g a b b a y , d m w h a t 括al o g i c a ls 归t e mi m 】o x f o r du n i v e r s i t yp r e s s 1 9 9 4 2 g e n t z e n , g i n v e s t i g a t i o n si n t ol o g i c a ld e d u c t i o n s 【a 】s z a b o ，m e t h ec o l l e c t e dp a p e r so f g e r h a r d g e n t z e n 【c 】n o r t h - h o l l a n d , a m s t e r d a m , 1 9 6 9 6 8 1 3 1 3 【波】维马奇舍夫斯基现代逻辑词典【z 】张兆梅，等译北京：中国人民大学出版社，1 9 9 2 3 2 3 i 及形式可推导性( s e n m n t i ce r a a i l m e n ta n df o r m a ld e r i v a b i l i t y ) 中提出“语义表 列( s e m a r t i ct a b l e a u ) 概念：“若能够找到这样一个反例，那么我们便有了对 问题的否定回答。若不能找到反例，那么对问题的回答便是肯定的。在后一种情 形下，我们必须保证反例永不出现。要做到这一点，我们就不能没有计划地去寻 找反例，而必须以一种系统的方式去构造反例。如今就有这么一种方法，它要求 我们去构造语义表列。 4 在逻辑演绎研究一文中，根岑还研究了直觉主义逻辑的矢列演算。1 9 5 6 年，贝特则在论文直觉主义逻辑的语义构造( s e r m r 吐i cc o m t r u c t i o no f i n t u i t i o n i s t i cl o g i c ) 中给出直觉主义逻辑的一种语义解释，又叫贝特模型( b e t h m o d e l ) ，5 同时还以矢列演算的形式给出直觉主义逻辑的一个表列系统。6 在根岑的直觉主义逻辑的矢列演算中，为了反映直觉主义逻辑所强调的可构 造性，根岑规定，矢列中箭头的右边最多出现一个公式。与根岑的系统不同，贝 特的系统则允许箭头的右侧出现多个公式。贝特注意到，他的系统可被看作矢列 演算，也可被看作表列系统。值得一提的是，贝特的直觉主义表列演算引入两种 不同的树枝分叉方式：析取分叉和合取分叉。当一个树枝出现析取分叉时，如果 新树枝有一个封闭，则原始树枝封闭；当一个树枝出现合取分叉时，新树枝必须 两个都封闭，原始树枝才封闭。7 因此，经典命题逻辑的表列系统中的树枝的分 叉方式均是合取分叉。 几乎是与贝特同时，欣迪卡( j h i n t i k k a ) 也是出于语义学的考虑，研究如 何利用构造反模型的方式来证明公式的有效性的问题。欣迪卡引入“模型集 ( m o d e ls e t s ) ”这一重要概念。8 借助于模型集，运用欣迪卡引理，可以简化表 列方法完全性的证明。 斯穆里安( rm s m u u y a n ) 的一阶逻辑( f i r s t - o r d e rl o g i c ) 一书使得表 4 【转自】d a g a s t i n o ，m & d m g a b b 巧e t a lh a n d b o o k o f t a b l e a u m e t h o d s 【m 】s p r i n g e r , 1 9 9 9 1 3 - 1 4 5 请参见：【美】罗格勃尔哲学逻辑【c 】张清字，等译北京：中国人民大学出版社，2 0 0 8 2 6 5 2 6 9 6 请参见：d 。a g a s t i n o 。m & d m g a b b a ye t a lh a n d b o o k o f t a b l e a u m e t h o d s m i s p i r i n g e r , 1 9 9 9 2 5 8 - 2 6 0 7d a g a s t i n o ，m & d m g a b b a y e t a lh a n d b o o k o f t a b l e a u m e t h o d s m i s p r i n g e r , 1 9 9 9 1 6 。模型集如今常被称作下饱和集( d o w n w a r ds a t u r 砒e ds e t s ) 或欣迪卡集( h i n t i k k a s e t ) 。请参见：d a g o s t i n o ， m & d m g a b b a ye ta 1 h a n d b o o k o f t a b l e a um e t h o d s m i s p r i n g e r , 1 9 9 9 1 8 2 模态逻辑的关系语义学的建立引发了人们对模态逻辑本身和模态逻辑的表 列系统的兴趣。克里普克曾给出自己的模态逻辑贝特式表列系统，它对公理系统 完全性的证明是这样的：先证明公理系统与贝特式表列系统等价，再通过系统的 表列式构造去证明表列系统的完全性。上述证明是非常复杂的，后来为亨金( l h e n k i n ) 式证明所取代。 1 9 6 9 年，费廷在其专著直觉主义逻辑、模型论及力迫法) ) ( i n t u i t h g n i s t i cl o g i c m o d e lt h e o r ya n d f o r c i n g ) ) 中给出s 4 的一个表列系统。1 9 7 2 年，费廷又在其著 作模态逻辑证明的表列方法( t a b l e a u m e t h o d so f p r o o f f o r m o d a l l o g i c s ) ) 中给 出另外几种模态逻辑的表列系统。1 9 8 3 年，费廷还在其著作模态逻辑和直觉 主义逻辑的表列方法( p r o o f m e t h o d s f o rm o d a la n d i n t u i t i o n i s t i cl o g i c s ) 对模态 逻辑的表列方法作出全面的发展。1 0 9 在斯穆里安之前，里斯( z b i g n i e wl i s ) 于1 9 6 0 年在逻辑研究( s t u d i al o g i c a ) 杂志上用波兰语发表 论文 、 t x 或 f x ) 的一个表列，则分别称t 是x 、t x 或f x 的一个表列。为方便起见，下文将只 考虑带记号公式的集合( 或带记号公式) 的表列。 定义1 4 ( 封闭)某表列的树枝b 是封闭的，若存在公式x ，t x 和 f x 同时出现在b 上；否则，b 便是开放的。 节点n 是封闭的，若通过n 的所有树枝均是封闭的；否则，n 就是开 放的。 表列t 是封闭的，若t 的根节点慰十闭的；否则，t 是开放的。 定义1 5 ( s 0 表列证明)若表列t 是带记号公式f x 的一个封闭的s o 表列，则称t 是x 的一个s o 表列证明。 定义1 6 ( s o 的内定理)若存在公式x 的一个s o 表列证明，则称x b o a 表示由树枝b 增加末节点n 得到的树。 7 是系统s o 的一条内定理，记作b o x 。 例如，下面表列便给出公式( m 八( q 3 r ) b r ) 的一个表列证明： f ( p 3 q ) a ( q 3 r ) 3 ( p 3r ) t ( p 3 q ) ( q r ) f p3 r t p q t q3 r t p 至! 即i f 赫 因此，b ( q ) 八( q 3 r ) ) 3 r ) 。 根据定义1 3 ，任何公式集s 均有无限多个表列。例如，设f s ，则下列含 有r 1 个f 的树f 。f o 。f 均是s 的表列。这类表列对于定理证明的意义不大。为 了排除这些用途不大的表列构造，便需要引入一个概念。 定义1 7 ( 完成的表列)称一个表列的某个树枝b 是完成的 ( c o m p l e t e d ) ，若对任一出现在b 中的0 t 型公式，0 t l 和眈均出现在b 中， 且对任一出现在b 中的1 3 型公式，p l 和陀至少有一个出现在b 中。 称表列t 是完成的，若t 的每一个树枝均是完成的。1 8 经典命题逻辑是能行可判定的，表列构造可以为人们提供一种判定方法。1 9 设s 是一个由s o 的公式组成的可数集，其元素排列为x l ，x 2 ，。则可按下述 方式构造一个s 的完成的表列t 。 完成的表列不同于封闭的表列，完成的未必是封闭的，封闭的也无需是完成的。 1 9 s m u l l y 盈- t , r m f i r s t - o r d e r l o g i c 【m 】d o v e rp u b l i c a t i o n s ，i n c 1 9 9 5 3 3 8 步骤l ：仅含x l 的单节点树t o 是s 的一个表列；2 0 步骤仆l ( 逢1 ) ：记步骤i 得到的表列为t i ，首先对t i 上所有可施用表列 规则的公式全部施用表列规则，然后在所得树的所有开放树枝末尾均增加节 点x i + l ，得到s 的又一表列t i + l 。 。蔓 当s 为无限集时，上述程序是一个半判定程序( s e m i - d e c i s i o n p r o c e d u r e ) 。2 1 但是，当s 为有限集时，上述程序是一个判定程序，它在有限步内是可结束的， 结束后要么得到一个s 的封闭表列，要么得到一个s 的开放且完成的表列。这 里的终止性有赖于s o 表列规则的一个重要性质：子公式性，即s o 表列规则的结 论均是其前提的子公式。 1 2 s o 的可靠性和完全性 这里不再详述s o 的真值语义，而直接证明其可靠性和完全性。t x 是可满足 的，当且仅当，x 是可满足的。f x 是可满足的，当且仅当，一x 是可满足的。 表列t 的树枝b 是可满足的，当且仅当，由b 上的所有公式组成的公式集是可 满足的。表列t 是可满足的，当且仅当，存在t 的某个树枝b ，b 是可满足的。 定理1 8 ( s o 的可靠性定理)系统s o 的内定理均是重言式，即 b x jb x 。2 2 证明的关键在于表列规则保持可满足性。要证明i _ - s o xb x ，只需证明： 若存在f x 的一个封闭表列，则f x 是不可满足的，从而只需证明：若f x 是可 满足的，则不存在f x 的一个封闭表列；若能证明：若表列t 是可满足的，则由 t 运用某条表列规则而得到的任一表列t 也是可满足的，2 3 即各条表列规则均保 为了叙述方便，本文直接将公式作为树的节点，而非作为节点的标签。 2 1 s 不可满足时，程序会在有限步内终止，s 可满足时，程序永不终止。 2 2 s i m u l l y m , r m f i r s t - o r d e rl o g i c m i d o v e rp u b u c 缸i 0 璐i n c 1 9 9 5 2 5 2 3 这时称t 为t 的一个直接扩张。请参见：s m u l l y m , 凡m f i r s t - o r d e r l o g i c 【m 】d o v e r p u b l i c a t i o n s ，i n c 1 9 9 5 2 4 9 持可满足性，就可以很容易地证明可靠性。 现以规则黑为例，证明其保持可满足性。设分子t ( x v 是可满足的， t x l 、。 即存在赋值v ，t ( x v y ) 在v 下为真，即x v y 在v 下为真，倘若分母t x i t y 不 是可满足的，则t x 和，i y 在v 下均为假，即x 和y 在v 下均为假，则x v y 在 v 下亦为假，矛盾。所以，分母t x i t y 亦可满足。 由于s o 的完全性证明与下一章阐述的一阶语句表列的完全性证明的思路类 似，所以我将在下一章具体探讨相关证明过程。 1 3 优先策略 前文描述的表列构造不排除存在这样的表列：其树枝9 上含有节点p 和某个 节点既( i = l 或2 ) ，当针对p 运用规则( p ) 后，将得到一个具有下述形式的表 列( 这里不妨令i = 1 ) ： d 1 3 l 1 3 llp 2 在上述表列中，d l 在某个树枝中有两次出现。当用某个公式去检验其所在树 枝是否封闭时，只需用到这个公式的一次出现，更多次的出现是多余的。为了避 免这种冗余现象，便需要对表列做出限制。 定义1 9 ( 正则表列)称表列t 是正则的( r e g u l a r ) ，若不存在公式x ， x 在t 的某个树枝中有一次以上的出现。2 4 m d a g ) s t i n o ，m & d m g a b b a y , e t a l h a n d b o o k o f t a b l e a um e t h o d s 【m 】s p r m 寥r , 1 9 9 9 7 0 1 0 正则性的限制可以避免某些冗余的出现，但有时也会带来一定的不便，这种 不便与( a ) 规则的应用有关。例如，公式x _ _ 1 ( q 八q ) 八q 八- - - , q ) ) ，容易证明， x 是s o 的一个内定理但不存在x 的封闭的正则表列。为解决这一问题，可采取 下面两种方法之一：2 5 1 用规则( 旺1 ) 和规则( 睨) 代替规则( a ) 。 2 按下述方式修改( 仅) 规则和( p ) 规则的定义 修改后的( 0 【) 规则：若树枝q 含有公式q ，则可以给q 增加某个未出 现在q 中的公式o t i ( 1 或2 ) 修改后的( p ) 规则：若树枝午含有公式p ，且p l 和陇均为出现在9 中， 则可对p 应用以前的( p ) 规则 关于正则表列，一个重要的事实是： 命题1 1 0 设s 是一个不可满足的公式集，则s 的任一极小封闭表列均 是正则的。2 6 表列构造的又一重要问题是：各条规则的采用顺序如何? 或者说，是不是应 该优先采用某条或某些规则? 这一问题涉及表列规则应用的优先策略和限制策 略。2 7 这里阐述两种优先策略。 斯穆里安给出一种非常简单的优先策略：首先处理i f , 型公式，然后处理d 型公式，因为( a ) 规则的应用不会导致分叉。 第二种优先策略也是出于尽可能避免产生新树枝的考虑，称作冲突( c l a s h ) 优先策略，这个策略要求优先处理a 型公式和满足下列条件的p 型公式：当p l 和p 2 已经出现在p 所在树枝中时，才对p 应用( p ) 规则，其中p l 和p 2 分别为 ”d a s o s t i n o ，m & d m g a b b a y ，e ta 1 h a n d b o o k o f t a b l e a um e t h o d s 呻】s p r i n 静, 1 9 9 9 7 0 7 1 拍d a g o s t i n o ，m & d m o a b b a y ，e t a l h a n d b o o k o f t a b l e a u m e t h o d s 【m 1 s p r i n g e r , 1 9 9 9 7 1 2 7 d a g o s t i n o ，m & d m g a b b a y , e ta lh a n d b o o k o f t a b l e a um e t h o d s 【m 】s p r i n g e r , 1 9 9 9 7 1 - 7 5 p l 和f i z 的补。2 8 显然，这种对( p ) 规则的限制等价于下面两条规则的组合：( 1 ) 由d 和1 3 1 得出1 3 2 ，( 2 ) 由p 和& 得出p l 。 关于限制策略，本文将针对子句表列进行讨论，相关内容请参见第2 章。 拍带记号公式t x ( f x ) 的补为f x ( t x ) ，无记号公式x 的补可如下定义：若x 是一个否定式一y ，则 x 的补为y ，若x 不是一个否定式，则x 的补为一x 。 1 2 第2 章经典一阶逻辑的表列演算 相对于第1 章的0 【型公式和d 型公式，经典一阶逻辑的全称量词和存在量词 导致两种新的公式类型：丫型公式和6 型公式，相应的新规则为( 丫) 规则和( 6 ) 规则。新规则的表述方式是一阶表列系统的一个重点，不同的一阶表列系统对新 规则的表述方式是不同的，从而它们的性质也有所区别。本章将探讨4 种一阶表 列系统：一阶语句( s e n t e n c e ) 表列系统、一般自由变元表列系统、自由变元表 列系统和子句( c l a u s e ) 表列系统。2 9 2 1 语句表列 一阶逻辑具有如下元定理：某公式是可证的，当且仅当，它的全称闭包 ( u n i v e r s a lc l o s u r e ) 是可证的。3 0 由此，要想证明某个一阶公式，只需证明其全 称闭包即可。所以，本文在给出经典一阶逻辑的形式系统时可以只考虑闭公式( 又 称语句) ，来建立语句表列系统。 语句表列系统的标准形式是由斯穆里安给出的，3 1 本节的s l 与斯穆里安的系 统本质上是相同的。s i 为加快表列分解的速度，将对型公式和p 型公式做出一 个简单的推广，并针对q 、p 、丫、6 型公式分别给出其a 子公式的序列、p 子公 式的序列、丫子公式、6 子公式，具体见下表： 2 9 关于这里使用的一阶语言，请参见：d a g o s t i n o ，m & d m g a b b a y ，e t a l h a n d b o o k o f t a b l e a u m e t h o d s 【m 】s p r i n g e r , 1 9 9 9 1 2 6 - 1 3 0 3 0 h a m i l t o n , a gl o g i c f o rm a t h e m a t i c i a n s 【m 】c a m b r i d g eu n i v e r s i t yp r e s s ，1 9 7 8 8 0 8 1 3 1 s m u l l y m l , r m f i r s t - o r d e r l o g i c 叫】d o v e rp u b l i c a t i o n s ，i n c 1 9 9 5 5 2 5 4 a 型公式 p 型公式 伍a 子公式的序列 pp 子公式的序列 1 1 ff f l 八八f n f 1 ，f nf l v v f nf l ，f n 一0 ：1 v v f n )一f l ，- 1 f n一l 八a f n )- - - , f l ，- 1 f n 一正3 g )f ，一g f g _ 1 f ，g 丫型公式 6 型公式 丫 丫子公式 66 子公式 v x f f t ) j x f v x c ) - 1 j ) ( f f t )一v x ff c 其中，t 为任一基项( g r o u n dt e r m ) ，即不含变元符号的项。c 为任一常量。 s l 的表列规则可表示如下： ( a )旦( 嘶为a 的某个子公式，i = l ，2 ，n ) ( x i 赤 ( 丫) 素( 对任一基项t ) ( 6 ) _ i ( 对任一新常量c ) 6 ( c ) 下面定义“s l 表列”这一概念：3 2 3 2 定义2 1 - 定义2 3 参考了d a g o s t i n o , m & d m g a b b a y ，e ta 1 h a n d b o o k o f t a b l e a um e t h o d s 【m 】s o r i n g e r , 1 9 9 9 1 4 4 - 1 5 1 1 4 ，s 的一个语 1 任一以s 中的某个公式为标签的单节点树，均是s 的一个语句表列； 2 若t 是s 的一个表列，b 是t 的任一树枝，则通过下述五种方式之 一所得到的任何一个树，均是s 的一个语句袁列： 融】b 。0 【i 。其中是b 上某个公式0 【的一个a 子公式 略】b 。p l i 1 p n 其中p 1 ，艮是b 上某公式p 的p 子公式序列 丫】b 。丫( t ) 。其中丫是b 上的某个公式，t 是一个基项。 【6 】b 。6 ( c ) 。其中8 是b 上的某个公式，c 相对于s 和t 是一个新 的常量。 i f 】b 。f 。其中f 是s 中的任一语句 3 只有能由步骤1 、2 得到的树，才是s 的语句表列 在上述定义中，m 、嵋】、m 、【6 】统称作推理规则，口】称作公式规则。若t 是单元集 x ) 的一个语句表列，则称t 是x 的一个语句表列。 语句表列的封闭、s l 表列证明、s l 的内定理等概念与第1 章中的定义是相 似的，这里不再重述。例如，下面便是对公式x = 3 x v y a ( x , y ) d v y 3 xa ( k y ) 的一 个表列证明： ( 1 ) 1 ( 3 x v y a ( x , y ) 3v y 3 x a ( x , ”) ；0 c ( 1 ) ( 2 ) 3 x v y a ( x ，” ；0 【( 1 ) ( 3 ) 1 v y 3 x a ( x ，y ) ；6 ( 2 ) ( 4 ) v y a ( a , y ) i 6 ( 3 ) ( 5 ) 1 j x a ( x ，b ) i y ( 5 ) ( 6 ) 1 a 仇b ) ；y ( 4 ) ( 7 ) a 伍b ) 2 2 语句表列的可靠性与完全性 s l 是可靠的和完全的，其证明均与s o 的可靠性与完全性的证明相类似。s o 的完全性证明需要用到“完成的表列”概念，s l 的完全性证明有一个相应的概念 “系统化表列( s y s t e m a t i ct a b l e a u x ) 。 当依据定义去构造一个表列时，构造过程的每一步都会有多种选择。所以， 表列演算是非确定性的( i n d e t e r m i n i s t i c ) 。不过，人们可以给出一个程序，使得 当依此程序去构造表列时，每一步都是确定的( d e t e r m i n i s t i c ) 。这种依程序构造 出的表列就是系统化表列。为获得确定性，需解决： ( 1 ) 表列构造的每一步各要处理哪个公式； ( 2 ) 当应用量词规则时，要选择哪个项去例示( i m t a n t h t e ) 相应的变元： ( 3 当输入集为无限集时，要确保输入集的每一元素均会得到处理。 定义2 2 ( 可用节点)如果表列t 含有带数字标签的节点”，则在带有 最小标签的所有节点中，深度最小、最靠左侧( d e p t h - l e a s t , l e f t - m o s t ) 的那 个节点便是t 的可用节点；如果t 中没有带数字标签的节点，则t 无可用 3 3 这里我们考虑的表列中，某些节点将含有两类标签：公式标签和数字标签。 1 6 节点。 定义2 2 用来解决问题( 1 ) 。为解决后两个问题，便需要分别在封闭项的集 合和公式的集合上引入一个全序： 定义2 3 ( 系统化的表列( 序列) )设兀是一个从非负整数集n o 到基项集上的映上函数，一 是一阶语言l 的公式集上的一个全序，s 是 一个闭公式集，是s 中模一 最小的公式。s 的关于兀和 的系统化表 列序列是如下定义的s 的表列序列t 1 根节点上的公式为西，数字标签为0 的单节点表列t o 是t 的第一个元素 2 若t n 是t 的第n 个元素，且t n 含有带数字标签的节点， 设其可用节点为n ，n 带公式标签f ，数字标签k ，且s 中有公式 不出现在通过n 的某个树枝中，令g 代表这样的公式中模 是r 一一致的。 a 3 ：若丫s ，则 s ，丫( a ) ) 是r 一一致的。 ：若8 s ，则 s ，6 ( a ) ) 是f 一一致的，其中a 不出现在s 中。 定义2 6 ( 综舍的相容性) 3 8 称a 是一个“综合的相容性( s y n t h e t i c c o n s i s t e m yp r o p e r t y ) ”，若对任意s 、丫、6 均有： b o ：若s 是真值函项不一致的，则若s 是不一致的。 b i ：若 s ，丫) 是_ 一致的，则 s ，丫( a ) ) 也是- 一致的。 b 2 ：若 s ，6 ) 是一一致的，且a 不出现在 s ，8 ) 中，则 s ，8 ，6 ( a ) ) 也 是一致的。 b 3 ：若s 是一致的，则对任一句子x ， s ，) 和 s ，f x ) 中至少 有一个是- 一致的。 条件b 3 又称切割条件。 定义2 7 ( ( 一阶) 欣迪卡集) 3 9 对论域u 而言的一个欣迪卡集是一个 满足下述条件的集合s ： h o ：没有e u 中的一个原子公式及其否定同时属于s 。4 0 h i ：若a s ，则a l s 且a 2 s h 2 ：若p s ，则p l s 或p 2 s 。 h 3 ：若7 e s ，则对任一k u ，丫s 。 h 4 ：若8 s ，则存在k e u ，6 0 ( ) s 。 定义2 8 ( ( 一阶) 真值集) 4 1 对论域u 而言的一个真值集s 是一个满 足下述条件的e u 的子集： 勰s m u l l y a n , r m f i r s t - o r d e r l o g i c 【m 】d o v e rp u b l i c a t i o n s ，i n c 1 9 9 5 9 2 辨s m u l l y a n , i lm f i r s t - o r d e rl o g i c 【m 】d o v e rp u b l i c a t i o n s ，i n c 1 9 9 5 5 7 柏关于e u 的详细定义，请参见：s m u l l y a n , i lm f i r s t - o r d e r l o g i ci m i d o v e r p u b l i c a t i o n s i n c 1 9 9 5 4 6 - 4 7 4 1 s m u l l y m , m f i r s t - o r d e r l o g i c 【m 】d o v e rp u b l i c a t i o n s ，i n c 1 9 9 5 4 7 2 0 s o ：t x 与f x 中有且仅有一个公式属于s 。 s l ：a s ，当且仅当，a l s 且0 c 2 s s 2 ：p s ，当且仅当，8 1 s 或p 2 s 。 s 3 ：v x a e s ；当且仅当对任一k e u ，氚x s 。 s 4 ：了x a s ，当且仅当存在k u ，h k x s 。 s l 的完全性证明的要点是：证明任一分析一致的集合都是可满足的。为此， 需要采取的步骤是：先将一个分析一致的集合扩张为一个欣迪卡集，再将一个欣 迪卡集扩张为一个真值集。4 2 这一过程与人们熟悉的公理系统完全性证明是有区 别的，后者的证明要点是：任一综合一致的集合都是可满足的。它的相应步骤是： 直接将一个具有综合相容性的集合扩张为一个真值集。4 3 前一种证明路线是林登 堡姆辛钦( l i n d e n b a u m - h e n k i n ) 式的，后一种证明路线是哥德尔艾尔伯朗根 岑( g 甜e l - h e r b r a a d - g e n t z e n ) 式的。4 4 2 3 自由变元表列 s l 的丫规则的一个弱点是：在尚不清楚例示是否会对树枝的封闭发挥作用 时，就不得不应用丫规则。为解决这一问题，可在表列中引入自由变元以推迟对 项的选择，并且仅当某个例示能封闭某个树枝时，才去使用这个例示。如此发展 的表列演算，便称作自由变元表列演算。自由表列演算要完成的一个重要任务是： 寻找一个代入a ，使得对某树枝上的文字l 和k ，有：k 6 = 一k 。为解决此问题， 便需要将“合一( u n i f i c a t b n ) ”概念引入表列演算。4 5 一、合一 4 2 c f s m u l l y a a , r m f i r s t - o r d e r l o g i c 【m 】d o v e rp u b l i c a t i o n s ，i n c 1 9 9 5 5 7 - 6 0 村h