S5 (modal logic)

From Wikipedia, the free encyclopedia

In logic and philosophy, S5 is one of five systems of modal logic proposed by Clarence Irving Lewis and Cooper Harold Langford in their 1932 book Symbolic Logic. It is a normal modal logic, and one of the oldest systems of modal logic of any kind.

Contents

[edit] Axiomatics

S5 is characterized by the axioms:

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

and either:

  • 5: \Diamond A\to \Box\Diamond A;
  • or both of the following:
  • 4: \Box A\to\Box\Box A, and
  • B: A\to\Box\Diamond A.

[edit] Kripke semantics

In terms of Kripke semantics, S5 is characterized by models where the accessibility relation is an equivalence relation: it is reflexive, transitive, and symmetric. Alternatively, the accessibility relation is "universal", that is, every world is accessible from any other.

Determining the satisfiability of an S5 formula is an NP-complete problem. The hardness proof is trivial, as S5 includes the propositional logic. Membership is proved by showing that any satisfiable formula has a Kripke model where the number of worlds is at most linear in the size of the formula.

[edit] Applications

S5 is useful because it avoids superfluous iteration of qualifiers of different kinds. For example, under S5, if X is necessarily, possibly, necessarily possible, then X is possible. The unbolded qualifiers are superfluous under S5. Only the final "possible" is important. While this is useful for keeping propositions reasonably short, it also might appear counter-intuitive in that, under S5, if something is possibly necessary, then it is necessary.

[edit] See also

[edit] External links

Languages