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

模态逻辑讲义（2006 年）李 小 五 编 著中山大学逻辑与认知研究所第1 章公理化系统在本章 1 我们给出模态语言和模态公式，讨论它们的语形特性，引入刻画模态的公理和推理规则，然后定义本书主要关注的公理化系统，并定义相对模态系统的形式证明和推演概念最后我们证明这些系统是协调和和谐的从 2 到 5 我们分别介绍初等系统、基本系统、退化系统和其他重要系统，着重证明这些系统的内定理和导出规则以及这些系统之间的相互关系我们也证明某些系统的元定理，例如，等价置换定理、对偶公式定理、对偶符串定理、演绎定理、归约定理、Post-完备性定理和模态合取范式存在定理这些定理往往是经典逻辑相应定理的本质推广1 公理化系统 协调性 和谐性本节我们给出模态语言和模态公式，讨论它们的语形特性，引入刻画模态的公理和推理规则，然后定义本书主要关注的公理化系统，并定义相对模态系统的形式证明和推演概念最后我们证明这些系统是协调和和谐的为了简洁，本书我们用=表示元语言意义上的“当且仅当”，用=表 示“若，则”，用表 示“并非”，用：表 示“因为”，用 表 示“所以”1.1.1定义（1）称 L是（句子型的）模 态 语 言 o L由下列互不相同的符号组成：句 符 集:A t=d f 3，p（,）；逻辑符：，口，A；技术符：（，）。

2）递归定义ML是满足下列条件的最小集合：Ay ML；A,B e M L =N,DA,（4 人 8）e M LH说明：（一）上述表示非空集At是可数的，即 A t 或是有穷的，或是可数无穷的At中的元素称为句符句符通常也称为命题变元或句子变元或原子公式通常也把ML称为模态语言，这似乎更符合我们对语言的直观理解和 1 人称为联结符读作：非）直 观 上 表 示“否定”，A（读作：合取）直观上表示“并且”，它们通常称为真值联结符或命题联结符口（读作：必然）称为模态符或（一元）模态算子从上述定义看，口也是 一 个 元联结符，只是在本书我们一般不把它解释为真值联结符本书我们用口指称要讨论的模态概念这个概念通常理解为 某 种“必然性”实际上，人们在I I常思维中有各种模态概念，其直观语义多种多样，但本书一般不讨论本书主要研究模态逻辑的技术部分，即使在语义方面也着重研究两种形式语义当然，不同的形式语义，特别是不同的公理化系统，刻画了不同的模态符，而这些差异的后面实际上有不同的直观语义（背景）请有兴趣的读者参见相关的文献At的基数是有穷或可数无穷的但事实上，本书的绝大部分结果对任意基数的句符集皆成立三）对任意形如口4的公式，称”是口的辖域。

