S5 (模態邏輯)

模态逻辑

邏輯哲學中,S5Clarence Irving LewisCooper Harold Langford 在他們1932年的書《Symbolic Logic》中提議的五個模態邏輯之一。

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

公理化

S5 特徵化為如下公理:

  • K:  ;
  • T:  ,

和如下中的一個:

  • E:  ;
  • 或下列二者:
  • 4:  ,和
  • B:  .

Kripke語義

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

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

應用

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

參見

外部連結