Axiom S5

Axiom (5) extends the modal logic M, to form the modal logic S5. Which in turn, consists of modal logic called K, in honour of Saul Kripke. It is the most basic modal logic, 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 \Box and its dual possibly \Diamond. To deal with the new formulas of the form \Box \varphi and \Diamond \varphi, the following rules complement the inference apparatus of K:

the distribution axiom \Box(\varphi \implies \psi) \implies (\Box \varphi \implies \Box \psi)
necessitation rule \frac{\varphi}{\ \Box \varphi\ }

The logic M is K plus the axiom:

(M)  \Box \varphi \implies \varphi

which restricts the accessibility relation of the Kripke frame to be reflexive.

The modal logic S5 is obtained by adding the axiom:

(5) \Diamond \varphi\implies\Box\Diamond \varphi

The (5) axiom restricts the accessibility relation R, of the Kripke frame to be euclidean, i.e. (wRv \land wRu) \implies vRu .

In S5 formulas of the form OOO\ldots\Box\varphi can be simplified to \Box\varphi where OOO\ldots is formed by any (finite) number of either \Box or \Diamond operators or both. The same stands for formulas of the form OOO\ldots\Diamond\varphi which can be simplified to \Diamond\varphi.

References

External links

This article is issued from Wikipedia - version of the Wednesday, September 17, 2014. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.