Modal logic

From New World Encyclopedia
Revision as of 16:42, 13 August 2006 by Tomohiro Hoshi (talk | contribs)

A modal logic was originally designed to describe the logical relations of modal notions. The list of the notions includes metaphysical modalities (necessity, possibilities, etc.), epistemic modalities (knowledge, belief, etc.), temporal modalities (future, past, etc.), deontic modalities (obligation, permission, etc.). Because of the importance of these modal notions, modal logics have attracted many areas in philosophy, including metaphysics, epistemology, etc. However, the interests in modal logics are not limited to such a philosophical investigations. Because of its wide applicability, the general framework of modal logic have been used in various areas including artificial intelligence, database theory, game theory, etc.

The languages of modal logics usually extend preexisting logics, e.g propositional logic, first-order logic etc. with modal operators, which are often symbolized as boxes and diamonds . Semantic structures for the languages of modal logics are relational structures, and the modal languages can be characterized as describing various properties of the relational structures.

Basic Ideas

One major notion that has been considered in modal logics is metaphysical modality. Examples of the modal notion are necessity and possibility. The modal logic that describe the logical relations of statements such as “It is necessary that 2+2=4,” “It is possible that Bigfoot exists” etc. is called alethic modal logic. The main idea of analyzing such modal statements was produced based on the metaphysical view that is usually credited to Leibniz. The idea is to analyze the statement of the form “It is necessary that p” as “In all possible worlds, p is the case,” and “It is possible that p” as “There is some possible world in which p is the case”. In other words, necessity is analyzed as the truth in all possible worlds, and possibility, as the truth in some possible world.

Based on this idea, alethic modal logic clarifies the logical relations of modal statements of the kind in question. For instance, one basic equivalence in alethic modal logic, the one between “It is necessary that p” and “It is not possible that not-p,” is explicated as the equivalence between “In all possible worlds, p is the case” and “There is no possible world in which p is not the case.” Alethic modal logic enables one to see more complex relations of the metaphysical modal statements.

This general idea is modeled in what is called Kripke semantics by relational structures (see below). Because of the wide applicability of the general framework, modal logics have been used, beyond the formalization of metaphysical modality, to represent modal concepts and phenomena. Depending on the purposes of applications, modal logics get specific names. Epistemic logic is designed to describe epistemic notions such as knowledge and belief; temporal logic, temporal structures; deontic logic, deontic notions such as obligation and permission; dynamic logic, actions of computer programs, etc.

Standard Syntax and Semantics of Modal Logics

Sytax

The languages of modal logics extend preexisting logical languages with modal operators, most standardly boxes and diamonds . The intended meanings of boxes and diamonds, say, in alethic modal logic, are respectively “It is necessary that...” and “It is possible that...”.

The language of propositional modal logic, the extension of propositional logic with modal operators, consists of propositional variables (p, q, r, …), Boolean connectives (, &, V, ), and modal operators ( and ). In a standard way, the sentences of propositional modal logic is recursively defined as follows:

 := p (with p a propositional variable) | & | |

The other Boolean connectives are defined as follows, and, based on the observation about the above basic equivalence, “” is defined as the abbreviation of “”.

Other than the language of modal propositional logic, there are various versions of extensions of preexisting languages. Extensions with modal operators are considered for other preexisting languages. For instance, the extension of first-order logic, called modal predicate logic, has been widely considered. Also, extensions are given with modality operators with multiple arities, i.e. modal operators that are followed by a multiple number of formulas rather than by just a single formula as is the case of the propositional modal logic presented above.

Kripke Semantics

The standard semantics of modal languages is Kripke semantics, which is given by relational models. The Kripke semantics of propositional modal logic can be presented as follows. A frame is a tuple <W, R>, where W is an non-empty set and R is a two-place relation on W. W can be thought of as a set of possible world, and R, the accessibility relation between worlds, which represents the possible worlds that are considered at a given world. Given a frame <W, R>, a model is a tuple <W, R, V> where V is a map that assigns to a world a valuation function on propositional variables. Truth is defined with respect to a model M and a world w as follows:

(M, w|=p reads as “p is true at a world p in a model M.)

  • M, w |= p iff V(w)(p)=1 (with p a propositional variable)
  • M, w |= p& q iff M,w|=p and M, w|= q.
  • M, w |= ~p iff M, w|!= p.
  • M, w|= []p iff, for every world w’ such that Rww’, M, w|=p.

