S5 (模态逻辑)

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

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

S5 特征化为如下公理：

• K: ${\displaystyle \Box (A\to B)\to (\Box A\to \Box B)}$;
• T: ${\displaystyle \Box A\to A}$,

和如下中的一个：

• E: ${\displaystyle \Diamond A\to \Box \Diamond A}$;
• 或下列二者：

• 4: ${\displaystyle \Box A\to \Box \Box A}$，和
• B: ${\displaystyle A\to \Box \Diamond A}$.

依据 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