形式化数理逻辑_第1页
形式化数理逻辑_第2页
形式化数理逻辑_第3页
形式化数理逻辑_第4页
形式化数理逻辑_第5页
已阅读5页,还剩58页未读 继续免费阅读

下载本文档

版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领

文档简介

1、1形式化数理逻辑形式化数理逻辑n侯越先,, 25-B-510n一般性参考: 离散数学,左孝凌等,上海科学技术出版社 数学家的逻辑,哈密尔顿,商务印书馆 元数学导论, SC克林,科学出版社n课程辅助材料: 2重新审视逻辑的本质n真与逻辑n经验意义上,命题的“真”指命题的断言符合其所指涉事物的实际状态n逻辑(Logics)研究的是有效的推理方法,数理逻辑(Mathematical Logics)就是用数学化(符号化)的手段,研究有效的推理方法3重新审视逻辑的本质n什么是有效推理方法? a 有效推理方法应具备保真性,即如果推理前提真,则推理结论真 b 有效推理方法的保真性应具有普遍意义,即不同的人,

2、在不同的应用背景下使用相同的推理过程,可获得真值相同的结论n有效推理的例子:三段论4重新审视逻辑的本质n两个基本问题: 问题1:是否所有真命题都可从特定的逻辑前提出发,由满足条件a和b的逻辑推理过程获得? 问题2:如果推理前提真,有效推理方法的结论是否无条件地真?5重新审视逻辑的本质n问题1(是否所有真命题都可从特定的推理前提出发,由满足条件a和b的逻辑推理过程获得?)n下面各个推理结论(蓝色部分)的真值由何决定? 例1 因为他是医生,所以他是大夫 例2 如果下雨,野餐取消; 现在确实下雨了; 野餐将取消 例3 如果A胜过B; 且B胜过C; 则A胜过C 例4 任何一个男同学都不能断定本语句是真

3、的6重新审视逻辑的本质n获致“真”的途径: 基于逻辑的真(基于形式的真) 基于语义的真 基于直觉的真n注:4与说谎者悖论的区别 4与哥德尔不完备性定理之间的关系n数理逻辑的研究目的:研究形式有效的推理,用形式手段地刻画人们对形式真的朴素理解。7重新审视逻辑的本质n问题2(如果推理前提真,有效推理方法的结论是否无条件地真?)n例子(量子物理的双缝实验):电子e通过左缝隙或右缝隙达到屏幕,且通过缝隙时的动量是pn小练习:将以上例子用命题逻辑符号化n量子逻辑:刻画量子世界的命题逻辑1 G. Birkhoff and J. von Neumann, The Logic of Quantum Mecha

4、nics2 http:/wapedia.mobi/en/Quantum_logic8重新审视逻辑的本质nRemark 1:形式逻辑系统本质上是一种形式约定系统,系统内的真命题(永真式)只在形式约定的意义下为真,而并不必然对应于实际物理状态。nRemark 2:只有当形式逻辑系统的解释(即模型)确定之后,才可能讨论形式命题(在特定解释下的)“物理真实性”。一般来说,古典逻辑系统适用于经典物理世界,因此在日常情况下,基于古典逻辑系统得出的真命题对应于事物的实际状态。以下我们约定已给出合适的模型,使得形式真等价于真9形式化数理逻辑的研究目的形式化数理逻辑的研究目的n1 研究逻辑(形式)有效的推理,用

