《模态逻辑形式系统.ppt》由会员分享，可在线阅读，更多相关《模态逻辑形式系统.ppt（55页珍藏版）》请在三一办公上搜索。
1、第6章 模态逻辑,2,本章内容,1 模态逻辑介绍2 模态命题逻辑形式系统3 NSK元理论4 其他正规系统5 模态词的归约,3,1模态逻辑（Modal Logic）介绍,逻辑的一个分支，研究必然、可能及其相关概念的逻辑性质。模态词：表示事物的“势态”、人的“情态”、过程的“变迁”的词，如“必然、可能”、“应该、允许”、“知道、认可”、“一贯、偶然”等。逻辑学中，有狭义模态和广义模态之分。狭义模态：涉及必然性和偶然性的模态。从某种观点来看，它们表达的是命题的真假强度，因此，也称为真值模态。例如：“物体间存在着引力是必然的”“火星上可能有人”,4,广义模态：涉及命题本身所具有的非真值函项的种种性质的
2、模态。广义模态词：必然、可能真理论模态逻辑应该、允许、禁止道义论模态逻辑知道、相信、可接受、可疑、可证认识论模态逻辑曾经、总是、将是时序逻辑一贯、偶然、经验的、有先例的经验论模态逻辑优先、中立等价值论模态逻辑比如：“子女赡养父母是应该的”“宇宙间存在着黑洞是可信的”,模态逻辑介绍（续）,5,模态逻辑引入,逻辑系统的发展命题逻辑一阶谓词逻辑，扩充命题逻辑系统的描述能力。模态逻辑，扩充一阶谓词逻辑和命题逻辑的描述能力。命题逻辑的不足：原子命题不能细化，不能完全描述现实世界中的问题。,6,命题逻辑和一阶谓词逻辑的不足：都不能描述有时间、地点概念的变化。有些命题是否成立与其所在的时间和场合有关系。例如
3、：A：“太阳系有八颗行星。”B：“汽车是一个必备的生活工具。”C：“112”用模态逻辑来描述这样的时间与场合上的概念。对于在某些场合成立的命题，规定为“可能真”的。对于在所有场合都为真的命题，规定为“必然真”的。,模态逻辑引入（续1）,7,模态命题：陈述事物情况的必然性或可能性的命题。反映人们对客观事物认识的程度。模态逻辑中，对必然和可能的描述：可能A：A，命题A至少在一个可以实现的场合中成立。必然A：A，命题A在所有能够实现的场合中成立。,模态逻辑引入（续2）,8,模态逻辑的实质,命题逻辑和一阶谓词逻辑的扩充引入了两个模态词(必然/、可能/)场合之间的“可达”关系 场合从目前所处的场合是否可
4、以实现（到达）。模态词：表示在当前场合可以达到的场合中都是成立的模态词：表示在当前场合可以达到的场合中，至少有一个是成立的场合与现实之间的关系 程序模块、时间段、地理位置等在模态逻辑中，称这些不同的场合为可能世界。,9,基本模态概念,真命题，区分为必然真的命题和并非必然真的命题假命题，区分为必然假的命题和并非必然假的命题必然命题：必然真的命题，也称为必真命题。不可能是假的命题。不可能命题：必然假的命题。可能命题：并非不可能的命题。可能命题包括所有的真命题（必然命题和并非必然的命题），即除不可能命题以外的所有命题。偶然命题：既非必然又非不可能的命题。,10,真命题：“在实际世界中为真”的命题。例
5、如：“尼克松在1969年成为总统。”必然命题：“在所有可能世界中都为真”的命题。例如：“所有单身汉都是未婚的。”不可能命题：“不在可能世界中为真”的命题，也称为“必然假命题”。例如：张三 和 李四 同时比对方高。可能命题：“至少在一个可能世界中为真”的命题。例如：“明天不下雨”、“这个地区有石油”偶然命题：“在一些可能世界中为真，在另外一些可能世界中为假”的命题。比如：“尼克松在1969年成为总统。”偶然为真“休伯特汉弗莱在1969年成为总统。”偶然为假,基本模态概念（续1）,11,“模态”概念：“必然性”、“不可能性”、“偶然性”、“可能性”指的是逻辑上的必然性、不可能性、偶然性、可能性。可
6、以根据它们中的任何一个概念来解释其余三个概念。“必然”的含义：无论事物是怎样的、也无论世界是怎样的，这个命题都不可能不真。如命题：所有单身汉都是未婚的。再如命题：没有物体的运动速度比光速更快。“命题P是必然真的”等价于“P是假的是不可能的”。“P是可能真的”等价于“P是假的不是必然为真的”。,基本模态概念（续2）,12,由命题A可以形成命题：A是必然的，表述为：必然A。当A是必然命题时，“必然A”为真；否则为假。“必然”：一元命题形成算子，不是真值函项算子。A假，可确定命题“必然A”是假的。A真，可否确定“必然A”的真假？不能。A真分为两种情况：A必然真和并非必然真。对于前者：“必然A”真，对
7、于后者：“必然A”假。“可能”：一元命题形成算子，不是真值函项算子。A真，可确定命题“可能A”是真的。A假，可否确定“可能A”的真假？不能。A假分为A必然假和并非必然假。对于前者，“可能A”假，对于后者，“可能A”真。“必然”和“可能”算子称作模态算子。,基本模态概念（续3）,13,模态命题演算基于命题演算。FSPC的公理、定理、推导规则等，在模态系统中仍然有效，且其解释和以前一样，包括其初始变形规则，如一致代入规则、分离规则和置换规则等。模态算子不是真值函项算子。意味着它们不可能由PC的算子（如、及它们的复合）来表示，因为PC的算子都是真值函项算子。模态命题逻辑是对FSPC进行扩充得到的。引
8、入新的模态算子，并扩充了公式的种类。增加“必然”算子/L、“可能”算子/M 并允许它们把任何公式作为自变元。如：(pq)（意思是：“必然 p或q”）pq（意思是：“必然p 或 q”）,基本模态概念（续4）,14,如果和被解释为必然性和可能性算子，则下面的等价式应该是有效的：pp，pp 包含这些等价式的系统无须将和都作为初始符号：将作为初始符号，并定义=这样的系统称为-基系统。将作为初始符号，并定义=这样的系统称为-基系统。,对模态系统的直观要求,15,模态算子不是真值函项。在任一直观上似乎合理的模态系统中，p必定不与p的任何真值函项等价。对于p，只有四个性质不同的真值函项：f p自身 p的否定
9、 t 下面所列出的公式是不是有效的？pp pp ppp ppp,对模态系统的直观要求（续1）,16,pp 是有效的（尽管pp不是有效的）。必然性公理，简单地表达了必然真为真的原理。一个类似的原理：真的是可能的。用公式 pp 表达。这个公式同样被认为是有效的。任何一个具有有效公式形式的命题不仅是真的，而且是必然真的。即：如果是一个有效的公式，那么不仅具有形式的每个命题都是真的，而且具有形式的每个命题也都是真的，而且，也是有效的。因此，希望在一个模态逻辑中得到这样一个定理：如果是有效的，那么也是有效的。在一个公理化模态系统中，希望有这样一个规则：如果是一个命题，那么也是一个命题。,对模态系统的直观
10、要求（续2）,17,模态逻辑的简单(语义)性质,直觉上的语义关系A A A A(AA)AA(A和A可能同时成立）(AA)(A和A不可能同时成立)AA AA AA(AB)AB AB(AB)(AB)AB(AB)AB(AB)(AB)如何理解：A、A、A、A、,18,2模态命题逻辑形式系统,模态命题演算是现代模态逻辑的基本内容之一。是应用数理逻辑的方法研究模态命题逻辑的结果。模态逻辑形式系统与FSPC类似。模态逻辑形式系统根据对模态词的不同的解释形成不同的形式系统，称为正规系统(Normal System)。NSK 是最简单的正规系统。NSKD NSKTNSKBNSK4NSK5,19,NSK系统构成,
11、NSK系统的构成：语言部分+推理部分NSK系统语言部分 符号表：P1,P2,(,)其中：Pi为原子命题，,为联接词，,为模态词，(,)为技术符号。项集：空集。公式集：公式递归定义如下：1)Pi为公式(i=1,2,3,4,)2)如A,B为公式,那么(A),(AB),(A),(A)都是公式 3)除由有限次使用1),2)得到公式外,没有别的东西是公式。（说明：,的优先级与的相同。公式中括号的省略规则同前。）,20,NSK系统推理部分 公理集：包含以下公理模式 A1:AA AA A2:(AB)(AB)(公理K)A3：全部重言式 A4：A(当A为公理)推理规则模式（分离规则rmp）：AB,A B 例如：
12、(AB)(AB),AAA(A1(A2(A3A4)(A1(A2(A3A4)(A1(A2(A3A4)(A1(A2(A3A4),NSK系统构成（续）,21,NSK性质,性质1：如果公式A是NSK的定理，那么A也式NSK的定理；即如果NSKA，则NSKA。证明：NSKA 存在A的证明序列 A1,A2,An(=A)对证明序列的长度 l 归纳证明：当l=1时，A为公理，根据A4，A也是公理，NSKA成立。假设l n时，命题成立。当l=n时，设An是由Ai和Aj根据分离规则得到的，i,jn，不妨设Aj=AiAn 根据归纳假设，有(AiAn)和 Ai 都是定理。根据公理K，(AiAn)AiAn,所以，AiAn
13、是定理。根据分离规则有：AiAn,AiAn，即NSKAn成立。因此，命题成立。,22,性质2：设A1、A2、An和 A 均为NSK的公式，如果NSK(A1(A2(AkA)，则NSK(A1(A2(AkA)成立。即：设A1,A2,An和A均为NSK的公式，如果NSKA1A2AkA，则NSK(A1A2Ak)A成立。,NSK性质（续1）,23,性质3：如果公式A是NSK的定理，那么A也是NSK的定理。证明：由于A是NSK的定理，即NSKA；根据性质1有：A是定理，即NSKA;利用公理A1有：NSKA,因此NSKA成立。所以A是NSK的定理。,NSK性质（续2）,24,性质4：如果AB为NSK的定理，那
14、么AB亦然。即：如果NSKAB，则NSKAB。（证明提示：对BA 利用性质2）性质4推广：如果NSKA(A1Ak)则NSKA(A1Ak)AB=BA 根据性质2有：BA 所以：AB=AB,NSK性质（续3）,25,性质5：对任何公式A,B，下列各式均为NSK的定理：(1)(AB)AB(2)AB(AB)(3)(AB)AB(4)(AB)AB(5)(AB)(AB)（公理K的对偶K）(6)(AB)(AB),NSK性质（续4）,26,性质6：设A是NSK的公式，A是把公式A中的和分别全部改为k和k所得的公式。那么，如果A是NSK的定理，则A仍为NSK的定理。即如果NSKA,则NSKA。证明提示：A是定理，
15、存在A的证明序列。对证明序列的长度进行归纳证明。若A是公理，则A肯定是NSK的定理，因为：A1:NSKkA kA NSKkA kA A2:NSKk(AB)(kAkB)（公理K）A3：若A是重言式，则A也必为重言式。A4：NSKA 蕴含NSKkA,NSK性质（续5）,27,划一定理,(1)(AB)(AB)(2)(AB)(AB),28,正规系统语义,Leibniz首先用“可能世界”来解释模态词。A，在一切可能世界中，A真。A，存在可能世界，使A真。每个命题的真假都和可能世界之间有着密切的关系，每个可能世界对应于不同的场合。所有的可能世界构成一个可能世界的集合。可能世界之间是可变换的。从一个可能世界
16、能否变换到另一个可能世界，在赋予真值时是非常重要的。如果一个可能世界不能变换到其他的可能世界上，那么在这个可能世界所讨论的A和A真都是指A真这一个概念。将Kripke语义结构稍加改进，作为解释模态逻辑的可能世界的语义结构。,29,正规结构-正规系统的语义结构,正规结构定义为三元组，其中：U：一非空集合，称为宇宙，其成员wi是可能世界。R：U上的一个二元关系，称为可能世界之间的可到达关系。I：从UP1,P2,P3,到0,1的映射，即在每一个可能世界wi中，对每一原子命题Pj的赋值。例如：I(wi,Pj)=1 表示在可能世界wi中给命题Pj赋值真。I(wj,Pk)=0 表示在可能世界wj中给命题P
17、k赋值假。通常，I可用U的一个子集序列1,2,3,来表示，这里，i是给原子命题Pi赋值真的可能世界的集合。即：I(w,Pi)=1 当且仅当 wi(i=1,2,3,),30,正规系统NSK是合理的、完备的。,正规结构（续）,正规结构中的赋值规定：,NSK系统是相当弱的。AA，AA，AA等直觉上认为真的公式均非NSK的定理。AA永真，要求可到达关系R是连续的。AA永真，要求可到达关系R是自反的。,31,例：,设宇宙K=w1,w6；可到达关系用表示，R=w1w3,w1w5,w2w4w6。这里，并不是说R就是偏序关系或者小于关系。,可到达关系的结构，可用右图表示：,32,例（续）,33,3NSK元理论
18、,从语法构成、语构语义关系两方面来说明。语法构成NSK是独立的 若把公理A从NSK中删除后，所得系统不满足A。NSK是一致的 不存在NSK的公式A，使得NSkA 和NSkA 同时成立。NSK是不完全的 存在公式A，使NSkA 和NSkA 都不成立。NSK是可判定的 对任一公式A，可在有限步骤内判定A是否为定理。演绎定理：对NSK中任何公式集，及公式A,B,NSKAB，当且仅当,ANSKB。,34,替换原理：在NSK中，如果AB，A为C的子公式，而D是将C中的若干个A替换为B之后得到的公式，则CD。对偶原理：对NSK中的任何公式A，NSK AA*，其中A*为A的对偶，且运算*递归地定义如下：(1
19、)Pi*=Pi(i=1,2,)(2)(A)*=A*(3)(AB)*=A*B*(4)(AB)*=A*B*(5)(AB)*=A*B*(6)(A)*=A*(7)(A)*=A*,练习：1）构造公理K的对偶：(AB)(AB)2）构造K的对偶：(AB)(AB),语法构成,35,对NSK中的任何公式A，B，有NSKA 蕴涵 NSKA*，NSKA 蕴涵 NSKA*NSKAB 蕴涵NSKB*A*NSKAB 蕴涵NSKA*B*这里，蕴涵后件称为其前件的对偶定理。公理K的对偶定理K：(AB)(AB)A1中AA的对偶定理：AA A1中AA的对偶定理：AA,语法构成（续1）,36,用表示由,和组成的符号串，*表示其对偶
20、符号串，即将中的改为，改为后得到的。(1)NSK A*A(2)NSK A 当且仅当NSK*A(3)NSK AA 当且仅当NSK*A*A(4)NSK AA 当且仅当NSK*A*A设,的意义如上，且满足：符号的出现均为偶数次，设A，B为NSK的任意公式，那么，NSK AA 当且仅当下列条件之一成立：(1)NSK*A*A(2)若NSK AB，则NSK AB(3)若NSK AB，则NSK*A*B,语法构成（续2）,37,语构语义关系,合理性 NSK是合理的，即如果对公式A，有A，则 A。完备性 NSK是完备的，即如果对公式A，有 A，则A。,38,4其他正规系统,在NSK的公理系统中加入不同的公理模式
21、后可以得到不同的正规系统。KD系统D：AA(D：AA)KT系统T：AA(T：AA)KB系统B：B：AA(B：AA)K4系统4：AA(4：AA)K5系统5：AA(5：AA),39,可到达关系R的性质,连续性自反性对称性传递性欧几里德性质,40,R的连续性,如果宇宙中的每一个可能世界都有一个R后继。则R是连续的。,为了使 AA 永真，必须限制R为连续的。即：D：AA R是连续的。,41,R的自反性,如果R满足 wRw,则称R为自反的。直觉上，认为AA，AA 应该是成立的。但在模态逻辑中，未必成立。,为使这两个公式成立，只需R是自反的。因此可知，公理T与可达关系的自反性是相对应的，即T：AA R是自
22、反的。如果R满足自反性，则R必然是连续的。如果R是自反的，则公理D和T同时是永真式。为保证形式系统的独立性，可以将公理D删除。,42,R的对称性,对U中元素w,如果有w1Rw2,则有w2Rw1,则R是对称的。公理B(AA)在KD、KT中均不是永真的。,即，在可能世界w中，AA不成立。当R满足对称性时，公理B(AA)永真。即B:AA R 是对称的。,43,R的传递性,对宇宙中的可能世界w1,w2,w3，如果w1Rw2、w2Rw3成立，则有w1Rw3，称关系R是传递的。如果R满足传递性，则公理4：AA成立。例：若w1Rw2、w2Rw3成立，但 w1Rw3 不成立,则公理4对应R的传递性，即公理4：
23、AA R是传递的。,44,R的欧几里德性质,对宇宙中的任意可能世界w1,w2,w3，若w1Rw2,w1Rw3，那么w2Rw3，则称R具有欧几里德性质。公理5（AA）永真要求R具有欧几里德性质。,45,公理5与R的欧几里德性质对应，即：公理5：AA R具有欧几里德性质。,R的欧几里德性质(续）,46,可达关系小结,D：AA R是连续的T：AA R是自反的B:AA R 是对称的4：AA R是传递的5：AA R具有欧几里德性质R具有对称性和传递性=R具有欧几里德性质 满足公理B及公理4的结构满足公理5R具有对称性和欧几里德性质=R具有传递性 满足公理B及公理5的结构满足公理4在NSK中同时加入公理D
24、、T、B、4、5中的几个，可以得到更强的正规系统。如：KB4、KB5、S4、S5,47,5模态词的归约,讨论由,组成的符号串。用表示空串。在正规系统NS中,若对一切公式A有NSAA，那么称NS中的模态词与等价。若的长度小于等于的长度，那么称模态词可归约于。如：等价于，等价于。在KT4中，AA，因而 AA对任意正规系统NS，若模态词含有偶数个，那么存在一个不含的模态词，使得可归约于。若模态词含有奇数个，那么存在一个不含的模态词，使得可归约于。(AA,AA，AA),48,S4（KT4）的模态词,公理T：AA(T：AA)公理4：AA(4：AA)对任何公式A，S4有定理：(1)AA(AA)(2)AA(
25、AA)例：A=A=A=AS4中的所有模态词均可归约于14个模态词之一，即：、及它们的否定。,49,K5的模态词,公理5：AA(5：AA)对任意公式A，K5中有定理：(1)AA(AA)(2)AA(AA)(3)AA(AA)(4)AA(AA)例：在K5中归约 A=A=A=A=A=AK5的所有模态词均可归约于14个模态词之一，即：、及它们的否定。,50,KD5的模态词,公理D：AA公理5：AA(5：AA)在KD5中，K5的定理仍成立。在KD5中，对任何公式A，有定理：(1)AA(2)AA例：在KD5中归约 A=A=A=A=AKD5的所有模态词均可归约于10个模态词之一，即：、(/)、(/)及它们的否定
26、。,51,K45的模态词,公理4：AA(4：AA)公理5：AA(5：AA)在K45中，K5中的定理仍然成立。在K45中，对任何公式A，有定理：(1)AA(2)AA例：在K45中归约 A=A=A=A=AK45的所有模态词均可归约于10个模态词之一，即：、及它们的否定。,52,KD45的模态词,公理D：AA公理4：AA(4：AA)公理5：AA(5：AA)在KD45中，K45的定理仍成立。在KD45中，对任何公式A，有定理：(1)AA(2)AA例：在KD45中归约 A=A=A=A=AKD45的所有模态词均可归约于6个模态词之一，即：、及它们的否定。,53,S5的模态词,S5，即KT5，是KD45的扩充。公理D：AA公理4：AA(4：AA)公理5：AA(5：AA)公理T：AA(T：AA)S5的所有模态词均可归约于6个模态词之一，即：、及它们的否定。练习：在S5中化简公式 A,54,小结,模态词,的含义NSK系统的组成：语言+理论（公理模式+推理规则模式）NSK系统的性质：6个划一定理NSK中公式解释：,55,小结（续）,NSK元理论：演绎定理、替换原理、对偶原理其它正规系统：KD D：AA(D：AA)KT T：AA(T：AA)KB B：AA(B：AA)K4 4：AA(4：AA)K5 5：AA(5：AA)可到达关系R的性质连续性、自反性、对称性、传递性、欧几里德性质模态词归约,
