6--chapter6--模态逻辑形式系统.ppt

LI Wensheng, SCST, BUPT 李文生北京邮电大学 计算机学院 wenshli@ 010-62282929第6章 模态逻辑1wenshli@本章内容1 模态逻辑介绍 2 模态命题逻辑形式系统 3 NSK元理论 4 其他正规系统 5 模态词的归约2wenshli@1．模态逻辑（Modal Logic）介绍n逻辑的一个分支，研究必然、可能及其相关概念的逻 辑性质n模态词：表示事物的“势态”、人的“情态”、过程 的“变迁”的词，如“必然、可能”、“应该、允许 ”、“知道、认可”、“一贯、偶然”等n逻辑学中，有狭义模态和广义模态之分n狭义模态：涉及必然性和偶然性的模态 从某种观点来看，它们表达的是命题的真假强度，因 此，也称为真值模态例如： “物体间存在着引力是必然的” “火星上可能有人”3wenshli@n广义模态：涉及命题本身所具有的非真值函项的种种 性质的模态n广义模态词： 必然、可能——真理论模态逻辑 应该、允许、禁止——道义论模态逻辑 知道、相信、可接受、可疑、可证——认识论模态逻辑 曾经、总是、将是——时序逻辑 一贯、偶然、经验的、有先例的——经验论模态逻辑 优先、中立等——价值论模态逻辑n比如： “子女赡养父母是应该的” “宇宙间存在着黑洞是可信的” 模态逻辑介绍（续）4wenshli@模态逻辑引入n逻辑系统的发展 Ø命题逻辑 Ø一阶谓词逻辑，扩充命题逻辑系统的描述能力。

Ø模态逻辑，扩充一阶谓词逻辑和命题逻辑的描述能力n命题逻辑的不足：原子命题不能细化，不能完全描述 现实世界中的问题 Ø如：所有实数的平方都是非负的3 是实数3 的平方是非负的n一阶谓词逻辑利用谓词、函词和量词来解决这样的问 题x(R(x)P((x))) R(-3 )P((-3 )) 5wenshli@n命题逻辑和一阶谓词逻辑的不足： Ø都不能描述有时间、地点概念的变化 Ø……n有些命题是否成立与其所在的时间和场合有关系例 如： A：“太阳系有八颗行星 B：“汽车是一个必备的生活工具 C：“1＋1＝2” n用模态逻辑来描述这样的时间与场合上的概念 Ø对于在某些场合成立的命题，规定为“可能真”的 Ø对于在所有场合都为真的命题，规定为“必然真”的模态逻辑引入（续1）6wenshli@n模态命题：陈述事物情况的必然性或可能性的命题 反映人们对客观事物认识的程度n模态逻辑中，对必然和可能的描述： Ø可能A：◇A，命题A至少在一个可以实现的场合中成立 Ø必然A：□A，命题A在所有能够实现的场合中成立模态逻辑引入（续2）7wenshli@模态逻辑的实质 n命题逻辑和一阶谓词逻辑的扩充 Ø引入了两个模态词(必然/□ 、可能/◇) n场合之间的“可达”关系 Ø场合从目前所处的场合是否可以实现（到达）。

Ø模态词□：表示在当前场合可以达到的场合中都是成立的 Ø模态词◇：表示在当前场合可以达到的场合中，至少有一 个是成立的n场合与现实之间的关系 Ø程序模块、时间段、地理位置等n在模态逻辑中，称这些不同的场合为可能世界 8wenshli@基本模态概念 n真命题，区分为必然真的命题和并非必然真的命题n假命题，区分为必然假的命题和并非必然假的命题n必然命题：必然真的命题，也称为必真命题 不可能是假的命题n不可能命题：必然假的命题n可能命题：并非不可能的命题n可能命题包括所有的真命题（必然命题和并非必然的 命题），即除不可能命题以外的所有命题n偶然命题：既非必然又非不可能的命题9wenshli@n真命题：“在实际世界中为真”的命题 例如：“尼克松在1969年成为总统n必然命题：“在所有可能世界中都为真”的命题 例如： “所有单身汉都是未婚的 n不可能命题：“不在可能世界中为真”的命题，也称 为“必然假命题” 例如：张三 和 李四 同时比对方高n可能命题：“至少在一个可能世界中为真”的命题 例如：“明天不下雨” 、“这个地区有石油”n偶然命题：“在一些可能世界中为真，在另外一些可 能世界中为假”的命题。

比如：“尼克松在1969年成为总统 偶然为真“休伯特·汉弗莱在1969年成为总统 偶然为假基本模态概念（续1） 10wenshli@n“模态”概念： Ø“必然性”、 “不可能性”、 “偶然性”、“可能性” 指的是逻辑上的必然性、不可能性、偶然性、可能性 Ø可以根据它们中的任何一个概念来解释其余三个概念n“必然”的含义： 无论事物是怎样的、也无论世界是怎样的，这个命题 都不可能不真 如命题：所有单身汉都是未婚的 再如命题：没有物体的运动速度比光速更快n“命题P是必然真的” 等价于 “P是假的是不可能的 ”P是可能真的” 等价于 “P是假的不是必然为真 的”基本模态概念（续2） 11wenshli@n由命题A可以形成命题：A是必然的，表述为：必然A n当A是必然命题时，“必然A”为真；否则为假n“必然”：一元命题形成算子，不是真值函项算子 ØA假，可确定命题“必然A”是假的 ØA真，可否确定“必然A”的真假？不能A真分为两种情况：A必然真和并非必然真 对于前者：“必然A”真，对于后者：“必然A”假n“可能”：一元命题形成算子，不是真值函项算子 ØA真，可确定命题“可能A”是真的。

