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 下如果某個事物是可能必然的,則它是必然的。