查看“︁S5 (模态逻辑)”︁的源代码

在[[逻辑]]和[[哲学]]中，'''S5''' 是 [[Clarence Irving Lewis]] 和 [[Cooper Harold Langford]] 在他们1932年的书《Symbolic Logic》中提议的五个[[模态逻辑]]之一。

它是[[正规模态逻辑]]和最古老的模态逻辑系统之一。

== 公理化 ==
'''S5''' 特征化为如下公理：
*'''K''': <math>\Box(A\to B)\to(\Box A\to\Box B)</math>;
*'''T''': <math>\Box A \to A</math>,

和如下中的一个：

* '''E''': <math>\Diamond A\to \Box\Diamond A</math>;
* 或下列二者：
:* '''4''': <math>\Box A\to\Box\Box A</math>，和
:* '''B''': <math>A\to\Box\Diamond A</math>.

== Kripke语义 ==
依据 [[Kripke语义]]，'''S5''' 被使用可及关系是[[等价关系]]的模型来特征化：它是[[自反关系|自反]]、[[传递关系|传递]]和[[对称关系|对称]]的。可供选择的说可及关系是“普遍的”，就是说所有世界都可以从其他世界访问。

确定 '''S5''' 公式的满足性是 [[NP-完全]]问题。难度证明是平凡的，因为 '''S5''' 包括[[命题逻辑]]。成员关系证明通过展示任何可满足的公式有一个 Kripke 模型，这里的世界数目最多线性于这个公式。

== 应用 ==
'''S5''' 是有用的因为他避免了不同种类的量词的过量重复。例如，在 '''S5''' 下，如果说 ''X'' 是必然可能必然可能的，那么就等于说 ''X'' 是可能的。无约束的量词在 '''S5''' 下是多余的。只有最终的“可能的”是重要的。尽管这对于保持命题适度简短是有用的，它也可能出现反直觉：在 '''S5''' 下如果某个事物是可能必然的，则它是必然的。

== 参见 ==
* [[模态逻辑]]
* [[正规模态逻辑]]
* [[Kripke语义]]
* [[哥德爾本體論證明]]

== 外部链接 ==
* https://web.archive.org/web/20070626014132/http://home.utah.edu/~nahaj/logic/structures/systems/s5.html
* https://web.archive.org/web/20050113090442/http://www.columbia.edu/~av72/modallogic/LectureNotes/ModalLogic06.pdf

[[Category:模态逻辑]]