书眉模态逻辑讲义-中山大学逻辑与认知研究所

模态逻辑讲义（2006年）李小五编著中山大学逻辑与认知研究所第1章公理化系统在本章§1我们给出模态语言和模态公式，讨论它们的语形特性，引入刻画模态的公理和推理规则，然后定义本书主要关注的公理化系统，并定义相对模态系统的形式证明和推演概念。最后我们证明这些系统是协调和和谐的。从§2到§5我们分别介绍初等系统、基本系统、退化系统和其他重要系统，着重证明这些系统的内定理和导出规则以及这些系统之间的相互关系。我们也证明某些系统的元定理，例如，等价置换定理、对偶公式定理、对偶符串定理、演绎定理、归约定理、Post-完备性定理和模态合取范式存在定理。这些定理往往是经典逻辑相应定理的本质推广。§1公理化系统协调性和谐性本节我们给出模态语言和模态公式，讨论它们的语形特性，引入刻画模态的公理和推理规则，然后定义本书主要关注的公理化系统，并定义相对模态系统的形式证明和推演概念。最后我们证明这些系统是协调和和谐的。为了简洁，本书我们用=表示元语言意义上的“…当且仅当…”，用=表示“若…，则…”，用〜表示“并非"，用•••表示“因为…”，用...表示“所以…”。定义（1）称L是（句子型的）模态语言=L由下列互不相同的符号组成：句符集：At=df{pi，…，P"（，…）};②逻辑符：-1,口，A;③技术符：（，）o（2）递归定义ML是满足下列条件的最小集合：AtcML；A,BwMLnZ,DA,（4人8）eML。-\说明：（一）上述①表示非空集At是可数的，即At或是有穷的，或是可数无穷的。At中的元素称为句符。句符通常也称为命题变元或句子变元或原子公式。通常也把ML称为模态语言，这似乎更符合我们对语言的直观理解。「和a称为联结符,「（读作：非）直观上表示“否定”，A（读作：合取）直观上表示“并且”，它们通常称为真值联结符或命题联结符。□（读作：必然）称为模态符或（一元）模态算子。从上述定义看，口也是一个一元联结符，只是在本书我们一般不把它解释为真值联结符。本书我们用口指称要讨论的模态概念。这个概念通常理解为某种“必然性”。实际上，人们在日常思维中有各种模态概念，其直观语义多种多样，但本书一般不讨论。本书主要研究模态逻辑的技术部分，即使在语义方面也着重研究两种形式语义。当然，不同的形式语义，特别是不同的公理化系统，刻画了不同的模态符，而这些差异的后面实际上有不同的直观语义（背景）。请有兴趣的读者参见相关的文献。（-）At的基数是有穷或可数无穷的。但事实上，本书的绝大部分结果对任意基数的句符集皆成立。（三）对任意形如口/的公式，称4是口的辖域.（四）今后若不特别提到，我们总用元变元p,q,r.-（带或不带上下标）表示At中的公式，其中p,q,r分别特指P”02，P3；用元变元A,B,C,D,•••（希或不带上下标）表示ML中的公式；用「，①,甲,0,三，…（带或不带上下标）表示公式集，即ML的子集。（五）•••上述①一③提到的符号互不相同，，通过⑵得到的ML中的句子具有唯一可读性，并且具有可枚举性。设语言L是可数无穷的，即At是可数无穷的。•.•由L构成的ML中的公式是有穷个符号构成的符号串，.••据集合论的基本事实，可数无穷集的所有有穷子集的个数仍是可数无穷的，.•.我们可以枚举ML中的所有公式如下：A. •・・A・・・zl], ， ，o关于这方面的严格表述和证明，请读者参见Enderton的[1972]O(六)“T”称为结束符。用在定义、引理、定理和推论等后面。缩写定义(Dfv)(4v8)=df-1(-—1B)>(Df->)(A―>S)=df—i(Aa—iff),(Df<^)(46B)=df((4T8)A(8T/)),(DfO)OJ=df->a-v4,(DfT)T=dfSv-jp),(Df_L),L=df->ToT说明：(一)上述定义前面的Dfv,Df7,…分别是相应定义的缩写。这在将来证明系统的内定理时是很方便的。(-)V(读作：析取)直观上理解为“…或…”，T(读作：蕴涵)直观上理解为“若…，贝IJ…”，6(读作：等价)直观上理解为“…当且仅当…”，◊(读作：可能)直观上理解为”…是可能的”。(三)◊也称为模态符或模态算子。以后口和◊都简称为模态。约定(1)为了节省括号，本书我们约定公式最外面的括号可以省略，且公式所含的联结符相对公式的结合力依次减弱：-1， □, ◊，A»V, —>，<->»(2)同类联结符满足右向结合律例如，我们用小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时，Ae<P不成立，；.(☆)空洞成立。.•.我们把八0定义为T。同理可解释V0=dfJ_。定义A的子公式集Sub.)是最小集合》使得①Aw3;②-.Be¥=BaCw+={B,C}uP；UBeWn加巴(2)我们用Sub(。)表示0的子公式集：Sub(0)=o{Sub(J)：Ae0}»(3)称0在子公式下封闭<=>Sub(0)=0=(4)若A是Y或口8,则我们称B是4的实主子公式(propermainsubfbrmula)o这时称-i和口是A的主联结符。若4是BaC,则我们称8和C是4的实主子公式。这时称a是A的主联结符.实主子公式也称为真主子公式或简称主子公式。T1.1.5定义(1)称c是代入映射是从At到ML中的映射。任给公式A,称Zo是/的代入特例(substitutioninstance)oZc如下递归定义：①PnO—oipn),对所有"V。；'②(-^尸-4郎)；③(8aO=(8o)a(C(t)；④(口8)<7=口(80)。给定A,我们IT；用4(Pn/B)表不Ao使得a(p„)=Bo(2)称48〃0是用C置换/中某个指定的子公式8得到的公式o4(8〃。如下递归定义：①若/是指定的a则4B〃C)=C；②若4=3且指定的8在。中②，贝IJA(B//G)=^(D(B//Q)；③若4=。人£且指定的8在。中，则A(B〃C)=(D(B〃C))八E；④若4=Z)aE且指定的8在E中，贝U/(8〃0=Oa(E(8〃0)；⑤若/=口。且指定的8在。中，则