5、形式手段刻画人们对逻辑(形式)真的朴素理解n2 研究形式逻辑系统的元性质:可靠性、可判定性、完备性等n形式化命题逻辑、形式化谓词逻辑、形式化非古典逻辑n思考题:是否有可能对基本的形式逻辑系统加以扩张,使其可把握其他类型的真?详细说明你的意见10形式数理逻辑的主要研究内容n3 扩展研究目的n模型论、证明论、递归论、公理化集合论 模型论:用数理逻辑和集合论的方法解释、分析形式的(数学或物理)概念和系统 证明论:用数理逻辑的方法研究数学证明的过程 递归论:研究解决问题的可行的计算方法和计算的复杂程度11形式化命题逻辑系统Ln(非形式)命题逻辑系统的能力和局限 命题逻辑系统的结论都是真的吗?(考虑命题

6、逻辑中真的定义) 命题逻辑系统的能力是否足够强,使得我们可由命题逻辑系统(算法地)推出所有的逻辑真命题?n引入形式化命题逻辑系统 理论方面:澄清命题逻辑系统的元性质(一致性、完备性和可判定性等)、澄清基本的数学哲学问题(例如数学是否可以形式化) 应用方面,形式化逻辑系统在人工智能、软件工程等领域有着深入的应用。n命题逻辑的形式系统L定义如下 1 符号字母表: ,(,),p1,p2,p3, 问题:为何只有两个逻辑联结词和?12形式化命题逻辑系统L2 命题公式的集合:如下3条递归规则确定命题公式的集合(1)对每个i=1,pi是命题公式(2)若A和B是命题公式,则(A)和(AB)是命题公式(3)所有

7、命题公式由递归应用(1)和(2)产生 注:在不引起歧义的情况下,括号可省略3 公理模式: L1: (A(BA) L2: (A(BC)(AB)(AC) L3: ( A)(B)(BA) 注:A、B和C可以是任意命题公式 显然,公理L1-L3是永真式 13形式化命题逻辑系统L4 演绎规则(分离规则,记为MP):从A和(AB),可以获得Bn定义1:L中的一个证明是命题公式的一个序列A1,A2,An,使得对每个i(1=i1时,假设L中证明序列长度小于n的定理都是重言式(归纳假设)。由于定理A在L中存在一个证明,则A或者是L的公理,或者由MP规则获得。当A是L的公理时,A显然是重言式。当A是由MP规则获得

8、时,其证明序列中必存在两个命题公式,不失一般性,记为B和BA。由于B和BA的证明序列长度小于n,由归纳假设,它们是重言式。这样A必然是重言式。 综上,L是可靠的。17形式化命题逻辑系统Ln定理2(一致性定理):L是一致的 证明:反证法,若L是不一致的,则存在命题公式A,使得A和A均为L的定理。由L的可靠性定理,L的定理必是重言式,矛盾。n定理3(完备性定理):L是完备的18定理4证明概要(数学家的逻辑)n引理1: (AA)是L的定理n证明: 1) (A(AA)A) L1 2) (A(AA)A) (A(AA)(AA) L2 3) (A(AA)(AA) MP 4) (A(AA) L1 5) (AA

9、) MP 19定理4证明概要(数学家的逻辑)n定义6:L* 称为L的扩张,如果L*是通过改变或扩大L的公理集合而得到的一个形式系统,使得L的所有定理仍是L*的定理。n问题:增加L的公理,是否必然增加L的定理?是否可能采用完全不同的公理集,但导出完全相同的定理集?n注:若L*是通过在L中增加公理集合X获得的,则L*可记为L+X;n注:以下两个说法是等价的 1)命题公式A在L+X中可证 2)命题公式A可在L中由前提X推演(证明)出 3)可记为X|-A 或 |-A L L+X20定理4证明概要(数学家的逻辑)n定义7:L的扩张L*是一致的,如果不存在命题公式A,使得A和A均为L*的定理n演绎定理:若

10、B是在L+X中增加公理A后形成的扩张系统的定理,则(AB)是L+X的定理n证明:数学归纳法并利用引理1的结果n注:逆定理成立n推论:对于任意的A、B和C,在L中可由(AB)和(BC)证得(AC)n证明:在L+(AB),(BC),A中易证C,由演绎定理, L+(AB),(BC)中可证(AC)n注:此推论可进一步扩展;此推论在逻辑推演中的使用称为HS规则21定理4证明概要(数学家的逻辑)n引理2:A(AB)和(AA)A是L的定理n一致性判定:由引理2,L的一个扩张L*是一致的,当且仅当存在一个命题公式A,A不是L*的定理n引理3:设L*是L的一致扩张,又A是L的命题公式,且A不是L*的定理,那么由

