Web Analytics
Privacy Policy Cookie Policy Terms and Conditions 模态逻辑 - Wikipedia

模态逻辑

维基百科,自由的百科全书

模态逻辑,或者叫(不很常见)内涵逻辑,是处理用模态如可能或许可以一定必然等限定的句子的逻辑。模态逻辑可以用语义的内涵来描述其特征: 复杂公式的真值不能由子公式的真值来决定的。允许这种决定性的逻辑是外延性的,经典逻辑就是外延性的例子。模态算子不能使用外延语义来形式化: "乔治·布什是美国总统" 和 "2 + 2 = 4" 是真的,但是 "乔治·布什必然是美国总统" 是假的,而"2 + 2 = 4 是必然的" 是真的。

形式模态逻辑使用模态判决算子表示模态。基本的模态算子\Box\Diamond。(有时分别使用 "L" 和 "M")。它们的意义依赖于特定的模态逻辑,但它们总是以相互定义的方式来定义:

\Diamond p = \lnot\, \Box\, \lnot\, p.

真势模态逻辑(就是说必然性和可能性的逻辑)中 \Box 表示必然性,而 \Diamond 表示可能性。所以 Jones 有兄弟是可能的,当且仅当 Jones 有兄弟是非必然的

句子被认定为

  • 可能的 如果它可能为真(不管实际上是真是假);
  • 必然的 如果它不可能为假;
  • 偶然的 如果它不是必然为真,就是说,可能为真可能为假。偶然的真理是实际上为真,但可能曾经不是的真理。

目录

[编辑] 形而上学和其他模态

[编辑] 真势和认识

模态逻辑最经常用来谈论所谓的真势模态: "...是必然的" 或者 "....是可能的" ,这些模态(包括形而上学模态逻辑模态)最容易混淆于认识模态(来自希腊语 episteme, 知识): "...确实是真的" 和 "...(对给定的可获得的信息)或许是真的"。在普通的话语中这两种模态经常用类似的词来表达;下列对比可能有所帮助:

一个人 Jones 可以合理的同时说出: (1) "我确信 Bigfoot 不可能存在",还有(2) "Bigfoot 存在的确是可能的"。Jones 通过(1)表达的意思是,对于给定的所有可获得的信息,Bigfoot 存在与否是没有疑问的。这是一个认识上的断言。通过(2)表达的意思是这个事物可能曾是其它样子的。他的意思不是 "就我所知而言,Bigfoot 可能存在" 。(所以这不矛盾于(1))。而是,他做了一个形而上学上的断定,即使他不知道,Bigfoot 存在仍是可能的

在其他方面,Jones 可以说 (3) "哥德巴赫猜想可能为真,并也可能为假,还有(4) 如果它真的,则它必然是真的,而不可能是假的。" 这里 Jones 的意思是,就他所知而言,它为真为假都是在认识上可能的(哥德巴赫猜想仍未被证明是真还是假)。但是如果这么一个证明(至今仍未发现),则哥德巴赫猜想为假在逻辑上是不可能的 -- 不会有一组数违背它。逻辑上的可能性是一种真势(alethic)可能性;(4)做了对这个数学论断已经为假是否可能的一个断言,而(3)只做了对就 Jones 所知而言这个论断被证实为假是否可能的一个断言,所以 Jones 还是不自相矛盾。

认识上的可能性还以一种非形而上学的方式关注真实世界。形而上学的可能性以可能曾是的方式关注世界,而认识上的可能性以(就我所知而言)可能正是的方式关注世界。比如,我想知道在离开前是否要带把伞。如果你告诉我 "外面可能在下雨" -- 在一种认识上可能的意义上--那么这会影响我是否带伞的决定。但是如果你告诉我 "外面下雨是可能的" -- 在一种形而上学上可能的意义上--那么我从这种大道理中没有得到任何启示。

大量的哲学文献关心真势而非认识模态。(实际上,其中大多数关心一种最广泛的真势模态,就是逻辑可能性)。这不是说真势可能性比我们日常用的认识可能性更重要(考虑上面决定是否带伞的例子)。只是说在哲学研究中的优先权不是日常生活中的重要性带来的。

[编辑] 道义和时间

言语中有一些类似的模式,尽管不大可能与真势模态混淆但仍密切的相关。其一是有关时间的谈论。明天可能会下雨,但也可能不下好像是合理的;在另一方面,如果昨天下雨了,如果实际上已经下了,则说"昨天可能没有下雨"就不是完全正确的。过去好像"固定的"或必然的,而将来在某种程度上不是。很多哲学家和逻辑学家认为这种推理不是很好;但是我们经常以这种方式谈话,所以最好有一种逻辑能捕获它的结构。类似的有关道德的谈论,或者说义务和规范一般好像也有模态结构。在 "你必须这么做" 和 "你可以这么做" 之间的区别看起来很像在"这是必然的和这是可能的"之间的区别。这种逻辑叫做道义逻辑,道义来自希腊语 "duty"。