ØA假，可否确定“可能A”的真假？ 不能A假分为A必然假和并非必然假 对于前者，“可能A”假，对于后者，“可能A”真n“必然”和“可能”算子称作模态算子基本模态概念（续3） 12wenshli@n模态命题演算基于命题演算FSPC的公理、定理、推导规则等，在模态系统中仍 然有效，且其解释和以前一样，包括其初始变形规则 ，如一致代入规则、分离规则和置换规则等n模态算子不是真值函项算子意味着它们不可能由PC的算子（如、、及它们 的复合）来表示，因为PC的算子都是真值函项算子n模态命题逻辑是对FSPC进行扩充得到的 引入新的模态算子，并扩充了公式的种类 Ø增加“必然”算子☐/L、 “可能”算子/M并允许它们把任何公式作为自变元如：☐(pq)（意思是：“必然 p或q”）☐pq （意思是： “必然p 或 q”）基本模态概念（续4） 13wenshli@n如果☐和被解释为必然性和可能性算子，则下面的 等价式应该是有效的：☐pp，p☐p包含这些等价式的系统无须将☐和都作为初始符 号：将☐作为初始符号，并定义 =☐这样的系统称为☐-基系统将作为初始符号，并定义 ☐=这样的系统称为-基系统。

对模态系统的直观要求14wenshli@n模态算子不是真值函项在任一直观上似乎合理的模态系统中，☐p必定不与 p的任何真值函项等价对于p，只有四个性质不同的真值函项：fp自身p的否定t下面所列出的公式是不是有效的？☐pp ☐pp☐ppp ☐pppp f1 f2 f3 f40 0 0 1 11 0 1 0 1对模态系统的直观要求（续1）15wenshli@n☐pp 是有效的（尽管☐pp不是有效的） ‘必然性公理’，简单地表达了必然真为真的原理 一个类似的原理：真的是可能的用公式 pp 表达这个公式同样被认为是有效的n任何一个具有有效公式形式的命题不仅是真的，而且 是必然真的即：如果是一个有效的公式，那么不仅具有形式的 每个命题都是真的，而且具有形式☐的每个命题也 都是真的，而且，☐ 也是有效的因此，希望在一个模态逻辑中得到这样一个定理：如果是有效的，那么☐也是有效的在一个公理化模态系统中，希望有这样一个规则：如果是一个命题，那么☐也是一个命题。

对模态系统的直观要求（续2）16wenshli@模态逻辑的简单(语义)性质 n直觉上的语义关系 □A  ◇A ◇A  □A □(AA) ◇A◇A (◇A和◇A可能同时成立 ） (□A□A) (□A和□A不可能同时成立) □AA A◇A □A◇A □(AB)  □A□B □A□B  □(AB) ◇(AB)  ◇A◇B ◇(AB)  ◇A◇Bn□(AB)(□A□B) n如何理解：□◇□A、◇□◇□A、◇□◇□□A、 ◇□◇◇□A、……17wenshli@2．模态命题逻辑形式系统n模态命题演算是现代模态逻辑的基本内容之一 是应用数理逻辑的方法研究模态命题逻辑的结果n模态逻辑形式系统与FSPC类似n模态逻辑形式系统根据对模态词的不同的解释形成不 同的形式系统，称为正规系统(Normal System)nNSK 是最简单的正规系统 NSKD NSKT NSKB NSK4 NSK518wenshli@NSK系统构成 nNSK系统的构成：语言部分+推理部分nNSK系统语言部分 Ø符号表：{P1,P2,…, ,,□,◇,(,) } 其中：Pi为原子命题，, 为联接词，□,◇为模态词，(,)为技术符号。

Ø项集：空集 Ø公式集：公式递归定义如下：1)Pi为公式(i=1,2,3,4,……) 2)如A,B为公式,那么(A),(AB),(□A),(◇A)都是公式3)除由有限次使用1),2)得到公式外,没有别的东西是公式 （说明： □,◇的优先级与的相同公式中括号的省略规则同前 19wenshli@nNSK系统推理部分 Ø公理集：包含以下公理模式A1: □A◇A ◇A□AA2: □(AB)(□A□B) (公理K)A3：全部重言式 A4：□A (当A为公理) Ø推理规则模式（分离规则rmp）：AB, A┝ B n例如： □(AB)◇(AB), □A◇A◇A □(A1(A2(A3A4)))(□A1□(A2(A3A4))) (□A1(□A2□(A3A4))) (□A1(□A2(□A3□A4)))NSK系统构成（续） 20wenshli@NSK性质 性质1：如果公式A是NSK的定理，那么□A也式NSK的定理；即如果├NSKA，则├NSK□A 证明：∵├NSKA ∴ 存在A的证明序列 A1,A2,…,An(=A) 对证明序列的长度 l 归纳证明： 当l =1时，A为公理，根据A4，□A也是公理，├NSK□A成立。

假设l ├BA n根据性质2有：├￿B￿A 所以： ├￿A￿B ==> ├◇A◇BNSK性质（续3） 24wenshli@性质5：对任何公式A,B，下列各式均为NSK的定理： (1) □(AB)□A□B (2) □A□B□(AB) (3) ◇(AB)◇A◇B (4) ◇(AB)◇A◇B (5) (◇A◇B)◇(AB) （公理K的对偶K◇） (6) ◇(AB)(￿A◇B)NSK性质（续4） 25wenshli@性质6：设A是NSK的公式，A是把公式。