11、L*增加A而得到的扩张L*也是一致的n证明:反证法,利用演绎定理和引理2的两个定理。n定义8:L的一致扩张是完全的,如果对于任意A,A或A是此扩张的定理n注:注意这里的“完全”与前面提到的完备性之间的区别n引理4:设L*是L的一致扩张,则存在L*的一致完全扩张22定理4证明概要(数学家的逻辑)n定义9:L的一个赋值是一个函数v,它的定义域是L的命题公式集合,它的值域是T,F,使得对L的任意命题公式A和B,有 1) v(A) v(A) 2) v(AB) = F iff v(A)=T 且 v(B)=Fn注:对L的命题符号p1,p2,的真值指派与L的赋值之间存在一一对应关系。一个真值指派可决定一个赋

12、值;反之,合法的赋值对应着一个真值指派。n引理5:若L*是L的一致扩张,则存在一个赋值,使得L*中的所有定理取值Tn证明:赋值由L*的完全一致扩张J给出。只需证此赋值满足定义9中的1)和2)即可23定理4证明概要(数学家的逻辑)n定理:L是完备的(L的完备性定理)n证明:反证法,假设L不完备,则可在L的公理集中增加了某个永真式Ak的否定,形成一致扩张L*。由引理5,存在赋值v使得L*中所有定理为真,则Ak在此赋值下也为真。这意味着永假式Ak在某个真值指派下为真,矛盾24形式化命题逻辑系统Ln定理4(可判定性定理):L是可判定的。 证明:真值表法。n问题:真值表法能否作为一般方法在实际自动推理系

13、统中应用?n总结:L具有我们所期望的性质(可靠性、一致性、完备性等)n问题:是否可能存在其他的形式命题逻辑系统(不同的联结词、不同的公理),也具有L的性质?n思考题(作业):构造一个使用逻辑联结词、和的形式命题逻辑系统:说明你构造的系统公理和推演规则;证明其具有L的性质(可靠性、一致性、可判定性和完备性)。25形式化命题逻辑系统Ln思考题:既然利用形式命题逻辑系统可以中肯把握(命题的)逻辑真,可否扩展的形式命题逻辑系统,以中肯地把握特定意义下的数学真(Hilbert方案)?例如,构造形式化数论系统。这样的系统是否也具有系统L的良好性质?n思考题:如果上一个问题的回答是肯定的,这样的数学系统的全

14、部内涵即可由形式系统囊括,至少在原则上,我们可以编写一个计算机程序,利用简单地穷尽搜索,逐步获得一个又一个定理,数学发现的过程可以还原为计算机程序操作,这个思路是否可行?26形式化命题逻辑系统Ln 线索:这样的前景不会发生。绝大多数实际数学系统的形式化是不完备的(哥德尔第一不完备性定理),甚至其一致性也无法在系统之内得到证明(哥德尔第二不完备性定理)。数学真理不可能由包括程序在内的任何机械过程所穷尽,而必然包含直觉和洞察的成份。存在着对于人的直觉来说明显为真,但无法形式证明的良定义数学命题(Godel命题;Goodstein定理等);存在无限多不可由“机械过程”计算的函数(图灵);存在着具有重

