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語義

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