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. It is formed with propositional calculus formulas and tautologies, and inference apparatus with substitution and modus ponens, but extending the syntax with the modal operator necessarily ◻ {\displaystyle \Box } and its dual possibly ◊ {\displaystyle \Diamond } .
The axioms of S5 The following makes use of the modal operators ◻ {\displaystyle \Box } ("necessarily") and ◊ {\displaystyle \Diamond } ("possibly"). S5 is characterized by the axioms:
K: ◻ ( A → B ) → ( ◻ A → ◻ B ) {\displaystyle \Box (A\to B)\to (\Box A\to \Box B)} ; T: ◻ A → A {\displaystyle \Box A\to A} , and either:
5: ◊ A → ◻ ◊ A {\displaystyle \Diamond A\to \Box \Diamond A} ; or both of the following: 4: ◻ A → ◻ ◻ A {\displaystyle \Box A\to \Box \Box A} , and B: A → ◻ ◊ A {\displaystyle A\to \Box \Diamond A} . The (5) axiom restricts the accessibility relation R {\displaystyle R} of the Kripke frame to be Euclidean, i.e. ( w R v ∧ w R u ) ⟹ v R u {\displaystyle (wRv\land wRu)\implies vRu} , thereby conflating necessity with possibility under idempotence.
Kripke semantics In terms of Kripke semantics, S5 is characterized by frames where the accessibility relation is an equivalence relation: it is reflexive, transitive, and symmetric. 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.
… excerpt ends here. Continue reading the full article.
