A '''multimodal logic''' is a modal logic that has more than one primitive modal operator. They find substantial applications in theoretical computer science.
==Overview== A modal logic with ''n'' primitive unary modal operators <math>\Box_i, i\in \{1,\ldots, n\}</math> is called an ''n''-modal logic. Given these operators and negation, one can always add <math>\Diamond_i</math> modal operators defined as <math>\Diamond_i P</math> if and only if <math>\lnot \Box_i \lnot P</math>, to give a classical multimodal logic if it is in addition stable under necessitation (or "possibilization", therefore) of both members of provable equivalences.
Perhaps the first substantive example of a two-modal logic is Arthur Prior's tense logic, with two modalities, F and P, corresponding to "sometime in the future" and "sometime in the past". A logic<ref name="TessarisFranconi2009">{{cite book|author1=Sergio Tessaris|author2=Enrico Franconi|author3=Thomas Eiter|title=Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 – September 4, 2009, Tutorial Lectures|url=https://books.google.com/books?id=JdyeU7zs4-AC&pg=PA112|year=2009|publisher=Springer|isbn=978-3-642-03753-5|pages=112}}</ref> with infinitely many modalities is dynamic logic, introduced by Vaughan Pratt in 1976 and having a separate modal operator for every regular expression. A version of temporal logic introduced in 1977 and intended for program verification has two modalities, corresponding to dynamic logic's [''A''] and [''A''*] modalities for a single program ''A'', understood as the whole universe taking one step forwards in time. The term ''multimodal logic'' itself was not introduced until 1980. Another example of a multimodal logic is the Hennessy–Milner logic, itself a fragment of the more expressive modal μ-calculus, which is also a fixed-point logic.
Multimodal logic can be used also to formalize a kind of knowledge representation: the motivation of epistemic logic is allowing several agents (they are regarded as subjects capable of forming beliefs, knowledge); and managing the belief or knowledge of each agent, so that epistemic assertions can be formed about them. The modal operator <math>\Box</math> must be capable of bookkeeping the cognition of each agent, thus <math>\Box_i</math> must be indexed on the set of the agents. The motivation is that <math>\Box_i \alpha</math> should assert "The subject ''i'' has knowledge about <math>\alpha</math> being true". But it can be used also for formalizing "the subject ''i'' believes <math>\alpha</math>". For formalization of meaning based on the possible world semantics approach, a multimodal generalization of Kripke semantics can be used: instead of a single "common" accessibility relation, there is a series of them indexed on the set of agents.{{sfn|Ferenczi|2002|p=257}}
== Notes == {{reflist}}
== References == * {{cite book |last=Ferenczi |first=Miklós |title=Matematikai logika |publisher=Műszaki könyvkiadó |location=Budapest |year=2002 |isbn=963-16-2870-1|language=hu}} * {{cite book|author=Dov M. Gabbay, Agi Kurucz, Frank Wolter, Michael Zakharyaschev|title=Many-dimensional modal logics: theory and applications|year=2003|publisher=Elsevier|isbn=978-0-444-50826-3}} * {{cite book|author1=Walter Carnielli|author1link = Walter Carnielli|author2=Claudio Pizzi|author2link = Claudio E.A. Pizzi|title=Modalities and Multimodalities|year=2008|publisher=Springer|isbn=978-1-4020-8589-5}}
== External links == *{{SEP|logic-modal|Modal Logic|James Garson}}
Category:Modal logic