The last clause captures the main idea of Leibnizian conception of necessary truth as truth in all possibilities in such a way that “It is necessary that p” is true at a world w in a model M if and only if p is true in all possible worlds accessible from a world w.

A sentence p is valid in a model M if it is true at every possible world in M.A sentence is valid in a frame F if it is valid in every model based on F. A sentence is valid if it is valid in all frames (or every model).

By extending this model-theoretic framework, the semantics for other modal languages are given. In modal predicate logic, a model is designed so that a domain of quantification is associated with each possible world, and in modal logics with modal operator with multiple arities, the accessibility relations of appropriate arities on possible worlds are taken.

Formal rules

There are many modal logics, with many different properties. In many of them the concepts of necessity and possibility satisfy the following de Morganesque relationship:

"It is not necessary that X" is equivalent to "It is possible that not X".
"It is not possible that X" is equivalent to "It is necessary that not X".

However modal logic texts like Hughes and Cresswell's "A New Introduction to Modal Logic" cover some systems where this isn't true.

Modal logic adds to the well formed formulae of propositional logic operators for necessity and possibility. In some notations "necessarily p" is represented using a "box" ( ), and "possibly p" is represented using a "diamond" (). Whatever the notation, the two operators are definable in terms of each other:

  • (necessarily p) is equivalent to (not possible that not-p)
  • (possibly p) is equivalent to (not necessarily not-p)

Hence, the and are called dual operators.

Precisely what axioms must be added to propositional logic to create a usable system of modal logic has been the subject of much debate. One weak system, named K after Saul Kripke, adds only the following to a classical axiomatization of propositional logic:

  • Necessitation Rule: If p is a theorem of K, then so is .
  • Distribution Axiom: If then (this is also known as axiom K)

