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

参见

编辑

外部链接

编辑