《书眉模态逻辑讲义-中山大学逻辑与认知研究所.docx》由会员分享，可在线阅读，更多相关《书眉模态逻辑讲义-中山大学逻辑与认知研究所.docx（273页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、模态逻辑讲义（2006 年）李小五编著中山大学逻辑与认知研究所第1章公理化系统在本章1我们给出模态语言和模态公式，讨论它们的语 形特性，引入刻画模态的公理和推理规则，然后定义本书主要 关注的公理化系统，并定义相对模态系统的形式证明和推演概 念。最后我们证明这些系统是协调和和谐的。从2到5我们分别介绍初等系统、基本系统、退化系统 和其他重要系统，着重证明这些系统的内定理和导出规则以及 这些系统之间的相互关系。我们也证明某些系统的元定理，例如，等价置换定理、对 偶公式定理、对偶符串定理、演绎定理、归约定理、Post-完备 性定理和模态合取范式存在定理。这些定理往往是经典逻辑相 应定理的本质推广。1
2、公理化系统 协调性 和谐性本节我们给出模态语言和模态公式，讨论它们的语形特 性，引入刻画模态的公理和推理规则，然后定义本书主要关注 的公理化系统，并定义相对模态系统的形式证明和推演概念。 最后我们证明这些系统是协调和和谐的。为了简洁，本书我们用=表示元语言意义上的“当且仅 当”，用=表示“若，则”，用表示“并非，用 表示“因为”，用.表示“所以”。1.1.1 定义（1）称L是（句子型的）模态语言=L由下列互不相同的 符号组成： 句符集：At=dfpi，P（，）;逻辑符：-1, 口，A;技术符：（，）o（2）递归定义ML是满足下列条件的最小集合： AtcML； A, BwMLnZ, DA, （4
3、人8）eML。-说明：（一）上述表示非空集At是可数的，即At或是 有穷的，或是可数无穷的。At中的元素称为句符。句符通常也 称为命题变元或句子变元或原子公式。通常也把ML称为模态语言，这似乎更符合我们对语言的 直观理解。和a称为联结符,（读作：非）直观上表示“否定”，A（读作：合取）直观上表示“并且”，它们通常称为真值联结 符或命题联结符。（读作：必然）称为模态符或（一元）模态算子。从上述定 义看，口也是一个一元联结符，只是在本书我们一般不把它解 释为真值联结符。本书我们用口指称要讨论的模态概念。这个概念通常理解 为某种“必然性”。实际上，人们在日常思维中有各种模态概 念，其直观语义多种多样
4、，但本书一般不讨论。本书主要研究 模态逻辑的技术部分，即使在语义方面也着重研究两种形式语 义。当然，不同的形式语义，特别是不同的公理化系统，刻画 了不同的模态符，而这些差异的后面实际上有不同的直观语义 （背景）。请有兴趣的读者参见相关的文献。（-）At的基数是有穷或可数无穷的。但事实上，本书的 绝大部分结果对任意基数的句符集皆成立。（三）对任意形如口/的公式，称4是口的辖域.（四）今后若不特别提到，我们总用元变元p, q, r.- （带或不带上下标）表示At中的公式，其中p, q, r分别特指 P” 02，P3；用元变元A, B, C, D, （希或不带上下标）表 示ML中的公式；用，,甲,0
5、,三，（带或不带上下标） 表示公式集，即ML的子集。（五）上述一提到的符号互不相同，通过得到 的ML中的句子具有唯一可读性，并且具有可枚举性。设语言 L是可数无穷的，即At是可数无穷的。.由L构成的ML中的 公式是有穷个符号构成的符号串，.据集合论的基本事实，可 数无穷集的所有有穷子集的个数仍是可数无穷的，.我们可以 枚举ML中的所有公式如下：A. A zl ,， o关于这方面的严格表述和证明，请读者参见Enderton的1972O(六)“T ”称为结束符。用在定义、引理、定理和推论 等后面。1.1.2 缩写定义(Dfv) (4v8)=df-1(-1B)(Df-) (AS)=dfi(Aaiff
6、),(Dfa-v4,(DfT) T=dfSv-jp),(Df_L) ,L =df -T o T说明：(一)上述定义前面的Dfv, Df7,分别是相应 定义的缩写。这在将来证明系统的内定理时是很方便的。(-)V (读作：析取)直观上理解为“或”，T (读作： 蕴涵)直观上理解为“若，贝IJ”，6(读作：等价)直观上 理解为“当且仅当”，(读作：可能)直观上理解为” 是可能的”。(三)也称为模态符或模态算子。以后口和都简称为模 态。1.1.3 约定(1)为了节省括号，本书我们约定公式最外面的括号可以 省略，且公式所含的联结符相对公式的结合力依次减弱：-1，,， A V,，(2)同类联结符满足右向结
7、合律例如，我们用小T -4表不：小)。(3)若。力0(0是空集符号)是有穷集，则我们用八。和 V0分别指称0的所有元素(据某个固定的排序方法)的合取和 析取。若。=Z,则八。=dfX， V0=df/t(4)若。=0,则八。=dfT, V0=df -L T说明：关于(4)的定义，直观解释如下：考虑八0=dfT。 我们知道，A。为真的充要条件是()若Ae。，则4真。而当。=0时，AeP不成立，；.()空洞成立。.我们把八0 定义为T。同理可解释V0=dfJ_。1.1.4 定义(1) A的子公式集Sub.)是最小集合使得Aw3;-.Be = BaCw+= B, CuP； UBeWn加巴(2)我们用S
8、ub(。)表示0的子公式集：Sub(0)=oSub(J)： Ae 0(3)称0在子公式下封闭Sub(0)=0=(4)若A是Y 或口8,则我们称B是4的实主子公式 (proper main subfbrmula)o这时称-i和口是A的主联结符。若4 是BaC,则我们称8和C是4的实主子公式。这时称a是A的 主联结符.实主子公式也称为真主子公式或简称主子公式。T1.1.5定义(1)称c是代入映射是从At到ML中的映射。任给公式A,称Zo是/的代入特例(substitution instance) o Zc如下递归定义： PnOoipn),对所有V。；(-尸-4郎)；(8aO=(8o)a(C(t)；
9、(口8)q/)(pq)pr,A(3) (rpTq)T(rpTF)p，(MP) A, AtB/B,(US) A/Aa,其中是任一代入映射。T说明：(一)MP称为分离规则，US称为代入规则“(二)以后我们把PC看作是最小的(空洞的)模态系统。在构造各种(非空洞的)模态系统之前，我们先来考虑下列 显表示(除了 RER)模态的公理和推理规则，它们在后面经常用 到：1.1.7定义(1)公理：(M) 口八夕)一(C) 口夕人夕一口防人4),(N) 口(K) 口。均)-一今(D)(T) 口pTp，(4)(B) /?-/?,(5) Op(G) 口/?，(McK) 口，(H) (pA p4) v (g 人 qT
10、p),(W)(Lem) ( p4)v ( qp),(Dum) ( (p- p)p) O /?po 推理规则(RN) A/OA,(RM) 48/口/一口8,(RE) /68/口/一口8,(RR) /U8tC/D/aD8tDC,(RK)小 a”7/口/仆aDZ”口.对所有co,(RER) AaB/CcC(AB)。-说明：(一)上述公理和规则左侧的大写字母串表示它的 名字(通常是英文名称的缩写)，其中推理规则前面都冠以Ro(二)当 =0 时，据 1.1.3(4), RK 是 T7/T.口儿 而 此规则本质上是RN.(三)下面我们对上述部分公理和规则作些简要的说明： K是为了纪念Kripke命名的一条
11、公理，但据R.A.Bull和 K.Segerberg 在其1984 (p.20)所说：“Kripke 似乎从来没有 关注过这条公理”。笔者认为K是模态逻辑的一条相当重要的 公理，用此纪念Kripke对模态逻辑做出的奠基性贡献也是恰当 的。D是deontic的缩写，T最早是由R.Feys提出和命名的。5也记作E,而后者是Euclidean的缩写。B是Brouwer的缩写，YT+B与直觉主义逻辑有关联。McK是McKinsey的缩写，也记作.1。G是Geach的缩写，也记作.2。Lem是Lemmon的缩写，也记作.3。H是Hintikka的缩写，Dum是Dummett的缩写。W是(anti-)we
12、lbrdered的缩写。文献中也记作G或GL,其中 L用来纪念M.H.L6b,他提出卜,面提到的系统KW。RN是Rule of Necessitation的缩写，称为必然化规则”RM是Rule of Monotonicity的缩写，称为单调规则”RE是Rule of Equivalence的缩写，称为（可证）等价规则或 全等规则（Rule of Congruence）.RR是Rule of Regular的缩写，称为正则规则。RK是Rule of Kripke的缩写，称为正规规则.RER是Rule of Equivalence Replacement的缩写，称为（可证） 等价置换规则。1.1.
13、8定义和约定令是公理集（本质上就是一集公式），R是推理规则集。（1）称s=是（一般意义上的）模态系统o s是如 下构成的系统：S的公理是PC的公理和八S的推理规则是MP, US和R。（2）这时称是S（相对PC）的特征公理的集合，R是S（相 对PC）的特征（推理）规则的集合。T说明：（一）为了方便，当或R为空集时，我们用S=或 S=来表示 S=或 S=注意：当和R皆为空集时，S=PC,（二）任给模态系统S=0令八是新公理集且R,是 新推理规则集。为了方便，我们也用S+Q + R表示RuRio令A是新公理，我们也用SA简单表示S+A。我们还用S-A, ST和SR分别表示从S中去掉公理 A和公理集厂
14、和规则集R得到的系统。下面的定义给出的模态系统是本书主要的研究对象。LL9定义E=df,M=df EM,R=df MC,K=df,D=dfKD,T=dfKT,B=dfTB,S4=dfT4,S5=dfT5,K4.3=df K4Lcm,S4.1=dfS4McK,S4.2=dfS4G,S4.3=S4Lem。-下面我们分别引入形式证明、内定理和推演概念：定义 令S是任意模态系统。(1)称公式序列小，4是S中的形式证明=对每 一 i使得下列条件至少有一成立： 4是S的公理的代入特例； 存在J,左，使得4是从4和4据MP得到的； 存在和力，使得4是从,， 4nl据S中的特征规则(模态规则)得到的。(2)称
15、在S中有形式证明=存在S中的形式证明 小，4使得4=，。(3)称4是S的内定理，记作-s4 Q 4在S中有形式 证明。我们用Th(S)表示S的所有内定理的集合。(4)若4任Th(S),则我们也记作公 /,并称/是S的非 内定理,(5)称力和8相对S等价 =is4一瓦T说明：(一)上述条件一也可以等价表示为：4是S的公理； 存在j, Yi使得4是从4和4据MP得到的； 存在机3和力，使得4是从4力， 4nl据s中的特征规则(模态规则)得到的； 存在使得4是从4据us得到的。(二)易见公理自身也是内定理。i.i.ii定义(1)称公式序列小，4是S中从。的推演O 对每一 IWiW,下列条件至少有一成
16、立：4是s的公理的代入特例；A 换句话说，存在S的公理A和代入映射。使得4=A(t。 存在),使得4是从4和4据MP得到的； 存在加存在S中从0的推演Ai，4使得A= A,这时也称小，4是S中从。到/的推演.为了方便，以后用。构成S的推理规则称为S的初始规则 例如，MP就是任何模态系统 的初始规则。表示：对每一/e巴。卜s4。我们也用Cns(0)表示/eML： 0 Hs J,且称Cns)是。 相对S的可证后承集。(3)若1任Cns)(即/没有S中从。的推演)，则我们也 记作(4)若。=小，A,则我们用小，4 % 4表 示。入儿 用小，4,表示。(5)称R=m，An/A是S的(强)推理规则，记作
17、Re Rule(S), 对所有代入映射 a, Aa, AffsA(r,称R是S的导出规则o ReRule(S)使得R不是构成S的 推理规则 o(6)称R=4，A,/A是S的弱推理规则，记作 ReWRule(S), 若 小，且 则(7)称小，An/A是S的虚规则0存在使 得S没有任何形如4的内定理。否则称小，4/4是s的实规则。T说明：（一）以后我们在不致混淆之处省略上面两个定义 中的下标S。（二）显然 Cns（0）=Th（S）。（三）称R是S的弱规则是因为R只能用于Th（S）的元素， 一般不能用于Cns（。）中的元素。例如，在上述定义中，代入规则只能用于公理（以后我们证 明代入规则只能用于S的
18、内定理），否则，例如，我们有p-r? 或p-_L,而这些推理都不是我们想要的。（四）（5）的意思是推理规则应该在模式的意义上理解的。严格来说，pi，p,卜sq不是S的推理规则，除非对所有 代入映射。，有如1）,，CT（p） HS这正是（5）要表达的意思。（五）以后我们用RPC表示Rule（PC）（中的元素）。（六）若Re（W）Rule（S）,则称S有R；否则称S没有R。（七）我们关注的规则除MP外都是单前提规则。对单前提规则，我们有A/B是S的虚规则o S没有任何形如A的内定理。 虚规则总是（空洞的）弱规则。为了方便，我们把模态系统分成几类：1.1.12 定义 令S是模态系统。（1）称S是全等
19、系统o S有规则REo（2）称S是单调系统o S有规则RM。（3）称S是正则系统o S有规则RRo（4）称S是正规系统 S有规则RK。(5)称E, M和R为初等系统，称K, D, T, B, S4和S5为基本系统。T1.1.13 定义 令S和团是两个模态系统。(1)称S是Si的子系统或S是S的扩充系统，记作 ScSp 0 Th(S)uTh(S。(2)称S是&的真子系统或&是S的真扩充系统， 记作 SuS|, o Th(S)uTh(Sj)。(3)称S和Si是等价系统，记作S = S, = TMS) = Th(S,)o T说明：要证明ScS),我们只须证S的公理和规则是Si的 内定理和(导出)规则
20、。1.1.14 定义 令S是模态系统。(1)称S协调 不存在A使得A和-iJ都是S的内定 理。(2)称S和谐o存在力使得/不是S的内定理。T我们先来证1.1.9定义的系统是协调和和谐的，为此我们先 给出一个定义：1.1.15 定义 任给A,递归定义A的PC-变形/一口如下： p,=p“，对每一 V(o； (8)w=田口； (5AO-n=S_nAC-n； (口8)-口=8一口。H：(-)“y就是删去工中口的每一出现得到的公式，其中若有当视为口。(二)一口实际上是一个从模态语言ML到经典句子语言的 翻译映射。1.1.16 定理 令S=是1.1.9定义的系统。(1) S协调。(2) S和谐。证明：(
21、1)逐个检查厂中公理，易见若4是中公理的代入特例，则-PC/T。逐个检查R中的规则，易见 若出，,B“/CeR,贝IJ8口，B/D/C-aGRPCo下证：)s / n卜pc4n 设is 4。则存在S中/的形式证明小，A”施归纳于 下证： ipc/j 口。若4是PC的公理的代入特例，则易得。若4是中公理的代入特例，则据易得。若4是从它前面的公式据MP得到的，则据归纳假设易得 。若4是从它前面的公式据R中的规则得到的，则据归纳假 设和易得。这样，我们证明了。旃面引入的公理只有w在删去其中的口后不是重言式。假设S不协调，则存在Z使得Is/且-S T1。据，有卜 pc 这种方法我们在谓词逻辑中也常用.
22、当然在那里我们删去的是量词。 1 pc - 矛盾于PC的协调性。(2)据(1)。T说明：(一)通常人们用两种方法证明S协调。第一种就 是上述方法删模态法：据上述，通过删去Th(S)中公 式的模态算子把S的协调性归约为PC的协调性。另一种方法 我们在以后给出。(二)后面我们还要引入另外一些系统，它们大部分都可以 用此方法证明其协调性和和谐性。练习1.11.1.17证明：(唯一分解定理)对每一 4eML,下列条件恰有一满足：(1) JeAt,(2)存在雎一的公式8eML和唯一的符号OeIf 口， 使得4 = 08,(3)存在雎一的公式序对g, OeMLXML和唯一的符号 Oga, v, t, 一使
23、得 4=BOC。提示：参见 Enderton 的1972。归纳原则)设(1) At的每一句符有性质(p；(2)若4有p,则F和口/有性质；(3)若/和8都有 hsA(7o T说明：此练习说明代入规则US可用于S的内定理。1.1.21 思考题 令舟是S的扩充系统。下列蕴涵关系是否 成立？Rg Rule(S) = Re Rule(S|) T1.1.22 令&是S的扩充系统使得S,和S有相同的初始推 理规则，且令证明：0%/ = W卜si 4。1.1.23 令 SuSi。(1)若S1协调，则S协调。(2)若&和谐，则S和谐。T2初等系统从本节起到本章末，我们分别考察一批重要的模态系统的 证明论性质。
24、从 2到 5我们分别考察初等系统、基本系统、退化系统 和其他重要系统，着重证明这些系统的内定理和导出规则以及 这些系统之间的相互关系。我们也证明其中的一些系统的元定 理，例如，等价置换定理、对偶公式定理、对偶符串定理、演 绎定理、归约定理、Post-完备性定理和模态合取范式存在定 理。这些定理往往是经典逻辑相应定理的本质推广.一、全等系统本节我们来考察全等系统的一些证明论性质。以后我们可 以看到，本书涉及的所有非空洞的都是全等系统，所以下面证 明的结果对所有非空洞模态系统都成立。我们先来证明这些系统的一些重要的内定理和导出规则， 它们在今后要不断用到。为了以后提述方便，在下面的定理 中,我们用
25、s(l),，S()来指称模态系统S的内定理和导出 规则。1.2.1定义任给 ,1 p oE(4) p p,-poE(5)对所有np.对所有ncoo(2) E=o证院1： (1)证 E(l)：假设i/l,，RPC-u4c口-18,，RE(4B,，RPCO/cOB。，DfO说明：（一）上面是一个推演的通常表述：这个推演可 看作是由3个竖列组成：第1个竖列是序号，它们 指称推演的步骤；第2个竖列是推演的本身；第3个竖列是推 演的根据（推演的出发点（假设）、公理、推理规则（包括导出规 则）、前面已证的内定理、形如Df那样的缩写定义）。例如， 上述第1行最右的“假设”表示推演的出发点，第2行最后的 “，
26、RPC”表示对提到的4cB运用RPC中的规则，。 以后我们也把此规则称为RER,虽然，严格地说，它相对E弱于 RERo为了简单，以后我们在第3个竖列不致混淆之处如下省略 序号：若一个公式直接从上一行公式推得，则在该行的根据中 不写序号。例如，上述第3竖列的，均可省略。注意：对一个推演来说，只有第2个竖列才是本质的。为了简洁，以后我们省略第二列中的标点符号。类似地，我们如上处理内定理的证明。(二)本书假定读者比较熟悉阶逻辑，特别是经典句子演 算的形式证明和推演，.本书以后我们经常只给出一个形式证 明或推演的关键部分，有时，写出的一步由几步缩写而成，想 必读者能自行补上跳跃的部分和根据。证E(2)
27、：在E中设n。要证-CC(A/B)o考虑置 换定义的5种情况：情况1 C就是特定的Z：则C(48)=B, .据设定和置 换定义，有C(48)。情况2 C=3 且特定的X在。中：据归纳假设，我们 有 FDD(AB),据 RPC,有 卜DcD(AB),据置换 定义，有情况3 C=Da且特定的/在。中：据归纳假设，我们 有-060(4 8),据 RPC,有 卜。aE(Z)(/8)aE, .据 置换定义，有F D八ESE)(A B)。情况4 C=Oa且特定的“在E中：据归纳假设，我们 有 FE0E(AB),据 RPC,有Oa(E(/8),二据置换定义，有卜。人Ec(U)(/5)。情况5 C=DD且特定
28、的“在。中：据归纳假设，我们 有DcD(AB)。据 RE,有 1口。6口(。(/18),二据置换定义，有 1 口()(/8)。证 E(3)：./?PC 从实用的角度，我们这里设可含v和.(2) 口 口 、pRER口/H-iO、pDfO证 E(4)： ip 口 、pPC-1口-、pDfO证E(5)：若=0,则显然。若=1,则据E(3)。设=% 时要证结果成立，下证=左+1时要证结果成立：口7-1-中归纳假设*+口-，RE+16-口-1二0RPC (或 RER)DfO证 E(6)：!pE(5), US fO JpCrCIJpRPC”,口口RER据 E(2),只须证 Eq, B|JW RE：AcB
29、假设 口2口5 RER说明：据(2),我们看到系统E实际上就是把PC的等价置 换规则运用到形如口工的公式，.全等系统(即E的扩充系统) 都有(相对所有公式的)等价置换定理。1.2.3对偶公式定义 设/中不含T和c。,称T是4的对偶公式0下列条件满足：(1) (P)d = -P,对每一 ”0口0”。T 说明：T可以直观地理解为：先加在A前，然后右移 越过口(或)时把口变成(或把变成口)，越过人(或V)时 把A变成V (或把V变成A),直到不能再内移为止(移到句符 前)。6.2.5 对偶公式定理 令S是全等系统。则卜sZ-证明：施归纳于Z的结构(这里设4含V和).情况1 A=pnP0一1-P，.据
30、对偶公式的定义，有 卜s PCP情况2则B-B。归纳假设此 eifidRPCiBcTrB)。对偶公式定乂情况3 A=BC贝IB-B”, CeC 归纳假设(2) BaCc-15dA-C41RPC(3) BACe/dvC*1)RPC8aCc( 8Aod对偶公式定义情况4 4=BvC。证明类似情况3。情况5 A = DB1,则归纳假设8c -18dRE口8-1-1口-1腔RPC口81bDfO口86-1（口8）6对偶公式定义情况6 A = OB.证明类似情况5。T说明：（一）对偶公式定理说明任何公式与它的对偶的否 定等价。（-）若我们把v和看作是缩写定义，则我们无需在上一 定理的证明中考虑情况4和情况
31、6,只须施归纳于A的实主子 公式，若Z自身不是句符。6.2.6 定义称一个符号串/是模态符串=/是由% ，口，中某些符号构成的有穷串，其中（|）表示空串。说明：（一）。与0不同，后者是空集的记号。（二）除了。以外的模态符串严格说就是一元逻辑符串。注 意：不是本质的。（三）据上述定义，下列都是模态符串：伞，口， O, 口，口。6.2.7 推论 下列是E的内定理或导出规则：E1/440E(8) Fc/。E(9) A/A(B/-d), A/AJBBd)。E(10) /一(屋)%E(ll) /4。E(12) F/。E(13) AtB/B&tALE(14)E(15) A/A, 其中4是若干次据F列原则从
32、4得到的 公式：若是4的子公式使得如含，则把夕中的右(或左) 移，在越过口(或)时把口(或)变成(或口)，在遇到时删 去成对的-m。证明：举例证明E( 10)：ri11对偶公式定理/c(F)d 对偶公式定义 Zc(T)dE(8), RER举例证明E(15)：据E(3)和E(4), US和PC的内定理，在 E中，有() 1-1口8-1B,卜一 BB,若干次运用RER,易从1得到X、注意：()中前两个等价式从左主子公式到右主子公式是 内移，从右主子公式到左主子公式是外移T说明：(一)以后我们把E(15)简记为LMC。(二)LMC的4个重要的特例是：/(-(口8 -18),LMC可以看作是RER的一
33、种特例。 据E(15)的证明，我们甚至还有6.2.8 定义 令夕是一个模态符串。(1)称/是正模态符串o夕中出现偶数次(包括0次)；(2)称/是负模态符串中出现奇数次：(3)称/是叠加模态符串Q夕中口或出现22次；(4)称夕是标准模态符串o,中不含或唯一的只出现 在夕中最前面。(5)称如是纯模态符串0如是不含的模态符串。T6.2.9 对偶符串定义 令如是一个模态符串。称，是/的对偶符串o 01是把夕中口和的每一出现 分别同时替换为和口得到的符串。T说明：上述定义的形式定义为：1.29定义任给模态符串夕，递归定义，如下：(1)(2)(- 尸=-)，,(3) (“=，(4) (O/)d=C/d T
34、1.2.10定理令夕和步是模态符串，令S是全等系统。则在s中:(1) 1 夕(2) 1-npCp。(3)卜加 o p,(4)(逆对偶定理)令 (A)手pTp, (Ad)科pT寸p。则-A 1 Ad。(5) S+A=S+Ado(6)(等价对偶定理)证明：证(1)：句?夕p)d/p-l，pd 如一-10dr?证：处父2(2) I /!，Ip-10-pCp 证(3)：据和(2)。(4) n :$pT善p-朔7-1%(3) #-2一一,/-1P，pp卜-1 /p -9。% 夕pc0P oisGpCp。对偶公式定理对偶公式定义，对偶符串定义对偶公式定义(1)US, RPCRERARPCUS (2)1我们
35、称Ad是A的逆对偶公式.，._，u ：据贤p一3pAd-1 d dpRpcI 夕1USP-0P(1)易得(5)和(6)。T说明：据(5),在全等系统中，用pTlJOp作为公理和用 口-口作为公理是等价的。1.2.11 定义 令S是任意模态系统。(1)令夕和步是两个模态符串。称小和/相对S等价=%如一期。(2)用Modal(S)表小S中两两不等价的模态符串的个数。 说明：在后面的1218,我们证明E有可数无穷多个两两 不等价的模态符串。1.2.12 推论(1)-,和相对E等价。(2)任意正模态符串相对E等价一纯模态符串。(3)任意模态符串相对E等价一标准模态符串。T二、单调系统1.2.13 定理
36、(1)下列是M的内定理或导出规则：M(l) RM,M(2) AtB/OAtOB (=RM。)，M(3)八夕)Op 八 Og,M(4) OpYOqTOipvq) (=Co),M(5) /? v (p vr) (=Fc),M(6) (OpT q)T (pTq)。)EcMo证明：(1)证M(l)：4TB假设RPC口/6口(4人8)RE口(Za5)tD4人口8M, US口力一口8，RPC证 M(2)：4TB假设BARPC15RM 口 A - 口 BRPCOAOBDfO据 M(2), PC 和 RPC,易得M(3)和M(4)o证M： 口一口丫夕)， 口夕一口丫夕) PC, RM (Jpv 口 qr 口
37、(pvq)RPC证 M(6)：(Op口4)(/口4PC(Op口夕)口-/口LMC(夕一口2口(/闻M(5)(Op口夕)一口仍一夕)RER(2)据 1.1.13,只须证 Th(E)qTh(M),而这显然。1.2.14对偶符串定理令S是单调系统，令，和步是两个正模态符串，且令(A) GpSp,(Ad)册厂断p,(RA)(正串单调规则)(RAd)(1) - A RAg Rule(S),(2) 4 s Ad o RAde Rule(S)o证明：“n” ：4TB假设aiBRM, RM。，假言易位规则(3)f4gAA,US，RPC“u” ：pipPCRA(Z)=：4TB假设r4rBRM,RM。，假言易位规
38、则步峭8Ad,US46b，RPCpipPC易见它是对RM和RM。的概括。严格证还是要施归纳于/的长度，/中有偶数个r。所以可以对偶 数个r做归纳。赞6P RAd T说明：本定理关于正模态符串的假设条件是本质的。因为 从pTq推不出-pTf1.2.15 推论 令S是单调系统。则S+A=S+Ad=S+RA=S+RAd。证明：据1.2.10(5)和上一定理。说明：据上述推论，在单调系统中，我们可以用公理，也 可以等价地用相应的规则。例如，M=E+M=E+RM。三、正则系统1.2.16 定理(1)下列是R的内定理或导出规则：r( 1) onn(=R),R(2) Ogv/cOpv夕(=Ro),R(3) (pvq)q ( = Mo),R(4) RR,R(5) K,R(6)小人aJ一4/口4仆人口 4T 口4R(7) AtBtC/QAtQBtQC ( = RRo),R(8) 口,人一(/?1),R(9) Q(p4)(口夕O)o(2) McRo(3) R=Dfn=dq =dq=, 其中下标“Df口”表示当前系统的初始模态符是,缩写定义是(DfO) 0/1=(if)A o