48〃0=口(。(8〃0)。~\说明：直观上说，代入式Z(p“/8)表示用8代入Z中的句符pn的所有出现得到的公式，而置换式4(8〃。表示用C置换A中子公式B的一个特定出现得到的公式。1.1.6定义我们用PC表示由下列公理和推理规则构成的系统：A(l)pTqTp,①①是全体自然数的集合，〃〈①即〃《①。②即不是情况①。A(2)(p->q—>/")―»(p―>q)―>p—>r,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，(B)/?->□<>/?,Op—◊口/?—>□◊〃，(McK)□◊〃—>◊口「，□(pA□p—>4)v□(g人□qTp),(W)(Lem)□(□p—>4)v□(□q—p),(Dum)□(□(p-»□p)—>p)—>O□/?—>po⑵推理规则(RN)A/OA,(RM)4—8/口/一口8,(RE)/68/口/一口8,(RR)/U8tC/D/aD8tDC,(RK)小a…"”7//口/仆…aDZ”—>口.对所有"<co,(RER)AaB/CcC(A〃B)。-\说明：(一)上述公理和规则左侧的大写字母串表示它的名字(通常是英文名称的缩写)，其中推理规则前面都冠以Ro(二)当«=0时，据1.1.3(4),RK是T7//T.口儿而此规则本质上是RN.(三)下面我们对上述部分公理和规则作些简要的说明：K是为了纪念Kripke命名的一条公理，但据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-)welbrdered的缩写。文献中也记作G或GL,其中L用来纪念M.H.L6b,他提出卜,面提到的系统KW。RN是RuleofNecessitation的缩写，称为必然化规则”RM是RuleofMonotonicity的缩写，称为单调规则”RE是RuleofEquivalence的缩写，称为（可证）等价规则或全等规则（RuleofCongruence）..RR是RuleofRegular的缩写，称为正则规则。RK是RuleofKripke的缩写，称为正规规则.RER是RuleofEquivalenceReplacement的缩写，称为（可证）等价置换规则。1.1.8定义和约定令「是公理集（本质上就是一集公式），R是推理规则集。®（1）称s=<r；r>是（一般意义上的）模态系统os是如下构成的系统：①S的公理是PC的公理和八②S的推理规则是MP,US和R。（2）这时称「是S（相对PC）的特征公理的集合，R是S（相对PC）的特征（推理）规则的集合。T说明：（一）为了方便，当「或R为空集时，我们用S=<??>或S=</>来表示S=<0；R>或S=<T；0>«注意：当「和R皆为空集时，S=<0；0>=PC,（二）任给模态系统S=<r；R>0令八是新公理集且R,是新推理规则集。为了方便，我们也用S+Q+R表示RuRi>o令A是新公理，我们也用SA简单表示S+A。我们还用S-A,S—T和S—R分别表示从S中去掉公理A和公理集厂和规则集R得到的系统。下面的定义给出的模态系统是本书主要的研究对象。LL9定义E=df<RE>,M=dfEM,R=dfMC,K=df<K；RN>,D=dfKD,T=dfKT,B=dfTB,S4=dfT4,S5=dfT5,K4.3=dfK4Lcm,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)称］在S中有形式证明=存在S中的形式证明小，…，4使得4=，。(3)称4是S的内定理，记作-s4Q4在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",下列条件至少有一成立：①4是s的公理的代入特例；②A"》换句话说，存在S的公理A和代入映射。使得4=A(t。存在), 使得4是从4和4据MP得到的；存在加<0和力，…，/“Si使得4•是从当,…，/友据S中的特征规则得到的。(2)称4在S中有从©的推演或称/在S中从0推出，记作0HsA,u>存在S中从0的推演Ai，4使得A„=A,这时也称小，…，4是S中从。到/的推演.为了方便，以后用。构成S的推理规则称为S的初始规则例如，MP就是任何模态系统的初始规则。构成S的推理规则称为S的初始规则例如，MP就是任何模态系统的初始规则。我们也用Cns(0)表示{/eML：0HsJ},且称Cns@)是。相对S的可证后承集。(3)若1任Cns@)(即/没有S中从。的推演)，则我们也记作(4)若。={小，…，A,,},则我们用小，…，4%4表示。入儿用小，…，4,表示。(5)称R=m，…，An/A是S的(强)推理规则，记作ReRule(S),<=>对所有代入映射a,A\a,A„ff^sA(r<,称R是S的导出规则oReRule(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的内定理），否则，例如，我们有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的虚规则oS没有任何形如A的内定理。虚规则总是（空洞的）弱规则。为了方便，我们把模态系统分成几类：定义令S是模态系统。（1）称S是全等系统oS有规则REo（2）称S是单调系统oS有规则RM。（3）称S是正则系统oS有规则RRo（4）称S是正规系统<=>S有规则RK。(5)称E,M和R为初等系统，称K,D,T,B,S4和S5为基本系统。T定义令S和团是两个模态系统。(1)称S是Si的子系统或S］是S的扩充系统，记作ScSp0Th(S)uTh(S。。(2)称S是&的真子系统或&是S的真扩充系统，记作SuS|,oTh(S)uTh(Sj)。(3)称S和Si是等价系统，记作S=S,,=TMS)=Th(S,)oT说明：要证明ScS),我们只须证S的公理和规则是Si的内定理和(导出)规则。定义令S是模态系统。(1)称S协调<=>不存在A使得A和-iJ都是S的内定理。(2)称S和谐o存在力使得/不是S的内定理。T我们先来证1.1.9定义的系统是协调和和谐的，为此我们先给出一个定义：定义任给A,递归定义A的PC-变形/一口如下：p,「'=p“，对每一〃V(o；(「8)w=田口；(5AO-n=S_nAC-n；(口8)-口=8一口。H：(-)“y就是删去工中口的每一出现得到的公式，其中若有◊当视为「口「。(二)一口实际上是一个从模态语言ML到经典句子语言的翻译映射。定理令S=<F：R>是1.1.9定义的系统。S协调。S和谐。证明：(1)逐个检查厂中公理，易见①若4是「中公理的代入特例，则-PC/T□。①逐个检查R中的规则，易见②若出，…,B“/CeR,贝IJ8「口，…，B/D/C-aGRPCo下证：③)—s/n卜pc4n°设is4。则存在S中/的形式证明小，…，A”施归纳于下证：④ipc/j口。若4是PC的公理的代入特例，则易得④。若4是「中公理的代入特例，则据①易得④。若4是从它前面的公式据MP得到的，则据归纳假设易得④。若4是从它前面的公式据R中的规则得到的，则据归纳假设和②易得④。这样，我们证明了③。旃面引入的公理只有w在删去其中的口后不是重言式。假设S不协调，则存在Z使得Is/且-ST1。据③，有卜pc"这种方法我们在谓词逻辑中也常用.当然在那里我们删去的是量词。> 1pc-这种方法我们在谓词逻辑中也常用.当然在那里我们删去的是量词。矛盾于PC的协调性。(2)据(1)。T说明：(一)通常人们用两种方法证明S协调。第一种就是上述方法^——删模态法®：据上述③，通过删去Th(S)中公式的模态算子把S的协调性归约为PC的协调性。另一种方法我们在以后给出。(二)后面我们还要引入另外一些系统，它们大部分都可以用此方法证明其协调性和和谐性。练习7证明：(唯一分解定理)对每一4eML,下列条件恰有一满足：(1)JeAt,(2)存在雎一的公式8eML和唯一的符号OeIf口，◊｝使得4=08,(3)存在雎一的公式序对<g,OeMLXML和唯一的符号Og｛a,v,t,一｝使得4=BOC。［提示：参见Enderton的［1972］。］归纳原则)设At的每一句符有性质(p；(2)若4有<p,则F和口/有性质§；(3)若/和8都有<p,则有性质(p。证明：ML中每一公式有性质Q。［提示：参见Enderton的［1972］。］任给公式4。证明力的代入特例的代入特例也是A的代入特例。T令S是任意模态系统。证明S有弱规则US：对任意代入映射%“=>hsA(7oT说明：此练习说明代入规则US可用于S的内定理。思考题令舟是S的扩充系统。下列蕴涵关系是否成立？RgRule(S)=>ReRule(S|)«T令&是S的扩充系统使得S,和S有相同的初始推理规则，且令证明：0%/=W卜si4。~\令SuSi。(1)若S1协调，则S协调。(2)若&和谐，则S和谐。T§2初等系统从本节起到本章末，我们分别考察一批重要的模态系统的证明论性质。从§2到§5我们分别考察初等系统、基本系统、退化系统和其他重要系统，着重证明这些系统的内定理和导出规则以及这些系统之间的相互关系。我们也证明其中的一些系统的元定理，例如，等价置换定理、对偶公式定理、对偶符串定理、演绎定理、归约定理、Post-完备性定理和模态合取范式存在定理。这些定理往往是经典逻辑相应定理的本质推广.一、全等系统本节我们来考察全等系统的一些证明论性质。以后我们可以看到，本书涉及的所有非空洞的都是全等系统，所以下面证明的结果对所有非空洞模态系统都成立。我们先来证明这些系统的一些重要的内定理和导出规则，它们在今后要不断用到。为了以后提述方便，在下面的定理中,我们用s(l),…，S(〃)来指称模态系统S的内定理和导出规则。1.2.1定义任给"<0。(1)归纳定义口”/如下：口，=/1,•••,口"+)=口口7。(2)归纳定义如下：◊，=4,•••,On+'A=OOnA.说明：□7和分别表示4前面有〃个口和1.2.2定理（1）下列是E的内定理和导出规则:E(l)AcB/OAcOB(=REo)oE(2)RER,从而我们有4c8,C/C(A〃B)qE(3)□>—।◊―,―1□ >◊—\poE(4)◊p<—>—।□―\p,—-poE(5)对所有n<（oQE(6)>p.对所有n<coo(2)E=<RER>o证院①1：(1)证E(l)：假设②—i/l ,①，RPC③□-u4c口-18,②，RE④―(□—4《>—»□―\B,③，RPC⑤O/cOB。④，DfO［说明：（一）上面是一个推演的通常表述：这个推演可看作是由3个竖列组成：第1个竖列是序号①，②，…，它们指称推演的步骤；第2个竖列是推演的本身；第3个竖列是推演的根据（推演的出发点（假设）、公理、推理规则（包括导出规则）、前面已证的内定理、形如Df◊那样的缩写定义）。例如，上述第1行最右的“假设”表示推演的出发点，第2行最后的“①，RPC”表示对①提到的4cB运用RPC中的规则，……。®以后我们也把此规则称为RER,虽然，严格地说，它相对E弱于RERo为了简单，以后我们在第3个竖列不致混淆之处如下省略序号：若一个公式直接从上一行公式推得，则在该行的根据中不写序号。例如，上述第3竖列的①，②，③，④均可省略。注意：对一个推演来说，只有第2个竖列才是本质的。为了简洁，以后我们省略第二列中的标点符号。类似地，我们如上处理内定理的证明。(二)本书假定读者比较熟悉•阶逻辑，特别是经典句子演算的形式证明和推演，.•.本书以后我们经常只给出一个形式证明或推演的关键部分，有时，写出的一步由几步缩写而成，想必读者能自行补上跳跃的部分和根据。］证E(2)：在E中设n。要证^-C<->C(A//B)o考虑置换定义的5种情况：情况1C就是特定的Z：则C(4〃8)=B,...据设定和置换定义，有C(4〃8)。情况2C=3且特定的X在。中：据归纳假设，我们有FD—D(A〃B),据RPC,有卜「Dc^D(A〃B),据置换定义，有情况3C=Da£且特定的/在。中：据归纳假设，我们有-060(4〃8),据RPC,有卜。aE—(Z)(/〃8))aE,...据置换定义，有FD八ESE)(A〃B)。情况4C=Oa£且特定的“在E中：据归纳假设，我们有FE0E(A〃B),据RPC,有 Oa(E(/〃8)),二据置换定义，有卜。人Ec(£U£)(/〃5)。情况5C=DD且特定的“在。中：据归纳假设，我们有・DcD(A〃B)。据RE,有1口。6口(。(/1〃8)),二据置换定义，有1口£>—(□£>)(/〃8)。证E(3)：TOC\o"1-5"\h\z①.□/? PC®从实用的角度，我们这里设《可含v®从实用的角度，我们这里设《可含v和◊.口>—।—।口—।—、p RER③口/H->-iO~、p DfO证E(4)：―।□—ip<—>―।口—、p PC②>-1口-、p DfO证E(5)：若〃=0,则显然。若"=1,则据E(3)。设〃=%时要证结果成立，下证"=左+1时要证结果成立：①口7"-1<>"-中 归纳假设②□*+》—口->◊， RE③ □"+16->~>口-1<>二0 RPC(或RER)④DfO证E(6)：①—!◊"—।——\p E(5),USfOJpCrCIJp RPC③◊”—।——,口"—<p RPC④◊>>>口" RER⑵据E(2),只须证Eq<RER>,B|J<RER>WRE：①AcB假设口2口5RER说明：据(2),我们看到系统E实际上就是把PC的等价置换规则运用到形如口工的公式，.•.全等系统(即E的扩充系统)都有(相对所有公式的)等价置换定理。1.2.3对偶公式定义设/中不含T和c。,称T是4的对偶公式0下列条件满足：(P")d=->P",对每一”<3;(18)d=此4(5AC)d=5dvCd;(5v0d=5dACd；(□S)d=O5d；(O5)d=n5do说明：据上面的定义，我们称A与V互为对偶，称口与◊互为对偶上述定义的(4)和(6)不是本质的，增加它们只是为了简洁。例如，若不用(4),则(SvOd=(-1(^BA-,Q)d=-1(-i5dv—iCd).. 据⑵和(3)而在PC中，从而在E中，有内定理T-18dV-1cdK^dAC*1。例令J=O-.DOnp,则Ad是□->0口0”。T说明：T可以直观地理解为：先加「在A前，然后右移越过口(或◊)时把口变成◊(或把◊变成口)，越过人(或V)时把A变成V(或把V变成A),直到不能再内移为止(「移到句符前)。对偶公式定理令S是全等系统。则卜sZ-证明：施归纳于Z的结构(这里设4含V和◊).情况1A=pn« P0一~1->P"，••.据对偶公式的定义，有卜sP"C—<P・°情况2 则①B-B。 归纳假设②此eifid RPC③—iBcTrB)。 对偶公式定乂情况3A=BC贝I]①B-B”,CeC」归纳假设BaCc-15dA-■C41 RPCBACe/dvC*1) RPC④8aCc「(8Aod 对偶公式定义情况44=BvC。证明类似情况3。情况5A=DB1,则①归纳假设②□8c□-18dRE③口8--1-1口-1腔RPC④口8<->—1◊b"DfO⑤口86-1（口8）6对偶公式定义情况6A=OB.证明类似情况5。T说明：（一）对偶公式定理说明任何公式与它的对偶的否定等价。（-）若我们把v和◊看作是缩写定义，则我们无需在上一定理的证明中考虑情况4和情况6,只须施归纳于A的实主子公式，若Z自身不是句符。定义称一个符号串/是模态符串=/是由｛%「，口，◊｝中某些符号构成的有穷串，其中（|）表示空串。~\说明：（一）。与0不同，后者是空集的记号。（二）除了。以外的模态符串严格说就是一元逻辑符串。注意：◊不是本质的。（三）据上述定义，下列都是模态符串：伞，口，伞，口，O,口◊「， ◊□「口◊。推论下列是E的内定理或导出规则：E⑺ ~1/440E(8)Fc/。E(9)A/A(B//-£d),A/AJB〃Bd)。E(10)/一(屋)%E(ll)//4。E(12)F//。E(13)AtB/B&tALE(14)E(15)A/A',其中4是若干次据F列原则从4得到的公式：若是4的子公式使得如含「，则把夕中的「右(或左)移，在越过口(或◊)时把口(或◊)变成◊(或口)，在遇到「时删去成对的-m。证明：举例证明E(10)：①ri11 对偶公式定理②/c(F)d对偶公式定义③Zc(T)d E(8),RER举例证明E(15)：据E(3)和E(4),US和PC的内定理，在E中，有(☆)1--1口8㈠◊-1B, 卜一B—B,若干次运用RER,易从1得到X、注意：(☆)中前两个等价式从左主子公式到右主子公式是内移「，从右主子公式到左主子公式是外移T说明：(一)以后我们把E(15)简记为LMC。(二)LMC的4个重要的特例是：①②③④///(-(口8〃◊-18),①②③④LMC可以看作是RER的一种特例。据E(15)的证明，我们甚至还有定义令夕是一个模态符串。(1)称/是正模态符串o夕中「出现偶数次(包括0次)；(2)称/是负模态符串中「出现奇数次：(3)称/是叠加模态符串Q夕中口或◊出现〃22次；(4)称夕是标准模态符串o,中不含「或唯一的「只出现在夕中最前面。(5)称如是纯模态符串0如是不含「的模态符串。T对偶符串定义令如是一个模态符串。称，是/的对偶符串o01是把夕中口和◊的每一出现分别同时替换为◊和口得到的符串。T说明：上述定义的形式定义为：1.29定义任给模态符串夕，递归定义，如下：(1)(2)(->—尸=-)，,(□“=◊，，(O/)d=C/d»T1.2.10定理令夕和步是模态符串，令S是全等系统。则在s中:1夕1-^-npCp。(3)卜加o—p,(4)(逆对偶定理)令(A)手pT@p,(Ad)科pT寸p。则-A<=>1Ad。(5)S+A=S+Ado(6)(等价对偶定理)证明：证(1)：①句?夕p)d②/p<->-l，pd③如一-10dr?证⑵：①处—「父2(2)―I/—!，<->―I―\p③-10-《pCp证(3)：据⑴和(2)。(4)n:①$pT善p②->朔7-1%(3)―>#->2一一,/-1P④，p"p卜-1/—>p<=>-9％。%夕pc0PoisGpCp。对偶公式定理对■偶公式定义，对偶符串定义对偶公式定义(1)US,RPCRERARPCUS(2)1我们称Ad是A的逆对偶公式.，，._，，u：①②③④据TOC\o"1-5"\h\z贤p一3p Ad①②③④据-1ddp—》 Rpc—I夕1 US©P-0P (1))易得(5)和(6)。T说明：据(5),在全等系统中，用◊pTlJOp作为公理和用◊口〃-»口「作为公理是等价的。定义令S是任意模态系统。(1)令夕和步是两个模态符串。称小和/相对S等价=%如一期。(2)用Modal(S)表小S中两两不等价的模态符串的个数。~\说明：在后面的1218,我们证明E有可数无穷多个两两不等价的模态符串。推论(1)]◊-,□和□□相对E等价。(2)任意正模态符串相对E等价一纯模态符串。(3)任意模态符串相对E等价一标准模态符串。T二、单调系统定理(1)下列是M的内定理或导出规则：M(l)RM,M(2)AtB/OAtOB(=RM。)，M(3) 八夕)—》Op八Og,M(4)OpYOqTOipvq)(=Co),M(5)□/?v□ □(pv^r)(=Fc),M(6)(OpT□q)T□(pTq)。)EcMo证明：(1)证M(l)：4TB假设RPC口/6口(4人8)RE口(Za5)tD4人口8 M,US口力一口8③，④，RPC证M(2)：4TB假设—\B—>—\ARPC□—15—>□—RM—।口—\A->—।口—\BRPCOA^OBDfO据M(2),PC和RPC,易得M(3)和M(4)o证M⑸：①口「一口⑦丫夕)，口夕一口⑦丫夕)PC,RM②(Jpv口qr口(pvq) RPC证M(6)：TOC\o"1-5"\h\z① (Op—＞口4)—＞—(◊「\/口4 PC②(Op—＞口夕)—＞口-^/口］ LMC③(◊夕一口2口(/闻 M(5)④ (Op—»口夕)一》口仍一＞夕) RER(2)据1.1.13,只须证Th(E)qTh(M),而这显然。~\1.2.14对偶符串定理令S是单调系统，令，和步是两个正模态符串，且令(A)Gp—Sp,(Ad)册厂断p,(RA) (正串单调规则)①(RAd)-A—RAgRule(S),4sAdoRAdeRule(S)o证明：⑴“n”：①4TB 假设②aiB RM,RM。，假言易位规则②TOC\o"1-5"\h\z(3)f4gA A, US④ ③，②，RPC“u”：① pip PC② RA(Z)=> ：①4TB 假设② r4rB RM, RM。，假言易位规则③步峭》8 Ad, US④「46b ②，③，RPC① pip PC®易见它是对RM和RM。的概括。®严格证还是要施归纳于/的长度，•••/中有偶数个r。所以可以对偶数个r做归纳。②赞…6PRAdT说明：本定理关于正模态符串的假设条件是本质的。因为从pTq推不出-pTf»推论令S是单调系统。则S+A=S+Ad=S+RA=S+RAd。证明：据1.2.10(5)和上一定理。~\说明：据上述推论，在单调系统中，我们可以用公理，也可以等价地用相应的规则。例如，M=E+M=E+RM。三、正则系统定理(1)下列是R的内定理或导出规则：r(1)o>nn(=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(p—>4)<->(口夕—>O^)oMcRoR=<RR>=<RRo>Dfn=<Mo；RM>>dq=<Co»Mo；REo>dq=<K:RM>,其中下标“Df口”表示当前系统的初始模态符是◊,缩写定义是(DfO)0/1=(if―)◊—\Ao证明：(1)据C和M,显然有R(l)。证R(2)：(D□(-\p/\-11)<—>口-i.aD—】q(2)□―>□―ipA□-、q(§)—।LU―i(pv(y)<->—)□―p\z―)□―11④OSvq)-OpvOg证R(4)：A八BtC口(4/\5)一口。③口/人口8一口(4八8)④DJaCB—>CC证R(5)：①(pTq)八pTq口仍一>4)人口/?一□[口⑦7l)—>□〃一>□夕证R(6)：①小人…aJ〃一>/假设RMC,US③，②,PCRRRPC②□小人口(42八…八4)一>□/③口小人…人□/〃一>□/证R(7)：①4tBvC(2)―iB八-iC-»-\A(§)O—«5aEZI-\C—>□—\A④OAtOByOC证R(8)：(J)EJ(p—》~»夕)一^口夕一^口-、q② □「(pAq)—>□〃一>□-1[R,USRERRPCDfORPC假设RRR,RERXw-2假设RPCRRRPC,DfOK,USRER-1◊(p八q)―>□p―>-1◊q(pM)R(9)：O(r2vq)c◊-ipvOq◊(—>―iLZIpvO^◊(P一夕)c(□pi◊1)LMCRPCRo,LMCRER举例循环证<RR>=<RR)>dq=<Mo；RMo>d「°假设RPCRRoRPCDf口先证假设RPCRRoRPCDf口①A八BtC②-iC—>—l4v-«5③◊「CtOYvOR—>◊—i/i八一)◊—18—>--iCRM>>Dfo：假设RMoMo,RPC(§)□/IaEiib―RM>>Dfo：假设RMoMo,RPC4tBvCOZtO/v。OAtOBvOC□—i/?a□—10—»□—i(pvq)PC,②—>□—«(pv^)—>—।□-ipv-i□—iq RPC③◊(pvq)->OpvOg DfO再证RMo：①4TB 假设②—(5a-\B—>―\A RPC③□—△□一♦□F RR④「口力—」口」8 RPC⑤ OAtOB DfO其余未证的均留给读者作为练习。T最后证vMo；RMo>DfaC<RR>：先证Mo:RR说明：(一)R(6)中的限制条件是本质的，不能改成〃20,也就是说，R(6)WRK。(―)<RR>和<RR°>dg可以称为(两两)对偶系统”后面我们可以看到这样的时偶系统有很多。1.2.17定理(Chellas,[1980](p.243))令S=E+0使得0g{M,C,N}o则S有下列弱规则(参见1.1.11(6))：OA/A,OA/A,口4—口8/4-»8,OAtOB/AtB,口4—口8/468,OA-OB/A-B。证明：先定义从ML到ML中的一步删模态映射6如下：即")=P"对每一“<3,⑷，5(Ja5)=5(J)a5(5),5(口4)=儿易证：8(AOB)=8(A)O8(B),其中Oe{v,t,c}[注意：(一)6(4)和1.1.15定义的《一口不同。例如，易见6(口。—>□□/?)是0-»口/?,而(□/7—□□「)一''是(—.)8(Oy4)=3(-1口-l4)=—।—iAo]先证在S中有下列弱规则：①r=>a8(j)o设卜4则存在S中4的形式证明小，…，An=Ao施归纳我们要证：②卜6(4)，对所有1<运〃。情况14是S的公理的代入特例：只须考虑模态公理。若4=C］(8aC)tDBaDC是公理M的代入特例，则N4)=BaCt8aC。...它是PC的内定理。若4=D8aEICtD(Ba。是公理C的代入特例，则3(4)=3aCt8/\C。，它是PC的内定理。若4=口丁是公理N,则易见B(4)=T是PC的内定理。［本情况我们实际证明了一个更强的结果：ipcM4)。］情况24是据MP从前面某个4和4T4得到：据归纳假设，我们有受⑷，卜5(474)。而后者是13(4)T3(4)，•••据MP,有13(4)。情况3A,是据RE从刖j面某个Aj=B^->C得到：小，…，4中每一项都是内定理，③HAj,,'：5(/4,)=5(□ □Q=B^C=AP.I据③，F(4)。［注意：本情况无需归纳假设。］这样我们证明了②,从而证明3(小)，…，—=6(4)是3(/)在S中的形式证明，，①成立。据①易证(1)—(6)oT说明：(一)我们在上一证明中主要采用一种有别于1.1.15的方法的删模态法。后面我们还会介绍其他同类的方法。(二)在后面的6.1.27,我们要求读者证明系统E,M和R没有形如的内定理，.,•口4/4也是这3个系统的虚规则。下面我们考察上述系统的不等价模态符串的个数。1.2.18定理令S=E+G使得。u{M,C,N}。则S有可数无穷多个两两不等价的模态符串。证明：定义从ML到ML中的另一种删模态映射t如下：T(P")=P”对每一n<a>,x(―\A)=-*iT(/4),t(Aa8)=t(J)at(5),t(D/1)=To如上一定理的证明易证(那里的情况3在此更简单)，在S中，有①HJ=>HT(J)o任给IWmVto,则工(pdZTp)=pcT。下证：②FpcETp。假设要证结果不成立，则...据①，我们有ip—T,ip,...对任意/,据US,有；.S不协调，矛盾。据②和1.2.17(5),我们有③-对所有n<(Oo据③，易见要证结果。也即我们有：Modal(S)=K0oT说明：据上述定理，初等系统有可数无穷多个两两不等价的模态符串。练习1.2证明E=<REo>DfOoT证明：M=<RM>=<RMo>nf-ioTx)zxuz)1234z(xzl\z(xz(x证明下列是M的内定理或导出规则：x)zxuz)1234z(xzl\z(xz(x□。、…丫口外一口伽丫…师)；AtB/$At©B, 其中/是正模态符串。(II)口4—5/口/一口8是M4的导出规则。T1.2.22(I)证明下列是R的内定理或导出规则：□ □(［一>〃)一>□(p—>r),□(pTq)八O(pz)T◊(g八厂)，O(pTqz)T(5T<>q)八(UpTOr),□(p-»^)-^Op-»O^,□(pTq)人□pT◊(［一>尸)一>◊(pAr),OT«-»(Dp-»Op),□(p—q)T(□p<->□q),D(pv^)—>OpvD^,□(piV-vpn+|)-»Op1v-vOpnvCprt+1,口⑦】人…A/?〃)cDp］A…人口为， 其中□p|A-ACprtAOpzl+1-»O(p|A-Apn+I),口口夕八O(q八人…人◊,〃)T◊(qa◊(qiap)a…a◊(q〃Ap)),At&v…v8“/OMT<>m8N…vO"B“，其中m<(o且AtBiv…vBa/OAiOBw…vOB“,其中1<"<3。(II)证明1.2.16(3)中未证部分。(III)证明R+Q(pTp)=R+D。(IV)(R4的演绎定理)0o{□J}•-K45=>0I-R4口/—»瓦T下面和后面我们在有一定难度的练习的序号上标以*:*证明口◊口◊「一口◊/?是R4的内定理。T说明：据上述练习，易见□◊口◊和□◊相对R4等价。§3基本系统本节我们来研究基本系统K,D,T,B,S4,S5,它们是6个最常见的正规系统，也是本书重点要研究的系统。定理(1)下列是K的内定理和导出规则：\!/V),\—/\!/\71\!/V),\—/\!/\7123456FZIVZIV/IXzl\/|\<<<<<<FKK-K-KKRM,RE,(从而)RER,□(pvg)—>Upv◊g,□/?a□q—>□(p^q)(=C),n(pA^)<—>oocj(=r)oKoK=<N,R；RE>=<C,K(l)；RM>=<N；RR>=<RK>oK=EMCN=MCN=RN。证明：(1)证K(l)：据RN显然。证K(2)：①A-^B 假设②□(28) RN③4T口5K, US④□力一口8 ②，③，MP证K(3)：据K(2),有RE。再如1.2.2的E(2)的证明，易得RERo

K(4)：□(fTp)TK,US□(-—>p)—>—।□―14V□pRPC□(pvq)TIZIpv◊1K(5)：RER,DfOp—q—p八qPC□pT□(qTpDRM□(qTp/\q)T□q-□(p/\q)K,US□/?aDqT□(pm)②，(3),RPC证K(6)：□(p八q)T□/7, □(p八夕)一>□qPC,RM□ Dp/\dqRPC,3；□(p八4)<~»口夕人口g②，K(5)⑵显然。(3)我们来循环证明。先证Kq<N,R；RE>：证RN：①A 假设②Tc4 RPC③□Tc口力 RE④□J (3),N,RPC据1.2.13的M(l)的证明，从M(R的一半)和RE得RM。下证K：①□((pTg)Ap)Tdg PC,RM② 口伊—>^)a□p—>□[ R③□(p-g)—>口°—>口9 RPC下证<N,R；RE>c<C,K(l)；RM>：据RM有RE。而据K(l)和RM易得No据RM易得M(见K(6)的证明)，再据C易得R。下证<C,K(l)；RM>c<N；RR>：证RM：①4TB 假设② AftB RPC口人口/一口8RR④ 口4一口8 RPC据N和RM易得K(l)»而据RR易得C«下证<N；RR>c<RK>：易见RR是RK(当"=2时)的特例。下证N：TtTPCTtDTRK("=0时)口丁RPC证<RK>UK：施归纳于〃。当”=01tRK就是TtZ/TtDH/.①Tf4T设②ARPC③□JRN④丁一口4RPC当"=1时，RK就是RM(=K(2))。归纳假设”=上时要证结果成立。则①4A+1—>8 假设②A।a*** ->B RPC③口工口…>8)归纳假设口/仆…K,RPC⑤口小a…aD/*+i->D8 RPC(4)据(3)显然。细节请读者补充。T说明：据(3),有RK的系统就有K和RN,所以正规系统总是K的扩充系统。1.3.2定理下列是K和D的弱推理规则:DA/A,OA/A,®口/-»口8//-»8,◊41OB/4-B。证明：本证明类似1.2.17的证明。.•.下面只补充不同之处：情况14是公理的代入特例：只须考虑模态公理。若是K的代入特例，则N4)=(B->C)t8tC。易见它是K的内定理。若4=口8-»08是D的代入特例，则6(4)=87「->8。易见它是D的内定理。情况34是据RN从前面某个4得到：；卜沟，且8(4)=3(口Aj)=Aj,•*.卜8(4)。 „说明：对其他基本系统，上述定理不成立。主要原因是上述情况1不能通过：口◊0一◊?是公理T的代入特例，但以后我们可以用反模型方法证明60OpTOp)=Ope「p不必然是含T的系统的内定理。口07口口0是公理4,但以后我们可以用反模型方法证明6(口0—口口°)=「一口。不必然是含4的系统的内定理。Op^DOp是公理5,但以后我们可以用反模型方法35参见后面练习3.4.10(1)①。证明&(◊「一口◊0)=Op不必然是含5的系统的内定理。从这里和1.2.17我们可以看到公理C,M,N,K和D(的代入特例)有一种对称性。这种对称性是1.1.7提到的其他公理(除了公理W)所不具备的。下面我们来考虑K的演绎定理。1.3.3定义令小，…，4是K中从。到X的推演。对每一143机W",称4在此推演中依赖4n0下列条件之一满足：4=4；(2)存在j,4Vi使得4从4和4据MP得到，且力和4至少有一在此推演中依赖Ami(3)存在_/<?使得4从4据RN得到，且4在此推演中依赖4。T说明：4依赖4“的直观意义是：4就是4或4是以Am为一个前提(可能还根据其他前提)经过若干步推演得到的。引理设在0u{4}1k8的某个推演中8不依赖4。则。FkB。证明：令8”…，8〃是K中从6j{4}到8的推演使得8在此推演中不依赖力。施归纳于IWiW”，只须证：(#)若5在此推演中不依赖人则。-8,。设5在此推演中不依赖4。分情况证明如下：情况18,是公理的代入特例或®则据推演的定①•.㈤在此推演中不依赖4.••无须考虑/=/的情况。义，。卜情况2存在/，左<〃使得8,是从5,和&据MP得到：•；5在此推演中不依赖4,.•.马和以在此推演中都不依赖儿据归纳假设，。卜身和。.•.据MP,易证0情况3存在〃使得8,是从与据RN得到：:B,在此推演中不依赖人.•.当在此推演中也不依赖4。据归纳假设，我们有0H即；.据RN,易证0H5,oT引理设d\j｛A｝卜kB,且存在K中从0u｛4｝到B的推演使得RN在其中有机<。次用于依赖/的公式。则01K□，人…八口"'/—>8。证明：设B\,…,B“是K中从入｛4｝到B的推演使得RN在其中有加<。次用于依赖4的公式。施归纳于下证：在K中，(☆)01口叮a…—>3"其中〃表示在推演丛，…，8,中运用RN于依赖4的公式的次数。因此当i=n时h=m。情况18,是K的公理的代入特例：则易见由H据RPC(蕴涵引入规则)，易证。14T80•.1=口，，二0卜口，-»瓦。；我们没有用RN,.•.(☆减立。情况2B,e@u｛4｝：若Bw©,则①H即其余如情况1所证。若8,=4,则0 其余也如情况1所证。情况3存在j,k<i使得8,从耳和Bk=BjTBj据MP得到，且在推演5，…，耳中运用RN于依赖4的公式有无次，在推演8”…，当中运用RN于依赖4的公式有人2次：据归纳假设，有0卜口，A…—>巨， 且卜□a•••a□l，2A o,:h，420，,易证卜口°/1人…aE|'/T口，A…Ad"/,P-□<)a……据三段论(RPC),易证P1口，a…»耳一》为，且•-口，人…据蕴涵分配规则(RPC),易见(☆)成立。情况4存在/<i使得8,从B)据RN得到«子情况1号不依赖出则据依赖的定义，Bi，…,Bj是K中从到名的推演使得用在此推演中不依赖A.据前一引理，0HBj,...据RN,0I-5„：.(P卜47比，...易见(☆)成立。子情况2号依赖4,且在推演S，…，身中运用RN于依赖力的公式有几次：据归纳假设，01□"“A…aD"47用,据RK.。1口'/a…人口"—>口用，'：hi<h,:.hi+19,二01口°/^…aEI'N—…Ad''9,再据三段论，我们有(☆)(1T据上面的引理，我们有:K的演绎定理(1)设以j{N}1k8,且存在K中从久j{N}到B的推演使得RN没有用于依赖/的公式。则01k/t艮(2)设41k8,且存在K中从N到8的推演使得RN没有用于依赖力的公式。则FkAt瓦T下面考察系统Do定理KcD»(2)下为是D的内定理或导出规则：d(i)oga，D(2)A/OA(=RN。)，D(3)OpvO-ip。D=K+O(p->p)。D=K+"O/。证明：(1)显然。(2)证D⑴:①□(/?—>p)->O(p—>p) D,US②□仍Tp) (1).K(l)③ O(p—p) ①，②，MP证D(2)：①/ 假设② 口4 RN③口/->◊/ D, US④ OA ②，③，MP证D(3)：据131(2),RcK,①②①②(3①②③d①②◊(pv「p)PC,D(2)◊pvO-ipR(2)据D(l),只须从K+O(pTp)推出D：VRcKcD,O(p->p) 公理◊(pTp)c(Dp—>Op)R(9)Dp-^Op ①，②，MP据(3)和D(2),只须从K+4/OZ推出◊(pip)：pTp PCo(/?—>/?) a/oaT1.3.8定义称1是常公式(constantformula)<=>A是用T和「，人或口构造出来的公式：/是用T作为原子公式构造起来的公式。T下面定理中的矛盾式是经典二值语义意义上的常假式。1.3.9定理令“是常公式。(1)若/々是重言式，则N是D的内定理。(2)若4口不是重言式，则Y是D的内定理。证明：令卜=卜口。施归纳于4的结构。情况1A=T：则不口=1"是重言式，二一4情况2A=「B：再分情况考虑：子情况1A口是重言式，则-vT。=「「8口不是重言式，.••8一口不是重言式，，据归纳假设，7, ”子情况27一口不是重言式：先证：(☆)用T和「或a构造起来的公式D是市言式或矛盾式[(☆)实际是经典句子逻辑中的一个结果。]施归纳于。的结构。若。是T,则。是重言式。若D=[E。则据关于(☆)的归纳假设，E是重言式或矛盾式，则是矛盾式或重言式。若0=Ea凡则据关于(☆)的归纳假设，E和尸是重言式或矛盾式。设E和尸是重言式：则。也是重言式。设E或产不是重言式：则据(☆)的归纳假设，E或尸是矛盾式，二。也是矛盾式。...(☆)成立。现在我们回到正题。•.7一口不是重言式，二据(☆%/T口是矛盾式，...8一口是重言式，，据归纳假设，卜8,；. ；.卜-vl。情况3A=BaC：再分情况考虑：子情况14口是重言式：因为工口=8口八C口，.IB口和C一口都是重言式。,据归纳假设，卜5且HC,/.14子情况24一口不是重言式：则易见一口或(T口不是重言式。.•.据归纳假设，有 或t~「C,二因此我们有1877),；.1-d。情况4A=DB：再分情况考虑：子情况14一口是重言式：口=广口，...8一口是重言式，据归纳假设，有卜8,.,.据RN,有卜口8,二卜儿子情况2 不是重言式：则8Y不是重言式，据归纳假设，有卜[8,...据RN,有卜口「8。据公理D,我们有i-O-.fi,据LMC,有卜-1口8,i-vl。T说明：这个定理揭示系统D的内定理集相对常公式的极大性：对每一常公式4/或-4是D的内定理。下面考察系统T。1.3.10定理(1)下列是T的内定理或导出规则：T(l)p—Op(=T。)，T(2)A/OA(=RN。)，T(3)D,T(4)Dp)。T(5)口-\(p―>□0)—>口―>paDcToT=K+T,,其中(Ti)(dp—pM—Og)。证明：证T(l)：① /+)口「 T,RPC②-n-ip^-iD-np US③ pTOp RER,DfOT⑴是T的逆对偶公式，，T(1)也可以从T和逆对偶定理1.2.10(4)直接得到。证T⑵:据T(l)。证T(3)：据T和T⑴。证T(4)：①□―◊□p T(l),US②◊—□夕).(口0-»0口?) R(9),US③ O(pTLIp) ①，②，RPC证T(5)：① O(pTUp) T(4)②—>□「) DfO③ 口—i(p―>LZlp)―>□―、p RPC⑵⑶①②③④据T(3)⑵⑶①②③④从T证Ti显然。下面只须证从K+T1证T：(□p—>p)v(―p—>◊―T],US(□p7p)v(-><>-ip—>p) RERTcRp(□p—>p)v(Dn—>p) LMCTcRp下面考察系统B.1.3.11定理TcB.(2)下列是B的内定理或导出规则：B(l)OAtB/4TDB(=RB),B(2)OUp—p(=B。)，B(3)ODp^QOp(=G),B(4)OC/jaOC^—>□<>(/?a^)oB=T+RBo证明：(1)显然。(2)证B(l)：①OAtB 假设②RM③ A-^UOA B,US④A^\JB ③，②证B(2)：据B和逆对偶定理1.2.10(4)。证B(3)：据B(2)和B显然。证B(4)：pAg7B,USOUpTp B(2)③④⑤G①②③④⑤G①②OCpAO□ ②，③，RPC◊□pA<>ElgTCIO(pAg)④，①据B(l),只须从T+RB证B：Op^OpPCp—>口◊/? RBT下面我们来考虑S4,这个系统有许多有趣的性质。据1.1.20,任意模态系统S都有弱规则US,.".若Hs$p—Sp，Hs则对所有4有我们可以有下面的约定：约定在不致混淆之处，我们用卜s©T力和1S©S、分别表示Hs©p10p和Hs T定理TcS4,(2)下列是S4的内定理：S4(l)口一□□，S4(2)S4(3)◊□◊一◊,S4(4)□◊一□◊□◊,S4(5)□◊一□◊□◊,S4(6)◊□一◊口◊口,S4(7)□一口◊口,S4(8)□(口p->g)T□pT□q0(3)(S4的演绎定理)eu{/}卜S48=。卜S4口/->8。证明：⑴显然。(2)证S4(l)：①□一口□ 4②□□一口 T, US③ □一□□ ①，②，RPC证S4⑵:据S4⑴和1210(6)。证S4(3)：①②证S4(3)：①②◊口◊一◊◊③◊口◊―证S4(4)：①口◊->◊口◊②□□◊—□◊口◊③□◊一口◊口◊证S4(5)：①□◊□◊一口◊②□◊一□◊□◊T,USRMoS4(2),RERT。，USRMS4(l),RERS4(3),RMS4(4),RPC证84(6)：据S4(5)和1210(6)。证84(7)：①◊口 To②口RM③口一□◊口 4

［证明2：；S4(7)是S4(3)的逆对偶公式，，据逆对偶定理1.2.10(4)立得。］证S4(8)：①□(□p-»g)—K②□(口/>―>q)——>CJq S4(1)>RER(3)设皿{4}1S4B。则存在8”…，B"是S4中从到8的推演。只须证：在S4中，(☆)0卜□/—>8" 对每一施归纳于IWiW"。在此我们只考虑不平凡的情况，其余情况请读者补充：存在/Vi使得8,从易据RN得到。据归纳假设，.,.据RM,01-口口/1—□易。.•.据4,01□/—»口鸟，0H口工一册T据上面定理的(2),易得：推论F列模态符串的序对相对S4等价：<oo,o>,<◊口◊口,◊□><>T定义A的模态度Deg(4)定义如下：①②③④Deg(p„)=0,对每一n<co；①②③④Deg(-iB)=Deg(B)；Deg(^A0=max{Deg(B),Deg(0),Deg(Q^)=Dcg(^)+lo(2)称/是"度公式<=>Deg(Z)="；(3)模态符串，的模态度Deg(/)定义如卜：Deg(O)=0；Deg(->/)=Deg(，)；Deg(□/)=Deg(^)+1.(4)称/是〃度模态符串=Deg(/)=〃。T说明：易见纯模态符串的模态度就是它的长度，且Deg(O/)=Deg(/)+k定义任给模态符串/和人(1)称。相对S可归约于#，记作/fs/，=0使得Deg(0)<Deg(/)。称/相对S可归约<=>存在0使得夕一s步。(2)称/相对S可归约于8oDeg(8)<Deg(4)且(3)称，相对S吸收实T说明：(一)在不致混淆之处我们省略“一s”的下标S。(二)据上述定义，Modal(S)及示相对S不可归约的模态符串的个数。据1.3.14,我们有：S4的归约定理相对S4,我们有下列归约关系：□□f口，口◊口◊一口◊,OO-O,◊口◊口一◊口。T1.3.18定理Modal(S4)^14o证明：据1212(3),只须证S4至多有下列不可归约的标准模态符串：(!(口◊口◊◊口nonOno-i-)□-nO->□<> -1<>□->□<>□ ->◊口◊我们先考虑上面一排。首先我们将它们编号如下：(1)% (2)口， (3)◊,(4)口◊, (5)◊口，(6)口◊口， (7)ODO.易见(1)是惟一的0度模态，(2)和(3)是两个1度模态。在(2)和(3)上叠加一个模态符(可加在前面也可加在后面)，我们至多有4个不可归约的2度模态符串：(8)口口，(9)oo,(10)no,(11)on,据归约定理,(8)和(9)分别可归约为⑵和(3)。在(10)和(11)上叠加一个模态符(可加在前面也可加在后面)，我们至多有6个不可归约的3度模符串：(12)□□<>, (13) (14)口◊口，(15)口◊◊, (16)◊◊口， (17)◊口口。据归约定理，(12)和(15)可归约为(4),(16)和(17)可归约为(5)。在(13)和(14)上叠加一个模态符(可加在前面也可加在后面)，我们至多有6个不可归约的4度模态符串：(18) (19) (20)◊口◊口，(21)OOOO,(22)□□<>□, (23)据归约定理，(18)可归约为(4),(19)和(21)可归约为⑺，(20)可归约为(5),(22)和(23)可归约为(6)。这样，在S4中没有不可归约的4度纯模态符串，从而(I)S4至多有7个不可归约的纯模态符串。在上述7个纯模态符串前加上下证：(II)S4没有形如©ASA的内定理。假设(【I)不成立，则和都是S4的内定理，易证「夕/和，T都是S4的内定理，矛盾于S4的协调性(参见1.1.16(1))。据(I)和(11),易见S4至多有14个不可归约的模态符串。T说明：(一)后面我们将证明Modal(S4)=14。Modal(S4)=14最早由Parry在1939年证明，读者可以参见Segerberg的口971](/?.59)。(二)在上述证明最后部分，我们实际证明一个更概括的命题：(ir)任一协调系统都没有形如灰4c「d/的内定理。(三)相对S4,不可归约的纯模态符串有下列关系：其中。一步表示-S4如f/：□-□on-onIIiI00-000i i0 ►◊说明：第1行的第1个f据S4(3)和逆对偶定理1.2.10(4),第1行的第2个一和第2行的左边两个I据T,第2行的第3个I,第3行的一和第5行的一据T。，第4行的右边的I据S4(3)。下面我们来考虑S5,这个系统比S4更有意思。1.3.19定理下列是S5的内定理。S5(l)◊一口◊,S5(2)口一◊口，S5(3)4,(从而S4qS5),S5(4)□(pr□])6口〃丫口q,S5(5)□(pvO^)<-^DpvO^,S5(6)O(p八S5(7)◊(/7人口9)10。八口幻S5(8)B,(从而BcS5),S5(9)G,(从而S4.2cS5)o证明：证S5(l)：①◊一口◊5②口◊7◊T,US③◊一口◊ ①，②，RPCffiS5(2)：据S5⑴和1.2.10(6)。证S5(3)：①口一◊口②◊口一□证S5(3)：①口一◊口②◊口一□◊口③口一口◊口④口一□口证S5(4)：To,US5,US①，②，RPCS5(2),RER①□(pvD^)—>D/?vOUq②口①"口夕)一口〃丫□夕③口,丫口口夕―>口9丫口夕)④Dpv□夕一口小口夕)⑤口伽\/口夕)<->口口口9证S5(5)：①口3/口◊[)一口夕\/口<>4②□(pvO^)<-^DpvO^证S5(6)：(T)口(一口一।[)<->口一ipv口一।夕K(4),US①，S5(2),RERM(5),US(3),S4(l),RER②，④，RPCS5(4),USS5(l),RERS5(4),US②③④证①②证①②③证①②②③④证①②证①②③证①②―iLJ(—ipvEJ-—i(LJ->pvLJ―>q) RPC◊TlpvrOq-OpvrOq) LMC◊(pAOg)cOpAOg RER5(7)：◊(/^◊□/6◊pAOdg S5(6),US◊(pAdg)-OpAC]g S5(2),RER5(8)：p—>0/2 To◊「—>口◊/? 5pTfJOp ①，②，RPC5(9)：□一◊D◊□一口◊S5(2),S5(l),RERH1.3.20S5的归约定理(1)相对S5,我们有下列归约关系：(☆)DD^D, <>□-□, □◊一◊,从而在S5中没有不可归约的2度模态符串，；.\10(1叫55)《6。(2)模态度大于1的公式相对S5可归约于®模态度小于等于1的公式。证明：⑴据S4的归约定理(1.3.17),S5(l)和S5(2),易见(众)成立，...在S5中没有不可归约的2度模态符串，.•.在S5中不可归约的标准模态符串至多有0, □, O»-1> ]□, —>◊。，Modal(S5)W6。》参见1.3.16(2).(2)令4是模态度大于1的公式，我们用下列方法进行归约：用缩写定义和RER消去T和c；用LMC等把「内移至句符前面：③用(1)给出的归约关系，把叠加模态符串归约为非叠加模态符串：④若据上述步骤得到的公式小还不是1度公式，则再据下列步骤进行归约：设A\含子公式口8使得Deg(8)>0。情况18=CaO：据R和RER内移口于8中。情况2B=CyD：子情况1C和。至少有一以口或◊开头：则据S5(4>-S5(5)和RER内移□于8中。子情况2C和。都没有以口或◊开头：•••Deg(8)>0,，Deg(C)>0或Deg(£>)>0。据本子情况的设定，我们不妨设C=CiaC2o据RER和R,□((C!aC2)vD)^□(C,vZ))a□(C2vD)o再据RER内移□于8中。若在经过上述内移后的合取肢或析取肢的模态度还大于1，则再据③或④进行归约，最后总能使B前面的口被B中的模态吸收。®设小含子公式使得Deg(8)>0。情况18=Cv0：据R。和RER内移◊于8中。情况2B=C八D：子情况1C和。至少有一以口或◊开头：则据S5(6)-S5⑺和RER内移◊于B中。®参见1.3.16(3).子情况2C和。都没有以口或◊开头：•.,Deg(8)>0,Deg(C)>0或Deg(0>O。据本子情况的设定，我们不妨设C=C,vC2»则据RER和Ro,1O((CivC2)a£>)<->O(CjaD)vO(C2aD)»再据RER如上内移◊于8中。若在经过上述内移后的合取肢或析取肢的模态度还大于1,则再如③或④进行归约，最后总能使B前面的◊被B中的模态吸收。重复上述步骤，最终我们能证明(2)。注意：我们在归约过程的开始、中间或结束遇到的公式有的可以直接归约为模态度为0的公式，例如，重言式或矛盾式的代入特例。T说明：(一)据上述(1),对系统S5来说，叠加模态符串不会增加新东西。更仔细地说：若。是叠加纯模态符串，则Oi…O”相对S5可归约于。”或者说O“吸收…0“一|。(二)以后我们要证明K,D.T和B没有上述归约定理。,.,口4—/和是S5的内定理，推论相对S5不可归约的纯模态符串是一个线序：说明：以后我们证明Modal(S5)=6。下面我们证明S5的模态合取范式存在定理。定义(1)称l是1度模态简单析取oA形如4V…v4,使得对每一1WiW",Deg(4)=0，或Deg(4)=l且4形如口8或◊以这时也称4是4的析取肢。(2)称/是1度模态合取范式<=>A形如4A…使得对每一lWiW〃，4是1度模态简单析取。这时也称4是/的合取肢。T说明：易见任何1度模态合取范式4的Deg(Z)e{0,1}。1.3.23例(1)下列公式是1度模态合取范式：p,DpA^vr),(□pvOgvr)A(OpvO(qw))。(2)下列公式不是1度模态合取范式：□□p,(□(pvO^)vr)Ar,DpA(Orv(^aO/?))»T定理(1)任给公式人存在公式8=8IA…a8”使得对每一14i《"，M是由形如5,.|>•••>Bh