S5 (模態邏輯)
模态逻辑
在邏輯和哲學中，S5 是 Clarence Irving Lewis 和 Cooper Harold Langford 在他們1932年的書《Symbolic Logic》中提議的五個模態邏輯之一。
它是正規模態邏輯和最古老的模態邏輯系統之一。
公理化
S5 特徵化為如下公理：
- K: ;
- T: ,
和如下中的一個：
- E: ;
- 或下列二者：
- 4: ，和
- B: .
Kripke語義
依據 Kripke語義，S5 被使用可及關係是等價關係的模型來特徵化：它是自反、傳遞和對稱的。可供選擇的說可及關係是「普遍的」，就是說所有世界都可以從其他世界訪問。
確定 S5 公式的滿足性是 NP-完全問題。難度證明是平凡的，因為 S5 包括命題邏輯。成員關係證明通過展示任何可滿足的公式有一個 Kripke 模型，這裡的世界數目最多線性於這個公式。
應用
S5 是有用的因為他避免了不同種類的量詞的過量重複。例如，在 S5 下，如果說 X 是必然可能必然可能的，那麼就等於說 X 是可能的。無約束的量詞在 S5 下是多餘的。只有最終的「可能的」是重要的。儘管這對於保持命題適度簡短是有用的，它也可能出現反直覺：在 S5 下如果某個事物是可能必然的，則它是必然的。