值得注意的是,模态逻辑可以开发出实现多数这种方言;它们有公共逻辑机构的事实(使用"内涵"或非真值泛函的句子算子)使它们都是同一个东西的变体。认识逻辑被证实捕获于系统"S4";道义逻辑捕获于系统"D",时间逻辑捕获于"t"(小写的),而真势逻辑被证实为"S5"

[编辑] 模态逻辑的释义

在模态逻辑的最常见解释中,你要考虑"所有逻辑上可能的世界"。如果一个陈述在所有可能世界中是真的,则它是必然的真理。如果一个陈述碰巧在我们的世界中是真的,但不是在所有可能世界中是真的,则它是偶然的真理。在某些(不是必须在我们自己的)可能世界中是真的陈述叫做可能的真理。

这种"可能世界"是否是解释模态逻辑的最佳方式,怎样在文字上接受这种方言,是形而上学的鲜活的问题。例如,可能世界的方言可以把关于 Bigfoot 的断言翻译为"有某个可能世界,在其中 Bigfoot 存在"。要主张 Bigfoot 的存在性是可能的,但不是现实的,你可以说"有某个可能世界,在其中 Bigfoot 存在;但是在现实世界中,Bigfoot 不存在"。但是对使模态断言对我们负责的那个东西是什么仍是不清楚的。我们真的要宣称可能世界的存在性吗?它在每一点都同我们的现实世界一样真实,却惟独不是现实的。David Lewis 强硬的说就是这样,可能世界同我们自己的世界一样真实。这种立场叫做"模态现实主义"。不足为奇的,多数哲学家不愿意接受这种特别的学说,在搜寻一种可替代的方式来释义我们的模态断言所蕴含的本体论承诺。

[编辑] 形式化规则

有很多有不同性质的模态逻辑。在其中很多必然性和可能性的概念满足下列 de Morgan 定律的联系:

"X非必然的" 等价于 "非 X可能的"。
"X非可能的" 等价于 "非 X必然的"。

尽管模态逻辑教科书比如 Hughes 和 Cresswell 的 "A New Introduction to Modal Logic" 覆盖了这个定律不成立的一些系统。

模态逻辑向命题逻辑合式公式增加上必然性和偶然性。在一些记号中 "必然的 p" 使用"方块"( \Box p)表示,而"可能的 p" 使用"菱形"(\Diamond p)表示。无论是什么样的记号,两个算子是以相互定义的方式定义的:

  • \Box p (必然的 p) 等价于 \neg \Diamond \neg p (非可能的非-p)
  • \Diamond p (可能的 p) 等价于 \neg \Box \neg p (非必然的非-p)

因此,\Box\Diamond 叫做对偶算子。

要建立模态逻辑的可用系统,必须向命题逻辑的增加什么公理是非常有争议的主题。得名于 Saul Kripke 的 K,只向经典命题逻辑公理体系增加了如下规则:

  • 必然性规则: 如果 p 是 K 的定理,则 \Box p 也是。
  • 分配律公理: 如果 \Box (p \rightarrow q)(\Box p \rightarrow \Box q) (这也叫做公理 K)

这些规则缺乏从 p 的必然性到 p 的实际情况的公理,所以通常要补充上下列"自反性"公理,这就生成经常叫做 T 的一个系统。

  • \Box p \rightarrow p (如果 p 是必然的,则 p 是事实)

这是多数但不是全部模态逻辑系统的规则。Jay Zeman 的书 "Modal Logic" 覆盖了没有这个规则的系统如 S1^0。

但 K 是一个弱模态逻辑。特别是留下了一个公开的问题,命题是必然的但只偶尔是必然的。如果 \Box p 为真则 \Box \Box p 为真不是 K 的定理,它是说,必然的真理必然是必然的。这可能不是 K 的大缺陷,因为这些好像是十分奇怪的问题,而试图解答它们的任何尝试都把我们卷入混乱的难题中。无论如何,对这种问题的不同解决方式生成了不同的模态逻辑系统。

今天最常见的系统是模态逻辑 S5,它通过增加使所有模态真理是必然的公理来粗壮的解答了这个问题: 例如,如果 p 是可能的,则 p 必然是可能的,如果 p 是必然的,则它必然是必然的。很多人认为它正当的根据是,它是在我们需要每个可能的世界相对于每个其他世界都是可能的时候所获得的系统。不过,模态逻辑的其他系统已经被公式化了,部分的因为 S5 不能很好的适合我们感兴趣的所有种类的形而上学模态。(若此则意味着可能的世界的谈论不能很好的适合这些种类的模态)。

[编辑] 模态逻辑的发展

尽管亚里士多德的逻辑几乎全部都关注直言三段论的理论,他的著作还包含在模态逻辑要点上的一些延伸讨论(比如他著名的在解释篇 § 9 中海战悖论),并且它们与潜在性和时间有关连。遵从他的著作,经院学者为模态逻辑的严格理论开发出了根基,大多在关于本质和偶然的陈述的逻辑的注释的上下文中。在中世纪的作家中,在 William of Ockham 和 John Duns Scotus 的著作中找到了关于模态逻辑的一些最重要的工作。