15、要实际意义,但无法被机械过程解决的判定问题(停机问题图灵;丢番图方程解的存在性问题(希尔伯特第十问题)。27形式化命题逻辑系统Ln注:机械过程现代数字计算机程序算法图灵机 所谓的“机械过程”,应广义理解,指可实现的经典物理过程。 “机械过程”涉及到数学之外的物理的内涵。量子计算的某些最新理论研究结果似乎暗示,某种理论上的量子计算模型似乎可以实现某些经典物理过程无法实现的计算任务(如等价于停机问题的丢番图方程解的存在性判定问题),但是上述结果尚未形成定论。n思考题:某些人认为,形式数学系统的不完备性意味着人工智能的不可能性,存在着直觉上为真但形式系统内无法证明的真理,说明人心比机器和程序更优越,

16、程序不可能充分模拟人类智能。谈谈你对该问题的看法。 28思考题:考试佯谬n逻辑课老师在周末放学时对学生说: 条件a:下周要进行一次考试; 条件b:到底哪天考试,你们在考试之前的任何一天都不能确知。 注:每周上课5天(周一至周五),每天都上一节逻辑课 只有在逻辑课时才可能考试。 一个聪明的学生做出了以下推理: 推论一:周五不可能考试,因为如果周一至周四都不考,那么周四下课时我们就事先知道了明天(周五)一定考试,这不符合条件b。但根据条件a,下周肯定考试,因此考试时间只能是周一至周四的某一天,周五可以排除。29思考题:考试佯谬n推论二:周四也不可能考试,因为如果周一至周三都不考,那么周三放学时我们

17、就事先知道了明天考试,这不符合条件b。但根据条件a,下周肯定考试,因此考试时间只能是周一至周三的某一天,周四可以排除。 推论三:周三也不可能考试,推理过程同上。 推论四:周二也不可能考试,推理过程同上。 推论五:周一也不可能考试,推理过程同上。 结论:下周不可能有考试30思考题:考试佯谬n下周的某一天老师突然考试了,这个聪明同学感到非常意外。问题究竟出在哪里?n练习:将推理过程符号化(不失一般性,考虑简化问题的版本:每周只有两次逻辑课,分别在周一和周四。教师在本周四下课时宣布下周将有一次逻辑考试。)31思考题:考试佯谬n考试佯谬的一个符号化表述n命题常元 P: 考试在下周一的逻辑课上举行 Q:

18、 考试在下周四的逻辑课上举行 K: 学生在考试所在的那天之前知道考试的时间n系统公理: A1: (PQ)(PQ) A2: K A3: PK A4: QK 32思考题:考试佯谬n论证过程:用间接证法证明A1-A4和Q矛盾,推出Q;再用间接证法证明A1-A4和P矛盾,推出P (1)1 Q 附加前提 2(PQ)(PQ) P 3(PQ)(PQ) T (2) 4 PQ T (3) 5 P T (1)(4) 6 PK P 7 K T (5)(6) 8 K P 所以,有Q33思考题:考试佯谬(2) 1 P 附加前提 2(PQ)(PQ) P 3(PQ)(PQ) T (2) 4 PQ T (3) 5 Q T (

19、1)(4) 6 QK P 7 K T (5)(6) 8 K P 所有,有Pn综合(1)和(2),有PQ34思考题:考试佯谬n两个观察:1 学生推理的没有错误 2 教师的两个条件符合事实,故应视为真命题n问题:似乎正确的前提和正确的推理导致了错误的结论(即与教师宣称的真命题矛盾的结论),为什么?n回答:佯谬之所以出现,是因为试图将一个广义哥德尔型命题(可粗略地理解为涉及系统元知识的命题)显式地作为系统公理,来建构系统的完备性。不幸的是,一旦这个原本是直觉真的广义哥德尔型命题在系统中被作为公理显式地表达出来,系统在一致性方面就产生了新的问题。n“There are truths of silenc

20、e, when spoken, no longer true anymore.” Ludwig Wittgenstein35进一步的参考书目n较为通俗的读物: 皇帝新脑,彭罗斯,胡南科技出版社 哥德尔、埃舍尔、巴赫,D. Hofstadter, 商务印书馆n技术性文章/wiki/G%C3%B6dels_incompleteness_theorems 数学家的逻辑36应用例子n搜索引擎的查询扩展(查询结果的精化)n项目背景:QONTEXT (Quantification of quantum entanglements in contextual IA

21、R and towards a non-Kolmogorovian probability model for contextual IAR), MARIE CURIE ACTIONS, International Joint Research Project of The Council of the European Union (FP7) 37形式化一阶谓词演算系统Kn这里讨论一个形式化的一阶谓词演算系统K。通过对K的形式化研究,回答下列问题: 在一阶谓词逻辑(简称为一阶逻辑)中,有效推理的含义? 一阶逻辑的有效推理如何完全形式化地执行? 在此基础上,讨论系统K的元性质。n形式化一阶谓词

22、演算系统Kn符号字母表: x1,x2,x3, 客体变元 a1,a2,a3, 客体常元 A11,A12,A21,A22, 谓词字母,其中Aij表示第j个i元谓词 f11,f12,f21,f22, 函数字母,其中fij表示第j个i元函数38形式化一阶谓词演算系统 (,),, 辅助技术性符号 , 逻辑联结词 量词 n注1:引入了函数符号(即客体函元)。客体常元、客体变元以及函数符号作用于客体常元和变元的结果可以作为谓词的项 K的项的递归定义: 1)客体变元和客体常元是项 2)若fij是函数符号, x1,xi 是项,则 fij(x1,xi)是项 3)所有的项通过有限次使用1)和2)生成39形式化一阶谓

23、词演算系统n问题:函数是一种特殊的关系,而(多元)谓词也可以看作关系。这样,允许函数作为谓词的项,会不会破坏形式谓词演算系统K的一阶性? 例子:任意比x大5的数大于比x大1的数 (x)G(g5(x),g1(x) (x)(y)(z)(G5(y,x)G1(z,x)G(y,z)40形式化一阶谓词演算系统n注3:K中只有两个联结词,为什么?n注4:K中只有一个全称量词,为什么?n原子公式:形如A(t1, t2, , tn)的公式称为K的原子公式,其中t1, t2, , tn是K的项n谓词公式(合式公式): 1) K的每一原子公式是K的谓词公式 2) 若A和B是谓词公式,则(A),(AB)和(xi)A是

24、谓词公式,这里xi是任意客体变元 3) 只有经过有限次应用步骤1)2)所获得的公式才是谓词公式41形式化一阶谓词演算系统n下面将给出K的公理。但是在此之前,需要澄清一个问题:K的公理在何种意义上是真的?为了讨论谓词逻辑的真性问题,需要引入解释的概念。n定义1:K的解释I是指一个对象域集合DI、常元的集合SI,DISI上函数的集合FI和关系的集合RI。n注:K中的客体变元x1,x2,的具体取值在DI中产生;K中的客体常元在SI上中产生;K中的函数和谓词分别由FI和RI产生 K的解释(以及赋值)类似于L的真值指派,K的谓词公式的真性需要基于解释(以及赋值)加以讨论。n例子:初等算术系统42形式化一

25、阶谓词演算系统n例子:(x1)(x3)A21(x1,x3) 当DI是正整数集合,A21(x1,x3)被解释为x1x30时? 当DI是整数集合,A21(x1,x3)被解释为x1x30时?n定义2:K的解释I的一个赋值是从K的项到DISI的函数v,满足: 客体变元取值于DI,客体常元取值于SI 对于K的每个常元:v(xi)=xi* 对于K的每个常元:v(ai)=ai* 对于K的任意函数fij: v(fij(t1,ti)=f*ij(v(t1),v(ti) 这里:xi*,ai* 和f*ij分别是xi,ai和fij在I中的对应物43形式化一阶谓词演算系统n注:上述定义保证了任意复杂函数的赋值可递归确定

26、解释I的赋值v将由对基本客体常元和变元的赋值,以及函数的解释完全确定 赋值起到了进一步的真值指派作用,解释和赋值共同确定了K中所有谓词公式的真值 注意K的赋值与L的赋值的区别n例子: A11(x1) 解释I的DI是整数集合,A11(x1)被解释为x1大于0。对于这个给定的解释I,当赋予x1不同的值时,上式有不同真值。 A31(f11(x1),x1,a1)A11(x1)44形式化一阶谓词演算系统n定义3:两个赋值 u、v是i-等价的,如果对于任意j不等于i,u(xj)=v(xj)n定义4:设A、B、C是K的谓词公式,I是K的一个解释。I的赋值v满足A,如果可由如下四种情形归纳证明v满足A: 1)

27、v满足A(t1,ti) A*(v(t1),v(ti)真 2)v满足B v不满足B 3)v满足BC v满足B或v满足C 4)v满足(xi)B 任何i-等价于v的赋值均满足Bn注:上述定义保证了赋值v相对于任意谓词公式的可满足性可递归判定45形式化一阶谓词演算系统n定义4:K的谓词公式A在解释I下是真的,如果I中每一赋值均满足A; K的谓词公式A在解释I下是假的,如果I中每一赋值均不满足An问题:对于特定解释I: 是否可能存在既不真又不假的谓词公式? 是否可能存在既真又假的谓词公式?n命题1:在K的解释I下,若AB和A真,则B也真n命题2:在K的解释I下,A真当且仅当(xi)A真,xi是任意变元n