四）今后若不特别提到，我们总用元变元p,q,（带或不带上下标）表 示At中的公式，其 中p,q,r分别特指P i，p2,而；用元变元A,B,C,D,（需或不带上下标）表示ML中的公式；用r,弘0,三，（带或不带上下标）表示公式集，即ML的子集五）上述一提到的符号互不相同，.通过（2）得到的ML中的句子具有唯一可读性，并且具有可枚举性设语言L是可数无穷的，即A t是可数无穷的由L构成的ML中的公式是有穷个符号构成的符号串，.据集合论的基本事实，可数无穷集的所有有穷子集的个数仍是可数无穷的，.我们可以枚举ML中的所有公式如下：A 1.，A，o关于这方面的严格表述和证明，请 读 者 参 见E n d er t o n的 1972(六)“T ”称为结束符用在定义、引理、定理和推论等后面1.1.2缩写定义(Df v)AvB)a A-IS),(Df )(A B)df I(/AiB)(D f-)(Z-B)=df(/T3)A(B f 4),(Df O)/=df C!F,(Df T)T=df(p v p),(DLL)_L-df iTo说明：(一)上述定义前面的Df v,Df.,分别是相应定义的缩写这在将来证明系统的内定理时是很方便的。

)v(读作：析取)直观上理解为“或”，7(读作：蕴涵)直观上理解为“若，则”，一(读作：等价)直观上理 解 为“当且仅当”，(读作：可能)直观上理解为”是可能的”三)也称为模态符或模态算子以后和 都简称为模态LL3约定(1)为了节省括号，本书我们约定公式最外面的括号可以省略，且公式所含的联结符相对公式的结合力依次减弱：-1,A,V,o(2)同类联结符满足右向结合律,例 如，我们用小T-4,表示：小-i-4)0(0是空集符号)是有穷集，则我们用八0和V 0分别指称的所有元素(据某个固定的排序方法)的合取和析取4 ,则/O=d f/，V O=d f/0,则 A0=d f T，V 0=d f a T说明：关于(4)的定义，直观解释如下：考虑八0=d f T我们知道，人为真的充要条件是()若 衣，则/真0时，不成立，：.()空洞成立我们把A0定义为T同理可解释V0=d f _ LLL4定义(1)A的子公式集Su b )是最小集合卜使得 A c 3；B e W；BAC三甲n B,CW：口8%=BeW.(2)我们用S u b()表示0 的子公式集：S u b(0)=u S u b(/)：(3)称 0 在子公式下封闭o S u b )=。

4)若A 是或口 员 则我们称B 是 4的实主子公式(p r op e r m a i n s u bf or m u l a)这时称-1和 口 是/的主联结符若 4是B C 则我们称8 和 C是 4的实主子公式这时称A是A的主联结符实主子公式也称为真主子公式或简称主子公式T1.1.5定义(1)称o是代入映射是从At 到 ML中的映射任给公式A,称 Zo是/的代入特例(s u bs t i t u t i on i n s t a n c e)0 如下递归定义：P Q=Q“)，对所有nw,办(5AQ7=(S7)A(C 口，口,(C)八口乡一口人9),(N)口(K)n(p q)口夕，(D)口Op,(T)CJpTp,(4)/?一，(B)p一(5)OpT U O p,(G)口一 2，(McK)口，(H)(pA pg)v (9 人 q p)，(W)口(/?一)一口夕，(Lem)(/?(Dum)(p p)p)O p ip2)推理规则(RN)A/D A,(RM)(RE)L8/口4 1 口8,(RR)/ABTC/CMACIBTLIC,(R K)小A人 4 /口小人 AO4,/，对所有n,(RER)AB/C-C(AB)。

T说明：(一)上述公理和规则左侧的大写字母串表示它的名字(通常是英文名称的缩写)，其中推理规则前面都冠以R二)当 =0 时，据 1.1.3(4),RK 是 T/TTL U,而此规则本质上是RN三)下面我们对上述部分公理和规则作些简要的说明：K 是 为 了 纪 念 K r ipke命名的一条公理，但 据 R.A.BulI和K Seger ber g在 其 1984(p.20)所说：“K r ipke似乎从来没有关注过这条公理”笔者认为K 是模态逻辑的一条相当重要的公理，用此纪念Kr ipke对模态逻辑做出的奠基性贡献也是恰当的D是deontic的缩写，T最早是由R.Feys提出和命名的5也记作E,而后者是Euclidean的缩写B是Br ouw er 的缩写，：T+B 与直觉主义逻辑有关联McK是McKinsey的缩写，也记作.1G是G each的缩写，也记作.2Lem是Lemmon的缩写，也记作.3H是Hintikka的缩写，Dum是Dummett的缩写W是(anti-)w ellor der ed的缩写文献中也记作G 或GL,其中L用来纪念M.H.LOb,他提出下面提到的系统KWRN是Rule of Necessitation的缩写，称为必然化规则。

