A multimodal logic is a
modal logic that has more than one primitive
modal operator
A modal connective (or modal operator) is a logical connective for modal logic. It is an operator which forms propositions from propositions. In general, a modal operator has the "formal" property of being non- truth-functional in the following se ...
. They find substantial applications in
theoretical computer science
computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory.
It is difficult to circumscribe the ...
.
Overview
A
modal logic with ''n'' primitive unary modal operators
is called an ''n''-modal logic. Given these operators and
negation, one can always add
modal operators defined as
if and only if
.
Perhaps the first substantive example of a two-modal logic is
Arthur Prior
Arthur Norman Prior (4 December 1914 – 6 October 1969), usually cited as A. N. Prior, was a New Zealand–born logician and philosopher. Prior (1957) founded tense logic, now also known as temporal logic, and made important contribution ...
's
tense logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
, with two modalities, F and P, corresponding to "sometime in the future" and "sometime in the past". A logic
with infinitely many modalities is
dynamic logic, introduced by
Vaughan Pratt in 1976 and having a separate modal operator for every
regular expression
A regular expression (shortened as regex or regexp; sometimes referred to as rational expression) is a sequence of characters that specifies a search pattern in text. Usually such patterns are used by string-searching algorithms for "find" ...
. A version of
temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
introduced in 1977 and intended for
program verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
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 In computer science, Hennessy–Milner logic (HML) is a dynamic logic used to specify properties of a labeled transition system (LTS), a structure similar to an automaton. It was introduced in 1980 by Matthew Hennessy and Robin Milner in their pap ...
, 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 Epistemic modal logic is a subfield of modal logic that is concerned with reasoning about knowledge. While epistemology has a long philosophical tradition dating back to Ancient Greece, epistemic logic is a much more recent development with applica ...
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
must be capable of bookkeeping the cognition of each agent, thus
must be indexed on the set of the agents. The motivation is that
should assert "The subject ''i'' has knowledge about
being true". But it can be used also for formalizing "the subject ''i'' believes
". For formalization of meaning based on the
possible world semantics
A possible world is a complete and consistent way the world is or could have been. Possible worlds are widely used as a formal device in logic, philosophy, and linguistics in order to provide a semantics for intensional and modal logic. Their me ...
approach, a
multimodal generalization of Kripke semantics can be used: instead of a single "common"
accessibility relation
An accessibility relation is a relation which plays a key role in assigning truth values to sentences in the relational semantics for modal logic. In relational semantics, a modal formula's truth value at a '' possible world'' w can depend on ...
, there is a series of them indexed on the set of agents.
[Ferenczi 2002: 257]
Notes
References
*
*
*
External links
*
Stanford Encyclopedia of Philosophy:
Modal logic – by
James Garson
James Garson is an American philosopher and logician. He has made significant contributions in the study of modal logic and formal semantics. He is author of ''Modal Logic for Philosophers'' and ''What Logics Mean'' by Cambridge University Pre ...
.
{{logic-stub
Modal logic