形式化数理逻辑-课件.ppt

* 模型和模态逻辑 “Logic is not the end of wisdom, it is the beginning…” anonymous * 思考题：考试佯谬 考试佯谬的一个符号化表述 命题常元 P: 考试在下周一的逻辑课上举行 Q: 考试在下周四的逻辑课上举行 K： 学生在考试所在的那天之前知道考试的时间 系统公理： A1： （P?┐Q）?（┐P?Q） A2： ┐K A3： ┐P→K A4： ┐Q→K * 思考题：考试佯谬 论证过程：用间接证法证明A1-A4和Q矛盾，推出┐Q；再用间接证法证明A1-A4和P矛盾，推出┐P （1）1 Q 附加前提 2（P?┐Q）?（┐P?Q） P 3（P?Q）?（┐P?┐Q） T (2) 4 ┐P?┐Q T (3) 5 ┐P T (1)(4) 6 ┐P→K P 7 K T (5)(6) 8 ┐K P 所以，有┐Q * 思考题：考试佯谬 (2) 1 P 附加前提 2（P?┐Q）?（┐P?Q） P 3（P?Q）?（┐P?┐Q） T (2) 4 ┐P?┐Q T (3) 5 ┐Q T (1)(4) 6 ┐Q→K P 7 K T (5)(6) 8 ┐K P 所有，有┐P 综合（1）和（2），有┐P?┐Q * 思考题：考试佯谬 两个观察：1 学生推理的没有错误 2 教师的两个条件符合事实，故应视为真命题 问题：似乎正确的前提和正确的推理导致了错误的结论（即与教师宣称的真命题矛盾的结论），为什么？ 回答：佯谬之所以出现，是因为试图将一个广义哥德尔型命题（可粗略地理解为涉及系统元知识的命题）显式地作为系统公理，来建构系统的完备性。不幸的是，一旦这个原本是直觉真的广义哥德尔型命题在系统中被作为公理显式地表达出来，系统在一致性方面就产生了新的问题。 “There are truths of silence, when spoken, no longer true anymore.” Ludwig Wittgenstein * 进一步的参考书目 较为通俗的读物： 《皇帝新脑》，彭罗斯，胡南科技出版社 《哥德尔、埃舍尔、巴赫》，D. Hofstadter， 商务印书馆 技术性文章/wiki/G%C3%B6del‘s_incompleteness_theorems 《数学家的逻辑》 * 应用例子 有哪些信誉好的足球投注网站引擎的查询扩展（查询结果的精化） 项目背景：QONTEXT (Quantification of quantum entanglements in contextual IAR 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) * 形式化一阶谓词演算系统K 这里讨论一个形式化的一