S5 (模态逻辑)

维基百科,自由的百科全书
跳转至: 导航搜索

逻辑哲学中,S5Clarence Irving LewisCooper 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 下如果某个事物是可能必然的,则它是必然的。

参见[编辑]

外部链接[编辑]