28、命题3:在K的解释I下,A真当且仅当(x1)(xk)A真,x1xk是任意变元n注:命题2、3意味着对A中的变元增加全称量词,不改变其真值46形式化一阶谓词演算系统n定义5:K的谓词公式A是重言式,如果A是L的重言式在K中的一个代换实例n例子:X(YX)代换为(xi)A(xj)B(xi)A)n命题4:K的重言式在K的任意解释下都是真的(反之未必成立)n定义6:K的谓词公式A称为封闭的,如果其中无自由变元n命题5:若A是K的封闭谓词公式,I是K的解释,则在I下,或者A为真,或者A为假n注:对于多数重要的系统,特别是数学系统,谓词公式A通常中并不会出现自由变元n定义7:K的谓词公式A是逻辑有效的,如

29、果A在K的每一种解释下都是真的;A是逻辑无效的,如果A在K的每一种解释下都是假的。n回顾:真、假、非真非假、满足、重言、逻辑有效、永假、逻辑无效、解释、赋值、封闭公式47形式化一阶谓词演算系统n公理:设A、B和C是任意谓词公式,则以下为K的公理模式 K1:(A(BA) K2:(A(BC)(AB)(AC) K3:(AB)(BA) K4: (xi)AA),xi不在A中自由出现 注: K4的作用是消除无用的量词,例如: (xi)(xi)A(xi)是否可以应用K4? (xi)A(xj)是否可以应用K4? (xi)A(f(xj)是否可以应用K4? (xi)A(xi)是否可以应用K4? K5: (xi)A

30、(xi)A(t),t是K的项,它对A(xi)中的xi是自由的48形式化一阶谓词演算系统 定义:设A是K的任意谓词公式,项t对A中的xi是自由的,如果xi在A中自由出现,且不在A的任何一个(xj)的辖域中,这里xj是在t中出现的任意客体变元 注:粗略地说,项t对A中的xi是自由的,意味着t可以对A中的xi的每一自由出现做代入,而不会引起与A中量词的相互作用 K5例子:xj对于(xi)A(xi,xj)中的xi是否可用K5? xj对于(xi)(xj)A(xi,xj)中的xi是否可用K5? f(xj)对于(xi)A(xi,xj,xk)中的xi是否可用K5? xi对于(xi)A(xi)中的xi是否可用K

31、5? xi对于(xi)(xi)A(xi)中的xi是否可用K5? 49形式化一阶谓词演算系统注:K4和K5用于去除演绎过程中产生的无用的量词或实现特殊化。例如,对于(xi)A这样的命题,xi可是也可不是A中自由出现的变元。若xi在A中自由出现,可把A记作A(xi),因为xi对A(xi)中的xi是自由的,于是由K5可获得A(xi)。若xi不在A中自由出现,则由K4可获得AK6: (xi)(AB)(A(xi)B),若A不包含变元xi的自由出现50形式化一阶谓词演算系统n命题6:K的公理模式的所有实例都是逻辑有效的nK6: (xi)(AB)(A(xi)B),若A不包含变元xi的自由出现 证明:若(A(

32、xi)B)|v = F,即有A|v = T和(xi)B|v = F,则存在一个与v i-等价的u,有B|u = F;又因A中不包括xi的自由出现,故有A|u = T; 所以u不满足AB 所以u不满足(xi)(AB) 所以v不满足(xi)(AB)51形式化一阶谓词演算系统nK的演绎规则: 1)分离规则,即从A和(AB),可以获得B 2)全称概括规则(UG):由A获得(xi)An问题:全程概括规则是合理的吗?n注:K的公理模式和演绎规则包括了L的公理模式和演绎规则,增加的公理和规则对于涉及量词的演绎是必要的52形式化一阶谓词演算系统n定义8:K中的一个证明是谓词公式的序列A1,A2,An,使得对每

