S5 (模態邏輯)

在邏輯和哲學中，S5 是 Clarence Irving Lewis 和 Cooper Harold Langford 在他們1932年的書《Symbolic Logic》中提議的五個模態邏輯之一。

它是正規模態邏輯和最古老的模態邏輯系統之一。

公理化

S5 特徵化為如下公理：

K: $\Box (A\to B)\to (\Box A\to \Box B)$ ;
T: $\Box A\to A$ ,

和如下中的一個：

E: $\Diamond A\to \Box \Diamond A$ ;
或下列二者：

4: $\Box A\to \Box \Box A$ ，和
B: $A\to \Box \Diamond A$ .

Kripke語義

依據 Kripke語義，S5 被使用可及關係是等價關係的模型來特徵化：它是自反、傳遞和對稱的。可供選擇的說可及關係是「普遍的」，就是說所有世界都可以從其他世界訪問。

確定 S5 公式的滿足性是 NP-完全問題。難度證明是平凡的，因為 S5 包括命題邏輯。成員關係證明通過展示任何可滿足的公式有一個 Kripke 模型，這裡的世界數目最多線性於這個公式。

應用

S5 是有用的因為他避免了不同種類的量詞的過量重複。例如，在 S5 下，如果說 X 是必然可能必然可能的，那麼就等於說 X 是可能的。無約束的量詞在 S5 下是多餘的。只有最終的「可能的」是重要的。儘管這對於保持命題適度簡短是有用的，它也可能出現反直覺：在 S5 下如果某個事物是可能必然的，則它是必然的。

參見

外部連結