资源描述：
《高级数理逻辑第9讲》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。
1、7模态谓词逻辑模态谓词逻辑与命题模态逻辑相类似,是将模态词引入到一阶谓词逻辑川形成的逻辑系统。对于模态谓词逻辑，我们从形式系统构成、语义结构和元理论三个方面来叙述模态谓词系统的构成。7.1形式系统构成与其他形式系统类似，模态谓词形式系统由语法构成和推理两个部分构成。7.1.1语法构成与其他形式系统一样，模态谓词形式系统的语法构成由：1.符号表：｛一阶+模态词｝•个体变元：兀•个体常元：ax•函词：⑴……斤”）……•谓词：斤..•联结词：一＞,-1•量词：V•括号：（，）•模态词：口，◊2.项1）变元、常元为项；2）对于自然数m如果％......匚为项，则••…匚）为项；3）项由
2、1）、2）经过有限步骤内形成的，除此Z外，没有英他的项。3.公式1）对于自然数n,如果人......-为项，则P4……-）为公式；2)如果A,B为公式，「A,AtB,VA,□A为公式；3)公式由1)、2)经过有限步骤内形成，除此之外，没有其他公式。7.1.2推理部分推理部分rti以下两个部分构成：1.公理集合1)一阶谓词公理2)模态正规系统公理：(k,D,T,B,4,5)3)模态词与量词关系：Vx□A□VxA2.推理：分离规则7.2模态谓词语义结构7.2.1语义结构与命题逻辑和谓词逻辑系统的关系相类似，模态谓词逻辑的语义与模态命题逻辑语义比较最主要的问题是引入了个体域的概念。从
3、而对于个体域产生了相关的指派解释等一系列相关的概念。1.结构:：模态谓词逻辑的语义结构由四元组，构成；其屮：U为宇宙；wwU为可能世界；R为是U上的二元关系，被称为可达关系；D为个体域集合；I为解释•个体域：既然有了个体域的概念，对于宇宙中的不同的可能世界，个体域是否相同呢？从直觉上来说，应该是不同的可能世界中的个体域是不同的。但是如果不同可能世界代表对应不同的个体域，则很难处理。为了解决这个问题，对于不同的可能世界上，所有的个体域都是相同的。如果对于真是情况，若不同，则将所有不同可能世界所对应的个体域的并集合作为整体。•解释I：解释I的构成有两种方式，第一种
4、与谓词系统的解释的概念一样，第二种对于不同的可能世界解释对同一个解释元素(如常元、变元和函数等)，对应与不同的解释方法。对于两种解释定义如下：■谓词解释>常元：a,I(a)eD>函词：f,1(f)为D*1上的函数—D的映射>谓词：P,I(p)为D11上的关系；■模态解释：将解释与可能的世界w相结合>常元：a,D>函数：f,函数>谓词：P，IW(P)关系1.指派对于指派，与解释I相同可以划分为谓词指派和模态指派两种形式。•谓词指派：概念与谓词逻辑相同；S为变元集合｛xi……｝到。上的映射。•模态指派：对于每个指派和可能世界w相对应，Sr为可能世界w,从变量集合｛xi……｝到个体域
5、D上的映射。2.赋值可能世界w中对解人，或/,及指派S,当且仅当对所有w,wRw,则“B在S和Iv下为真(Task!语义)；卜；OB当且仅当存在ww'Rw,卜;B在S和八下为真(Taski语义)；八八W实际上，到每个W上是一阶谓词逻辑系统。7.2.2语义相关性质1、性质1•一阶谓词的所有公理永真•与R相关特性永真：即对于R特性的公理永真。•分离规则保真性1、性质2：模态与塑词关系公理永真VxDA<=>□VxA证明：首先证明必要性：任取一个宇宙K,和其中任一可能世界vvgK:I.hrVxOA,则对于clwD,
6、=rnA(S[x/d])II.卜;□A(S[x/d]),则对于wRw
7、,卜：A(S[x/d])为真I.卜；A(S[x/d]),对于任一de卜;'A(S[x/d])所以，卜；VxAI(D为公用的)I.对于所有wRw,卜：VxA所以，hnVxA逆同样可证明。7.3元理论我们知道对于形式系统的元理论由三个方面构成，语法结构、语义结构和语法语义关系问题。対于语法结构和语义我们省略不讲，我们只涉及语法语义关系问题：1.合理性：对于模态谓词中的任意公式A,如果卜则卜；'A成立。证明：公里真推论保证逆归证明2.完备性：对于模态谓词中的任意公式A,如果卜；A,则卜;'A成立。例：证明□(ATB)T□(□AT□B)在NSK4中成立；证明：公理：□(AtB)t(□□
8、AtLJEJA根据演绎定理：a)EI(AtB)卜□B)b)□(□(AtB)T(□AT□B))T(□□(ATB)T□(□At□B))(k公理)c)□(□(AtB)t(LMtL]B))(□A公理)(b,c)(4公理)e)□(ATB)T□□(ATB)(a,e)(d,f)