形式模态逻辑的缔造者是 C. I. Lewis,他在专著 A Survey of Symbolic Logic (1918) 中介入了一个系统(后来叫做 S3),并(同 C. H. Langford 一起)在书 Symbolic Logic (1932)中介入了系统 S1-S5。J. C. C. McKinsey 在 1941 年使用代数方法(带有算子的布尔代数)来证明 Lewis 的 S2 和 S4 的可判定性。Saul Kripke 从 1959 年开始为模态逻辑设计了关系语义可能世界语义。Vaughan Pratt 在 1976 年介入了动态逻辑。Amir Pnueli 在 1977 年提出使用时态逻辑来公式化频繁操作并发程序的行为。

时间逻辑,在 1957 年由 A. N. Prior 发明,与模态逻辑有密切的关联,因为增加了模态算子 [F] 和 [P],分别意味着今后至今,导致了时间逻辑的一个系统。

模态逻辑的风味包括: 命题动态逻辑(PDL),命题线性时间逻辑(PLTL),线性时间逻辑(LTL),计算树逻辑(CTL), Hennessy-Milner 逻辑,S1-S5 和 T。

[编辑] 引用

  • M. Fitting and R.L. Mendelsohn (1998) First Order Modal Logic. Kluwer Academic Publishers.
  • James Garson (2003) Modal logic. Entry in the Stanford Encyclopedia of Philosophy.
  • Rod Girle (2000) Modal Logics and Philosophy. Acumen (UK). The proof theory employs refutation trees (semantic tableaux). A good introduction to the varied interpretations of modal logic.
  • Robert Goldblatt (1992) "Logics of Time and Computation", CSLI Lecture Notes No. 7, Centre for the Study of Language and Information, Stanford University, 2nd ed. (distributed by University of Chicago Press).
  • Robert Goldblatt (1993) "Mathematics of Modality", CSLI Lecture Notes No. 43, Centre for the Study of Language and Information, Stanford University. (distributed by University of Chicago Press).
  • G.E. Hughes and M.J. Cresswell (1968) An Introduction to Modal Logic, Methuen.
  • G.E. Hughes and M.J. Cresswell (1984) A Companion to Modal Logic, Medhuen.
  • G.E. Hughes and M.J. Cresswell (1996) A New Introduction to Modal Logic, Routledge.
  • E.J. Lemmon (with Dana Scott), 1977, An Introduction to Modal Logic, American Philosophical Quarterly Monograph Series, no. 11 (ed. by Krister Segerberg), Basil Blackwell, Oxford.
  • J. Jay Zeeman (1973) Modal Logic. D. Reidel Publishing Company.

[编辑] 参见

[编辑] 外部链接

[编辑] 致谢

本文包含最初来自Free On-line Dictionary of Computing的一些材料,经过授权在 GFDL 下。

THIS WEB:

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - be - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - closed_zh_tw - co - cr - cs - csb - cu - cv - cy - da - de - diq - dv - dz - ee - el - eml - en - eo - es - et - eu - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gd - gl - glk - gn - got - gu - gv - ha - haw - he - hi - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mg - mh - mi - mk - ml - mn - mo - mr - ms - mt - mus - my - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - rm - rmy - rn - ro - roa_rup - roa_tara - ru - ru_sib - rw - sa - sc - scn - sco - sd - se - searchcom - sg - sh - si - simple - sk - sl - sm - sn - so - sq - sr - ss - st - su - sv - sw - ta - te - test - tet - tg - th - ti - tk - tl - tlh - tn - to - tokipona - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu

Static Wikipedia 2008 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Static Wikipedia 2007:

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - be - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - closed_zh_tw - co - cr - cs - csb - cu - cv - cy - da - de - diq - dv - dz - ee - el - eml - en - eo - es - et - eu - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gd - gl - glk - gn - got - gu - gv - ha - haw - he - hi - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mg - mh - mi - mk - ml - mn - mo - mr - ms - mt - mus - my - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - rm - rmy - rn - ro - roa_rup - roa_tara - ru - ru_sib - rw - sa - sc - scn - sco - sd - se - searchcom - sg - sh - si - simple - sk - sl - sm - sn - so - sq - sr - ss - st - su - sv - sw - ta - te - test - tet - tg - th - ti - tk - tl - tlh - tn - to - tokipona - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu

Static Wikipedia 2006:

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - be - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - closed_zh_tw - co - cr - cs - csb - cu - cv - cy - da - de - diq - dv - dz - ee - el - eml - en - eo - es - et - eu - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gd - gl - glk - gn - got - gu - gv - ha - haw - he - hi - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mg - mh - mi - mk - ml - mn - mo - mr - ms - mt - mus - my - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - rm - rmy - rn - ro - roa_rup - roa_tara - ru - ru_sib - rw - sa - sc - scn - sco - sd - se - searchcom - sg - sh - si - simple - sk - sl - sm - sn - so - sq - sr - ss - st - su - sv - sw - ta - te - test - tet - tg - th - ti - tk - tl - tlh - tn - to - tokipona - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu