量词模态系统的代数语义与Kripke语义——关于S5~*情形

已故模态逻辑专家Lemmon在文献[1]和文献[2]中研究了一系列命题模态逻辑系统的代数语义与Kripke语义及其相互可转化性。他还在文献[1]中表示要用第三篇文章来讨论量词模态系统的相应问题;可惜该文未问世,Lemmon便溘然长逝了。在本文中我们对带量词的S5即S5~*而言讨论了两种语义的相互可转化性。S5~*在作者文献[3]和文献[4]中用S_5~*     

直觉主义量词模态逻辑的一个强完全性定理

在Ｔｈｏｍａｓｏｎ讨论到的直觉主义一阶谓词演算的基础上引进Ｐｒｉｏｒ工作中揭示的模态直觉主义系统ＭＩＰＣ的模态机制,从而得到一个直觉主义词模 逻辑系统ＭＩＰＣ,并给予它一个语义解释,证明其关于该语义的强完全性定理。多次实质性地用到Ｚｏｒｎ引理,因而在方法论上较Ｔｈｏｍａｓｏｎ的结果更加远离直沉主义观点。     

A.N.Prior的模态直觉主义演算MIPC具有13个模态辞

研究直觉主义系统的模态扩充,特别是在文献[1]中意义下属于S5型的有许多。这其中包括文献[2]中的系统IS5,以及文献[3]中的四个系统IM4W,IM4M,IM4S以及IM5。然而在这许多系统中提出最早且     

D.Hilbert第十问题的否定解决的两个简单推论

设Re、De和D分别表示全体递归可枚举集合组成的类,全体指数刁番图集合组成的类和全体刁番图集合组成的类(参看,例如,А.И.Мальцев或本文作者之).显然有     

关于判定问题的两个注记

1.在文献中Castaneda对Lewis模态命题演算S5证明了一条定理。此定理表明演算S5具有有穷模型性质,从而由之可推出S5的可判定性。略早于文献[1]时,著者在文献[2]中对于演算(?)_ε得到一条类似的定理,即文献[2]中的定理6。这里应指出,Castaneda在文献[1]中的定理和文献[2]中的定理6实质上是等价的。这里先对文献[2]中有关部分作一些修正。文献[2]的定理6陈述中的“B_0~()”应改为“B_0~(<2n>)”;相应地,该定理证明中     

关于Lewis的模态系统S5的几个注记

本文分三个部分:其一,将应用作者在文献[4]和[5]中得到的关于S5(即S_e)和S5(即S_e)的单纯完全性定理来证明Barcan公式和Prior的导出规则RLM可以分别在S5和S5中推出.这一事实已由Prior在文献[9]中指出,但本文给出的语义证明比[9]中的语法证明要简捷一些;其二,考虑了由S5添加命题量词而得的系统S5的判定问题;Kaplan在文摘[6]中已证明S5(在[6]中记为S5Q)为可判定的.在本文中我们采用Rasiowa和Sikorski在[10]中对一大类带命题量词演算S引进的代数语义方法并具体用到Ackermann在[1]中给出的关于二阶一目谓词演算P_m~2判定问题的一些事实得到更多的结果;其三,我们再次应用S5的单纯完全性定理重新证明S5具有6个模态辞.此事系由O.Becker首先于1930年在文[3]中证明的,本文中的语义证明比Becker[3]中的语法证明似要精致一些.     

关于无限值格模型论中条件(F_1)和(F_2)的可减弱性

在王世强等关于“格值模型论”的研究中,当值格L为无限(完备、“可补”)格的情形往往须假定L适合条件(F_1)和(F_2)方能将古典(二值)模型论中的结果移植过去。但是,就我们能见到的文献作一些考察之后,可以容易地看出,其中的条件(F_1)和