模态镜子里的反欧性，本文主要内容关键词为：镜子里论文,模态论文,反欧性论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
本文跨越模态逻辑的好几个领域。它从对应理论入手，转到完全性理论，再转到可判定性理论，最后止步于格论。整个这场漫游其实是由一个心血来潮的小问题引起的，应当先说说那是怎么回事。
一、谈一点背景
欧几里得从未插足模态逻辑，他的名字却频繁出现在模态文献里。众所周知，在S5-语义学中，克里普克框架F＝＜W，R＞内可能世界之间的可通达性关系R被赋予以下特殊性质：
欧几里得性——
，读作“有同一世界为其R-前趋的世界互为R-前趋”。
这个命名法的设计者是英国人莱蒙。他这样设计的理由是，当R被解释为＝时，上述关系性质就会变成《几何原本》中的一条公理“等于同量的量相等”①。
模态逻辑学者一直没有发觉欧几里得性身边有一位孪生兄弟，那就是反欧几里得性，简称“反欧性”——
，读作“有同一世界为其R-后继的世界互为R-后继”。
一直到20世纪80年代早期，研究自然语言中的二元量词的学者才把反欧性正式引入逻辑学家们的视野。他们的许多观察结果很出人意料。例如，欧几里得量词根本不存在，反欧几里得量词反倒多如牛毛②。本文第二作者惊讶之余，不能不疑心模态逻辑学者无视反欧性也许是一个错误。然而，从动念推敲反欧性的头一天起，第二作者便落入困境。
二、反欧性是模态可反映的么
只要可能，模态逻辑学者总要设法把他感兴趣的关系性质用模态语言说出来。按流行术语，这样的关系性质名叫“模态可定义的”。我们宁愿沿普赖尔更有表现力的老字眼，称之为“模态可反映的”③。一个关系性质P(R)是模态可反映的，如果存在着模态公式
，对于任何克里普克框架F＝＜W，R＞，F满足P(R)当且仅当F使有效。
入门书津津乐道的一些关系性质，如象自返性、对称性和传递性，都是模态可反映的。欧几里得性也是，一向充当路易士系统S5的特征性公理的公式：
E ◇p→□◇p
就是反映它的模态公式之一。
反欧性也是模态可反映的么？第二作者一度相信也是。不幸，他和他当年的学生为反欧性寻找模态等价物的多次试验，不但失败了，而且丝毫没有显出否定解似乎更言之成理，结果幻想依旧。说来滑稽，反欧性仅仅是某种一阶性质，而早在1975年便已经有了一阶关系性质的模态可反映性的判据④，那就是：
戈德布拉特—托马森定理 一阶关系性质P(R)是模态可反映的，当且仅当，┐P(R)在超滤子扩充的形成下保存，同时P(R)在不相交并、生成子框架和p-同态象的形成下保存。
然而，只是在本文第一作者也投入反欧性研究之后，我们才想到应当彻底告别试误法，以最大的耐性按部就班地应用这个重要定理久已配置齐全的判据。我们明白，这多半仍将是一个助探论证，必须做两手准备。假使一切顺利，我们会得到一个反欧性模态可反映的证明，尽管有可能依然不清楚它的模态对应物是什么。假使不很顺利，一时找不着办法来确定反欧性是否通得过所有四项测试，那就还是得不出最终的结论。毕竟，戈德布拉特—托马森定理本来没有提供“能行的”判据。
让我们回顾一下数年前实际完成的助探过程（不熟悉超滤子扩充等四种运算的读者从高等模态逻辑教材中可以查到它们的定义⑤⑥）。
我们尚未抵达最终目的地。所幸的是花这么大的气力做助探论证并非得不偿失。我们对否定解的正确性更有信心了。我们也懂得求得否定解的唯一有希望的途径是去表明反欧性在p-同态下不保存。然而，收获不限于此。仔细思考情况（Ⅳ）中所碰到的障碍就不难看出，尽可依样画葫芦地构造下面两个框架：
图1 框架F和G
注：此处。和·分别代表自返点和禁自返点。
只要规定f为从F到G上的如下映射：
那么G就成了F在映射f下的p-同态象。很清楚，F是反欧的而G不是反欧的。根据戈德布拉特-托马森定理，我们得到了
命题1 反欧性是模态不可反映的。
三、抗共死传递框架上的反欧性
方才的大否定结果强迫人们做抉择。假使不肯引进新型算子或新型规则来增强原有模态语言的表达力，又不肯根本放弃模态可反映的要求，只好降低要求。我们说，一个关系性质P(R)相对于克里普克框架类C是模态可反映的，如果存在着模态公式，对于C中任何框架F＝＜W，R＞，F满足P(R)当且仅当F使有效。
具体说到反欧性，应当选什么框架类呢？一般地取传递框架类肯定不行。事实上，图1中的框架F和G是传递的，可见反欧性在从传递框架向它的p-同态象过渡时不保存，反欧性相对于传递框架类同样不是模态可反映的。但是，只要给传递框架类加上一项很苛刻的限制就可以了。用λ(t)缩写存在量化式
，读作“t是活点”，那么，这项限制可以表述为
作者并不高估本节提到的对应论结果的重要性。谁都看得出来，抗共死性是一个典型的“证明生成的概念”⑦，除了排除像图1中的G那样的非反欧框架之外，很难说引进它还有更深的用意。况且抗共死性也无端地排除了一大批反欧框架，对研究反欧性明明不利。
四、K4T′B′——最小的反欧传递逻辑
撇开模态可反映性不谈，反欧性也可以对模态逻辑另有贡献，只不过一向无人留心而已。
考虑一个正规模态逻辑
问：K4T′B′是不是完全的？如果是，它被什么框架所刻画？
K4T′B′不仅完全，还是一种最为司空见惯的完全逻辑，叫做“典范逻辑”。每个一致逻辑的典范模型能够证伪该逻辑的每个非定理，但它的典范模型底部的典范框架未必能使该逻辑（的每个定理都）有效。只有典范逻辑的典范框架没有这个缺点，所以它恰好被它的典范框架所刻画。
典范性在逻辑的和运算
下保存⑧。K4的典范性是已知的，因此，为表明K4T′B′是典范的，只需要补充KT′和KB′的典范性证明。这实在很容易，我们只举KB′为例。
它说可通达性关系
具备拟对称性。足见逻辑KB′的典范框架的确能使B′有效，从而使KB′有效。总而言之，我们有了：
命题4 K4T′B′被它的典范框架所刻画，因而被全体拟自返和拟对称传递框架类所刻画。
然而，我们有理由不知足，有理由期待更“节省的”刻画结果：
命题5 K4T′B′被全体反欧传递框架类所刻画。
正因为这个命题站得住脚，人们才有权称K4T′B′为“最小的反欧传递逻辑”。怎么建立这个命题呢？我们都知道，每当框架类C刻画正规逻辑L，C中框架的点生成子框架所组成的类C′也刻画L。所以，只需要表明拟自返、拟对称传递框架的点生成子框架必定是反欧的，我们的目的便可以达到。
图2 框架F的若干生成子框架
生成点t或是死点或是活点。
我们已经无遗漏地枚举了逻辑上可能的情况。在所有情况下，点生成子框架
都是反欧的。不错，原框架F完全可以有图2d中所出示的那类非反欧的拟自返、拟对称子框架，但是它们永远也成不了点生成子框架的一部分，除非F的深度大于2！
五、反欧传递逻辑的有穷框架性
有了第四节的结果，我们可以有根有据地把K4T′B′的一切正规扩充都看成反欧的传递逻辑，因为它们都有适于自己的一类反欧的传递框架。不仅如此，它们还都是完全的，都被一类反欧的传递框架所刻画。进一步说，这类框架还能不太大，至多是有穷的。本节的主要任务正是要设法建立：
命题6 每个反欧的传递逻辑L都具备有穷框架性，就是说，对L的任何非定理，存在一使L有效但证伪的有穷框架。
不过，我们真正去证的并不是这个命题，而是表面上弱得多的——
命题7 每个反欧的传递逻辑L都具备有穷模型性，就是说，对L的任何非定理，存在一使L有效但证伪的有穷模型。
“弱得多”是假象，留待后文去说。要声明的是，塞格伯格已经极其一般地证明过一切深度为有穷的传递逻辑都具备有穷模型性和有穷框架性⑨，我们只是用更为径情直遂的方法把他的大结果的一种局部情况重证了一次。看来我们的方法也有它的妙处。
读者应当注意，在方才的有穷模型性证明中我们所用的有穷模型是所谓的“可区分模型”。根据塞格伯格的一个著名结果，如果L在代入下封闭，如果M＝
六、插议：三类反欧传递逻辑及其框架
后两节的内容要求我们给反欧性研究注入一种令常人怪异的眼光。源于英国人麦金森的这种眼光原是极其自然的，却至今被模态学者慢待了。
每个正规逻辑L的全体正规扩充构成一个格，可以记为NExtL。我们给格NExtK4及其子格NExtK4T′B′画一张“地图”，然后来解释麦金森的逻辑分类法。
图3 格NExtK4及其子格NExtK4′T′B′
与此相仿，K4T′B′，D4T′B′，Q4T′B′分别是NExtK4T′B′中最小的居间型、无谓型和无稽型逻辑。读者必须注意，D4T′B′＝S5。这说明K4T′B′的无谓型扩充无非是S5及其真扩充。
现在可以很准确地把握住三类反欧传递逻辑的框架有什么特征。当然，这些框架一定不出图2中a，b，c的范围，为便于记忆，我们称a为“黑子”，b为“球”，c为“仙人球”。
在NExtK4T′B′中，当LogF属无谓型或无稽型时，F既可以是点生成的又可以是若干点生成框架的不相交并。只描述前者的特征就行了。
稍费心思的是居间型的LogF。姑且假定F是点生成的。这时，F不能是黑子，也不能是球，因而深度应为2。在F的终端，必须有死点，否则LogF变成无谓型的；又必须有活点，否则LogF变成无稽型的（仙人球）。但是，兼有死终点与活终点的点生成框架根本不会是反欧的。
这样看来，对于居间型逻辑LogF，F只能是无谓型框架（球）与无稽型框架（黑子或仙人球）的不相交并。例如说，假使把NExtK4T′B′中最小居间型逻辑K4T′B′看成一框架F上的逻辑LogF，F不会是点生成的，但可以是一只最大球与一只最大仙人球的不相交并：
最大球是NExtK4T′B′中最小无谓型逻辑D4T′B′的框架，最大仙人球是NExtK4T′B′中最小无稽型逻辑Q4T′B′的框架。
七、从可有穷公理化到可判定性
前面已经证明过反欧传递逻辑具备有穷框架性。一旦证明它们也是可有穷公理化的，便自动得出它们都是可判定的。
命题8 每个反欧传递逻辑L都是可有穷公理化的。
证明：我们要利用麦金森分类法所提供的眼光——辅以范因的技术(13)——来处理这个有点麻烦的问题。
情况1：L属无谓型
依照上节的说明，L是球的逻辑——S5或其真扩充。S5＝K4TB，S5的每个真扩充可表述为
的形式，它们都有一有穷的公理集。
情况2：L属无稽型
依照上节的说明，L或是黑子的逻辑或是仙人球的逻辑。黑子的逻辑就是
，除K的公理外只添了一条公理。仙人球的逻辑虽然多种多样，却也无例外地可有穷公理化。好就好在仙人球的结构实在简单。
对一个由点t所生成的仙人球F，只有两个参数是重要的，一是非萎团C(t)的基数，一是在C(t)后面的死点集D的基数。假定F的这两个参数依次为正整数a和b，我们把有序数偶τ＝(a，b)叫做F的关联数偶(list)，把F叫做数偶τ＝(a，b)的关联框架。我们还说数偶τ＝(a，b)覆盖数偶σ＝(c，d)，如果a≥c并且b≥d。懂得p-同态的人一眼便能看出。
引理1 令τ和σ分别是仙人球F和G的关联数偶。如果τ覆盖σ，那么存在一从F到G上的p-同态映射。
关于数偶本身，有一简单的组合论结果是不久就要引用的：
系理1 每个反欧传递逻辑都是可判定的。
八、NExtK4T′B′中濒表格逻辑的两极化
我们对反欧传递逻辑的初步研究已经能够显示历来无人问津的格NExtK4T′B′的一些颇为有趣的性质。例如，既然有穷模态公式集总共只有可数多个，从第七节的可有穷公理化结果可以推出NExtK4T′B′不大，只含可数多个逻辑。又例如，既然有穷公理化的有穷深度逻辑都是所谓的“有穷并裂口”，因而都是所谓“框架逻辑”(14)，那么格NExtK4T′B′是由框架逻辑组成的。
不想谈得太深，但NExtK4T′B′中濒表格逻辑的分布问题恐怕不可不谈。
一个有穷框架F上的逻辑LogF叫做表格逻辑。正规逻辑格NExtL[,0]中的逻辑L，如果它本身不是表格的但它在该格中的一切真扩充都是表格的，就称作濒表格的。毫无疑问，任何濒表格逻辑一定是某单一可数框架F上的逻辑LogF，却绝对不会是另外两个互不包含的逻辑的交。既然NExtK4T′B′中的居间型逻辑全是这样两个逻辑的交，可见这个格里压根儿不存在居间型的濒表格逻辑！濒表格逻辑位于两极是这个格的一个很根本的特征，在图3中早有清楚的表现。
NExtK4T′B′中唯一的无谓型濒表格逻辑是最大球的逻辑S5＝D4T′B′。然而，无稽型濒表格逻辑却有两个：
图4 逻辑Q4T′B′F[+]与Q4T′B′H的刻画框架
两极化现象算不上最有趣，毕竟在某些热门格（如象NExtK4.3）里也没有居间型濒表格逻辑。更有趣的恐怕是“临界”现象。
两年前，本文第一作者曾这样写道：“麦金森分类法也引起若干涉及居间型的濒表格逻辑与非表格逻辑的问题。按麦金森定理，每个居间型逻辑L∈NExtK4都有无稽型扩充与无谓型扩充。……如果这个居间型L只是非表格的，L会不会具备那么一种‘临界性’，即L的一切濒表格扩充都是无稽型的或者都是无谓型的？这是一个真正费解的难题。”(15)
在NExtK4T′B′中，居然能不费周折就找到了“临界的”居间型非表格逻辑，这里只提两例。
尽管本文止步于此，但我们的研究显然可以继续深入下去。从反欧性的模态不可反映这样的小问题出发，我们对反欧传递逻辑有了进一步的认识，并且解决了之前一些悬而未决的问题。相信这样的研究过程决非孤例。
注释：
①E.J.Lemmon,D.S.Scott.The Lemmon Notes:An Introduction to Modal Logic.Oxford:Blackwell,1977,p.54.
②
"Some results on quantifiers",Notre Dame Journal of Formal Logic 1984(25),pp.152～170.
③A.N.Prior.Past,Present and Future.London:Oxford University Press,1967,p.45.
④R.I.Goldblatt,S.K.Thomason."Axiomatic Classes in Propositional Modal Logic",In J.Crossley(editor).Algebra and Logic.1974,pp.163～173,Springer.
⑤A.Chagrov,M.Zakharyaschev.Modal Logic.London:Oxford University Press,1997.
⑥P.Blackburn,M.deRij ke,Y.Vennema.Modal Logic.London:Cambridge University Press,2001.
⑦拉卡托斯：《证明与反驳》，上海译文出版社1987年。
⑧A.Chagrov,M.Zakharyaschev.Medal Logic.
⑨K.Segerberg.An Essay in Classical Modal Logic.Filosofiska Studier 13.Uppsala:University of Uppsala,1971.
⑩K.Segerberg.An Essay in Classical Modal Logic.
(11)D.C.Makinson."Some Embedding Theorems for Modal Logic",Notre Dame Journal of Formal Logic,1970,(12),pp.252～254.
(12)杜珊：《论麦金森定理及其等价命题》，载《华中科技大学学报（社会科学版）》2005年第3期，第21～25页。
(13)K.Fine."Logics containing S4.3",Zeitschrift für mathematische Logik und Grundlagen der Mathematik,1971,(17),pp.371～376.
(14)A.Chagrov,M.Zakharyaschev.Modal Logic.
(15)杜珊珊：《论NExtK4中的濒表格逻辑》，武汉大学博士学位论文2008年，第84页。