33、一个Ai(1=i1)的证明,而K的所有长度小于n步的定理都是逻辑有效的。n命题9(K的一致性定理):K是一致的,即不存在K的谓词公式A,使得A和A都是K的定理nK的完备性定理(Godel 1930) :若K的谓词公式A是逻辑有效的,则A是K的定理54模型和模态逻辑n系统K要求推理是逻辑有效的,即在任意解释下是均保真的。此要求使K具备逻辑上的可靠性。但系统的可靠性和能力之间常存在内在的冲突。这促使人们重新审视逻辑有效性,尝试放宽对可靠性的限制以获得更强有力的系统。n逻辑有效性被定义为对于任何解释均为真,但通常情况下,并非每个解释都令我们感兴趣,甚至有些解释是不可形式定义的(可形式定义的解释是可数

34、的,而所有可能的解释是不可数的)n例子:若确知日常空间可以由欧几里得几何精确地刻画,是否有必要让应用于日常空间中的形式系统也适用于黎曼几何或罗巴切夫斯基几何世界? 可否扩展K的公理集,保证其具有相对于特定解释的良好性质,并使其功能更强?例如,将欧几里得几何的公理和公设加入系统K。 这就是形式系统的基本思想。55模型和模态逻辑n定义1:设X是K的谓词公式集合,X的一个解释(世界)称为A的模型,如果X中每个谓词公式在此解释下是真的n定义2:若S是一阶系统,S的一个模型是一个解释,在这个解释中,S的每个定理都是真的n定理1:设S是一阶系统,I是使S的每个公理均为真且推理规则保真的解释,则I是S的一个

35、模型n注:定义1给出了公式集的模型的定义;定义2给出了一阶系统的模型的定义。由模型的定义可知,任何一个解释都是一阶谓词系统K的模型 由定理1,一个一阶系统的解释,只需使其所有公理真且推理规则保真,即可成为其模型n思考题:可否建构现实有效系统,即以所有可形式定义解释为模型的系统?56模型和模态逻辑n模态逻辑:关于可能世界(即解释)的逻辑n单世界和多世界 我们的世界是所有可能世界中的最完美者莱布尼茨 量子力学的多宇宙(multiverse)解释Everettn模态词 :读作可能,p指命题p在某个(或某些)解释中为真,即在某个(或某些)可能世界中为真 :读作必然,p指命题p在所用可能的解释中均为真,

36、即在所有可能世界中为真。n模态逻辑对于蕴含悖论的解决方案 例子:A(BA)与SP(S:太阳西升, P:有最大的质数) (A(BA))与(SP) 57模型和模态逻辑n模态(命题)逻辑的重言式集合S是古典命题逻辑重言式集合的超集S,S满足以下条件 1) (pq)(pq)S 2) S在分离规则下封闭:若AS,ABS ,则BS 3) S在代入规则下封闭:若AS,则AS,这里A是A的代入特例 4) S在弱必然化规则下封闭:若A是命题逻辑重言式,则AS 5) S在必然化规则下封闭:若AS,则ASn注:若一个模态逻辑系统满足1)-4),则称它为古典模态逻辑。 若一个模态系统满足1)-3)和5),则称它为正规

37、模态逻辑。 是否有必然化规则(记为N),是正规系统区别于非正规系统的的主要标志。N是说:如果一个公式是在系统内是可证的,则它是逻辑必然的。58模型和模态逻辑n命题模态逻辑系统的实例:S5nS5以代入规则(记为US)和分离规则(记为MP)作为推理规则nS5系统公理 M1(A2):pp M2(T): pp M3(K): (pq)(pq) M4(N):若A可证,则有A M5(4): pp M6(E): pp, pp (Becker假定) M7(A1):所有真值函项重言式59模型和模态逻辑n例子:安瑟伦的上帝存在性本体论证明的Descartes版本 “God could not be so complete if he werent. So he is.” Descartes 扩展表述: 定义上帝为具有所有积极属性者,则上帝必存在 证明:(反证法)假设上帝不存在,则我们可以设想一个God*, God*保有上帝的所有其他积极属性,除了需要额外设想God*是存在的。由于存在性是比虚

温馨提示

  • 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

评论

0/150

提交评论