These rules lack an axiom to go from the necessity of p to p actually being the case, and therefore are usually supplemented with the following "reflexivity" axiom, which yields a system often called T.

  • (If it's necessary that p, then p is the case)

This is a rule of most, but not all modal logic systems. Jay Zeman's book "Modal Logic" covers systems like S1^0 that don't have this rule.

K is a weak modal logic, however. In particular, it leaves it open that a proposition be necessary but only contingently necessary. That is, it is not a theorem of K that if is true then is true, i.e., that necessary truths are necessarily necessary. This may not be a great defect for K, since these seem like awfully strange questions and any attempt to answer them involves us in confusing issues. In any case, different solutions to questions such as these produce different systems of modal logic.

The system most commonly used today is modal logic S5, which robustly answers the questions by adding axioms which make all modal truths necessary: for example, if it's possible that p, then it's necessarily possible that p, and if it's necessary that p it's also necessary that it's necessary. This has been thought by many to be justified on the grounds that it is the system which is obtained when we demand that every possible world is possible relative to every other world. Nevertheless, other systems of modal logic have been formulated, in part, because S5 may not be a good fit for every kind of metaphysical modality of interest to us. (And if so, that may mean that possible worlds talk is not a good fit for these kinds of modality either.)

Development of modal logic

Although Aristotle's logic is almost entirely concerned with the theory of the categorical syllogism, his work also contains some extended arguments on points of modal logic (such as his famous Sea-Battle Argument in De Interpretatione § 9) and their connection with potentialities and with time. Following on his works, the Scholastics developed the groundwork for a rigorous theory of modal logic, mostly within the context of commentary on the logic of statements about essence and accident. Among the medieval writers, some of the most important works on modal logic can be found in the works of William of Ockham and John Duns Scotus.

The founder of formal modal logic is C. I. Lewis, who introduced a system (later called S3) in his monograph A Survey of Symbolic Logic (1918) and (with C. H. Langford) the systems S1-S5 in the book Symbolic Logic (1932). J. C. C. McKinsey used algebraic methods (Boolean algebras with operators) to prove the decidability of Lewis' S2 and S4 in 1941. Saul Kripke devised the relational semantics or possible worlds semantics for modal logics starting in 1959. Vaughan Pratt introduced dynamic logic in 1976. Amir Pnueli proposed the use of temporal logic to formalise the behaviour of continually operating concurrent programs in 1977.

Temporal logic, originated by A. N. Prior in 1957, is closely related to modal logic, as adding modal operators [F] and [P], meaning, respectively, henceforth and hitherto, leads to a system of temporal logic.

Flavours of modal logics include: propositional dynamic logic (PDL), propositional linear temporal logic (PLTL), linear temporal logic (LTL), computational tree logic (CTL), Hennessy-Milner logic, S1-S5, and T.

A note about intensionality of modal logics

Some people argue that modal logics are characterized by semantic intensionality: the truth value of a complex formula cannot be determined by the truth values of its subformulae, and modal operators cannot be formalized by an extensional semantics: both "George W. Bush is President of the United States" and "2 + 2 = 4" are true, yet "Necessarily, George W. Bush is President of the United States" is false, while "Necessarily, 2 + 2 = 4" is true.

Actually, this claim is not correct, since we can give the semantics of a modal logic by structural induction, if we use stateful models, also called coalgebraic models. For example, we can consider the following very simple modal logic syntax:

We can derive dual connectives using the basic ones:

The truth value of a formula is defined over models that are not sets, but transition systems.

A transition system is a pair where is a set and .

The interpretation of the logic over the state , given a transition system , is a relation , where is read "the state s satisfies the formula F", given by structural induction as follows:

If we view a transition system as a set of states and a set of transitions from a state to another, the modal formula , which is called the "next" modality, is read as "in my possible next states, there is one that satisfies F".

This logic is too simple for pratical uses; more complicated logics can have more complicated models (an example being Kripke frames), however the definition of the semantics is usually given by structural induction over states.

References
ISBN links support NWE through referral fees

  • Patrick Blackburn, Maarten de Rijke, and Yde Venema (2001) "Modal Logic". Cambridge University Press.
  • Brian F. Chellas (1980) "Modal Logic: an introduction". Cambridge University Press.
  • M. Fitting and R.L. Mendelsohn (1998) First Order Modal Logic. Kluwer Academic Publishers.
  • James Garson (2003) Modal logic. Entry in the Stanford Encyclopedia of Philosophy.
  • Rod Girlie (2000) Modal Logics and Philosophy. Acumen (UK). The proof theory employs refutation trees (semantic tableaux). A good introduction to the varied interpretations of modal logic.
  • Robert Goldblatt (1992) "Logics of Time and Computation", CSLI Lecture Notes No. 7, Centre for the Study of Language and Information, Stanford University, 2nd ed. (distributed by University of Chicago Press).
  • Robert Goldblatt (1993) "Mathematics of Modality", CSLI Lecture Notes No. 43, Centre for the Study of Language and Information, Stanford University. (distributed by University of Chicago Press).
  • G.E. Hughes and M.J. Cresswell (1968) An Introduction to Modal Logic, Methuen.
  • G.E. Hughes and M.J. Cresswell (1984) A Companion to Modal Logic, Medhuen.
  • G.E. Hughes and M.J. Cresswell (1996) A New Introduction to Modal Logic, Routledge.
  • E.J. Lemmon (with Dana Scott), 1977, An Introduction to Modal Logic, American Philosophical Quarterly Monograph Series, no. 11 (ed. by Krister Segerberg), Basil Blackwell, Oxford.
  • J. Jay Zeeman (1973) Modal Logic. D. Reidel Publishing Company.

See also

  • Possible worlds
  • De dicto and de re
  • Hybrid logic
  • Interior algebra
  • Interpretability logic
  • Provability logic
  • Kripke semantics

External links

Acknowledgements

This article contains some material originally from the Free On-line Dictionary of Computing which is used with permission under the GFDL.

ar:منطق طوري de:Modallogik es:Lógica modal fr:Logique modale he:לוגיקה מודלית io:Modala logiko nl:Modale logica ja:様相論理学 zh:模态逻辑

Credits

New World Encyclopedia writers and editors rewrote and completed the Wikipedia article in accordance with New World Encyclopedia standards. This article abides by terms of the Creative Commons CC-by-sa 3.0 License (CC-by-sa), which may be used and disseminated with proper attribution. Credit is due under the terms of this license that can reference both the New World Encyclopedia contributors and the selfless volunteer contributors of the Wikimedia Foundation. To cite this article click here for a list of acceptable citing formats.The history of earlier contributions by wikipedians is accessible to researchers here:

The history of this article since it was imported to New World Encyclopedia:

Note: Some restrictions may apply to use of individual images which are separately licensed.