RM是Rule of Monotonicity的缩写，称为单调规则RE是Rule of Eq uivalence的缩写，称 为（可证）等价规则或全等规则（Rule of Congr uence）RR是Rule of Regular 的缩写，称为正则规则RK是Rule of Kr ipke的缩写，称为正规规则RER是Rule of Eq uivalence Replacement的缩写，称为（可证）等价置换规则1.1.8定义和约定令 是公理集（本质上就是一集公式），R 是推理规则集1）称s=是（一般意义上的）模 态 系 统 o s 是如下构成的系统：S 的公理是P C 的公理和，S的推理规则是MP,U S和 R2）这时称是 S（相对P C）的特征公理的集合，R 是 S（相对 P C）的特征（推理）规则的集合T说明：（）为了方便，当 厂 或 R 为空集时，我 们 用 S=或 S=来表示 S=或 S=o注意：当厂和R 皆为空集时，S=P C任给模态系统S=令 八 是新公理集且R 是新推理规则集为了方便，我们也用S+Q+R 表示o参见 1.1.11(5)令 A 是新公理，我们也用SA 简单表示S+A。

我们还用S-A,S厂和 S-R 分别表示从S 中去掉公理A 和公理集和规则集R 得到的系统下面的定义给出的模态系统是本书主要的研究对象1.1.9 定义E=df,M=dfEM,R=df MC,K=df,D=df KD,T=d fKT,B=dfTB，S4=dfT4，S5=dfT5,K4.3=df K4Lem,S4.l=dfS4McK,S4.2=dfS4G,S4.3=dfS4LemT下面我们分别引入形式证明、内定理和推演概念：1.1.10 定义 令 S 是任意模态系统1)称公式序列小，4,是 S 中的形式证明o 对每-i 使 得 1 下列条件至少有一成立：4是S的公理的代入特例；存在),kV i使得4是从4和4据M P得到的；存 在，和力使得4,是从4 j，4n，据s中的特征规贝(模态规贝U)得到的2)称/在s中有形式 证 明=存 在s中的形式证明小，4使得4=4(3)称/是S的内定理，记 作-s/，0 N在s中有形式证明我们用Th(S)表示S的所有内定理的集合4)若/CT h(S),则我们也记作 4,并 称，是S的非内定理5)称/和8相 对S等价 Q%”一 瓦 T说明：(一)上述条件一也可以等价表示为：4是S的公理；存在，k V i使得4是从4和4据M P得到的；存 在 加 和 力，使 得4是从/八，4“据s中的特征规贝ij(模态规则)得到的：存 在 使 得4是从4据u s得到的。

)易见公理自身也是内定理i.i.i i定义(1)称公式序列小，4是S中从的 推 演 o对每一 下列条件至少有一成立：4是S的公理的代入特例；换句话说，存在S的公理A和代入映射 T使得4=A b存在J,左使得4 是从4-和念据M P 得到的；存 在 加(和力，/“i 使 得 4 是从4 i，4M据 S 中的特征规则得到的2)称/在 S 中有从的推演或称Z 在 S 中从推出，记 作i s/，o存 在 S 中 从的推演小，4,使得4=A.这时也称小，4,是 S 中从到力的推演为了方便，以后用S,表示：对每一/%我们也用加(0)表示/eM L：一 幻，且称Cns(初是相 对 S 的可证后承集3)若/任Cns(初(即/没 有 S 中 从 0 的推演)，则我们也记 作 0%/小，An,则我们用A,月“入 N表示 A,用 小，表 示卜 sZ5)称 R=4，An/A是 S 的(强)推理规则，记 作 ReRule(S),o 对所有代入映射A ff,AaHsAG称 R 是 S 的导出规则o ReRule(S)使 得 R 不是构成S 的推理规 则 少6)称 R=4，4“/A是 S 的弱推理规则，记作ReWRule(S),=若 小，且 则(7)称 小，An/A是 S 的虚规则o 存 在 iWiW”使得 S 没有任何形如4 的内定理。

构成S的推理规则称为S的初始规则 例如，MP就是。