View source for Modal logic

{{redirect|System T|the system used with the programming language|Typed lambda calculus}}
A '''modal logic''' is any system of [[formal logic]] that attempts to deal with ''[[Linguistic modality|modalities]]''.  Traditionally, there are three 'modes' or 'moods' or 'modalities' of the [[copula]] ''to be'', namely, ''[[Logical possibility|possibility]]'', ''[[probability]]'', and ''[[necessity]]''. Logics for dealing with a number of related terms, such as ''eventually'', ''formerly'', ''can'', ''could'', ''might'', ''may'', ''must'', are by extension also called modal logics, since it turns out that these can be treated in similar ways.

A formal modal logic represents modalities using [[modal operator]]s. For example, "Jones's murder was a possibility", "Jones was possibly murdered", and "It is possible that Jones was murdered" all contain the notion of possibility. In a modal logic this is represented as an operator, ''Possibly'', attaching to the sentence ''Jones was murdered''.

The basic unary (1-place) modal operators are usually written <math>\Box</math> (or ''L'') for ''Necessarily'' and <math>\Diamond</math> (or ''M'') for ''Possibly''. In a [[classical modal logic]], each can be expressed by the other and [[negation]]:

:<math>\Diamond P \leftrightarrow \lnot \Box \lnot P;</math>
:<math>\Box P \leftrightarrow \lnot \Diamond \lnot P.</math>

Thus it is ''possible'' that Jones was murdered if and only if it is ''not necessary'' that Jones was ''not'' murdered. For the standard formal semantics of the basic modal language, see [[Kripke semantics]].

==Brief history==

The founder of modern formal logic, [[Gottlob Frege]], doubted that modal logic was viable, and he discounted it.  Two of his well-known readers, [[Rudolph Carnap]] and [[Kurt Gödel]] (1933) broke with [[Frege]] on this topic, and chose to pursue the mathematical structure of a logic that deals with the three classic modes.  In 1937, [[Robert Feyes]], following Gödel, proposed System T modal logic.  In 1951, [[Georg Henrik von Wright]] proposed [[System M]], which is an elaboration on System T.   Also in the 1950s, [[C.I. Lewis]] built upon System M to construct his well-known modal systems S1, S2, S3, S4 and S5.  By 1965 [[Saul Kripke]] solidly established [[System K]], which is the form of modal logic that most scholars use today.

==Alethic modalities==
Modalities of necessity and possibility are called ''alethic'' modalities.  They are also sometimes called ''special'' modalities, from the [[Latin]] ''species''. Modal logic was first developed to deal with these concepts, and only afterward was extended to others.  For this reason, or perhaps for their familiarity and simplicity, necessity and possibility are often casually treated as ''the'' subject matter of modal logic. Moreover it is easier to make sense of relativizing necessity, e.g. to legal, physical, nomological, epistemic, and so on, than it is to make sense of relativizing other notions.

A proposition is said to be 
*'''possible''' if it is ''not necessarily false'' (regardless of whether it actually is true or false);
*'''necessary''' if it is ''not possibly false'';
*'''contingent''' if it is ''possibly true'' and ''possibly false''.

Clearly if we wish the definitions of these notions to be non-circular, we need to take either possibility or necessity as primitive, or further analyze these notions in terms of others that include neither possibility nor necessity, and which are themselves non-circularly defined.

===Physical possibility===

Something is physically possible if it is permitted by the [[physical law|laws of nature]].  For example, it is possible for there to be an [[atom]] with an [[atomic number]] of 150, though there may not in fact be one.  On the other hand, it is not possible, in this sense, for there to be an element whose nucleus contains cheese.  While it is logically possible to accelerate beyond the [[speed of light]], it is not, according to modern science, physically possible for objects with mass.

===Metaphysical possibility===

[[Philosophers]] ponder the properties objects have independently of those dictated by scientific laws.  For example, it might be metaphysically necessary, as some have thought, that all thinking beings have bodies and can experience the passage of [[time]], or that [[God]] exists (or does not exist).  [[Saul Kripke]] has argued that every person necessarily has the parents they do have: anyone with different parents wouldn't be the same person.

Metaphysical possibility is generally thought to be stronger than bare logical possibility (i.e., fewer things are metaphysically possible than are logically possible).  Its exact relation to physical possibility is a matter of some dispute.  Philosophers also disagree over whether metaphysical truths are necessary merely "by definition", or whether they reflect some underlying deep facts about the world, or something else entirely.

===Confusion with epistemic modalities===

Alethic modalities and epistemic modalities (see below) are often expressed in English using the same words.  Thus, "It is possible that bigfoot exists" might mean either "It would be possible for such a creature as a bigfoot to exist", or (more likely), "For all I know, bigfoot may exist" (It's compatible with what I know that bigfoot exists).

In the former case, the speaker might know that there are not any bigfoots, but is saying that (unlike round squares), there could be some – the existence of bigfoot is not impossible.  In the latter case he is saying that there may well be some "right now".

==Epistemic logic==

'''Epistemic modalities''' (from the Greek ''episteme'', knowledge), deal with the ''certainty'' of sentences.  The operators are translated as  "It is certainly true that..." and "It may (given the available information) be true that..."  In ordinary speech both modalities are often expressed in similar words; the following contrasts may help:

A person, Jones, might reasonably say ''both'': (1) "No, it is ''not'' possible that [[Bigfoot]] exists; I am quite certain of that"; ''and'', (2) "Sure, Bigfoot possibly ''could'' exist". What Jones means by (1) is that given all the available information, there is no question remaining as to whether Bigfoot exists.  This is an epistemic claim. By (2) he makes the ''metaphysical'' claim that it is ''possible for'' Bigfoot to exist, ''even though he does not'' (which is not equivalent to "it is ''possible that'' Bigfoot exists – for all I know," which contradicts (1)).

From the other direction, Jones might say, (3) "It is ''possible'' that [[Goldbach's conjecture]] is true; but also ''possible'' that it is false", and ''also'' (4) "if it ''is'' true, then it is necessarily true, and not possibly false". Here Jones means that it is ''epistemically possible'' that it is true or false, for all he knows (Goldbach's conjecture has not been proven either true or false), but if there ''is'' a proof (heretofore undiscovered), then it would show that it is not ''logically'' possible for Goldbach's conjecture to be false—there could be no set of numbers that violated it. Logical possibility is a form of ''alethic'' possibility; (4) makes a claim about whether it is possible (ie, logically speaking) that a mathematical truth to have been false, but (3) only makes a claim about whether it is possible, for all Jones knows, (ie, speaking of certitude) that the mathematical claim is specifically either true or false, and so again Jones does not contradict himself.  It is worthwhile to observe that Jones is not necessarily correct: It is possible (epistemically) that Goldbach's conjecture is both true and unprovable.

Epistemic possibilities also bear on the actual world in a way that metaphysical possibilities do not. Metaphysical possibilities bear on ways the world ''might have been,'' but epistemic possibilities bear on the way the world ''may be'' (for all we know). Suppose, for example, that I want to know whether or not to take an umbrella before I leave. If you tell me "it is ''possible that'' it is raining outside" – in the sense of epistemic possibility – then that would weigh on whether or not I take the umbrella. But if you just tell me that "it is ''possible for'' it to rain outside" – in the sense of ''metaphysical possibility'' – then I am no better off for this bit of modal enlightenment.

==Temporal logic==

There are several analogous modes of speech, which though less likely to be confused with alethic modalities are still closely related.  One is talk of time.  It seems reasonable to say that possibly it will rain tomorrow, and possibly it won't; on the other hand, if it rained yesterday, if it really already did so, then it cannot be quite correct to say "It may not have rained yesterday."  It seems the past is "fixed", or necessary, in a way the future is not. This is sometimes referred to as [[accidental necessity]].

A standard method for formalizing talk of time is to use ''two'' pairs of operators, one for the past and one for the future. For the past, let "It has always been the case that..." be equivalent to the box, and let "It was once the case that..." be equivalent to the diamond. For the future, let "It will always be the case that..." be equivalent to the box, and let "it will eventually be the case that..." be equivalent to the diamond.  If these two systems are used together, it will, obviously, be necessary to indicate, as by [[subscript]]s, which box is which.

Additional binary operators are also relevant to temporal logics, ''q.v.'' [[Linear Temporal Logic]].

==Deontic logic==
Likewise talk of morality, or of [[obligation]] and [[norm (philosophy)|norms]] generally, seems to have a modal structure.  The difference between "You must do this" and "You may do this" looks a lot like the difference between "This is necessary" and "This is possible".  Such logics are called ''[[deontic logic|deontic]]'', from the Greek for "duty".

== Doxastic logic ==

{{main|Doxastic logic}}

''Doxastic logic'' is a modal logic that is concerned with [[reasoning]] about [[belief]]s. The term doxastic is derived from the [[ancient Greek]] ''doxa'' which means 'belief.' Typically, a doxastic logic uses Bx to mean "It is believed that x is the case" and the set <math>\mathbb{B}</math> denotes a set of beliefs.

==Other modal logics==

Significantly, modal logics can be developed to accommodate most of these idioms; it is the fact of their common logical structure (the use of "intensional" or non-truth-functional sentential operators) that make them all varieties of the same thing. [[Epistemic logic]] is arguably best captured in the system "[[S4 (modal logic)|S4]]"; deontic logic in the system "D", [[temporal logic]] in "T" and alethic logic arguably with "[[S5 (modal logic)|S5]]".

== Interpretations of modal logic ==

{{see|Interpretation (logic)}}

In the most common interpretation of modal logic, one considers "all [[logically possible]] worlds". If a statement is true in all [[possible worlds]], then it is a necessary truth. If a statement happens to be true in our world, but is not true in all possible worlds, then it is a contingent truth. A statement that is true in some possible world (not necessarily our own) is called a possible truth.

Whether this "possible worlds idiom" is the best way to interpret modal logic, and how literally this idiom can be taken, is a live issue for metaphysicians. For example, the possible worlds idiom would translate the claim about Bigfoot as "There is some possible world in which Bigfoot exists". To maintain that Bigfoot's existence is possible, but not actual, one could say, "There is some possible world in which Bigfoot exists; but in the actual world, Bigfoot does not exist". But it is unclear what it is that making modal claims commits us to. Are we really alleging the existence of possible worlds, every bit as real as our actual world, just not actual? [[David Lewis (philosopher)|David Lewis]] made himself notorious by biting the bullet, asserting that all merely possible worlds are as real as our own, and that what distinguishes our world as ''actual'' is simply that it ''is'' indeed our world – ''this'' world (see [[Indexicality]]). That position is a major tenet of "[[modal realism]]". Most philosophers decline to endorse such a view, considering it ontologically extravagant, and preferring to seek various ways to paraphrase away the ontological commitments implied by our modal claims.

==Formal rules==
Many systems of modal logic, with widely varying properties, have been proposed since [[C. I. Lewis]] began working in the area in 1910. Hughes and Cresswell (1996), for example, describe 42 normal and 25 non-normal modal logics. Zeman (1973) describes some systems Hughes and Cresswell omit.

Modern treatments of modal logic begin by augmenting the [[propositional calculus]] with two unary operations, one denoting "necessity" and the other "possibility". The notation of [[Clarence Irving Lewis|Lewis]], much employed since, denotes "necessarily ''p''" by a prefixed "box" (<!--'''[]p'''--> <math>\Box p </math>) whose scope is established by parentheses. Likewise, a prefixed "diamond" (<!--'''<>p'''--><math>\Diamond p</math>) denotes "possibly ''p''". Regardless of notation, each of these operators is definable in terms of the other:
* <!--[]p--><math>\Box p</math> (necessarily ''p'') is equivalent to <!-- ~<>~p --><math>\neg \Diamond \neg p </math> ("not possible that not-''p''")
* <!-- <>p --> <math>\Diamond p </math> (possibly ''p'') is equivalent to <!-- ~[]~p --> <math>\neg \Box \neg p </math> ("not necessarily not-''p''")
Hence <math>\Box</math> and <math>\Diamond</math> form a [[duality|dual pair]] of operators.

In many modal logics, the necessity and possibility operators satisfy the following analogs of [[de Morgan's laws]] from [[Boolean algebra (logic)|Boolean algebra]]:

:"It is '''not necessary that'''  ''X''" is logically equivalent to "It is '''possible that not'''  ''X''".

:"It is '''not possible that'''  ''X''" is logically equivalent to "It is '''necessary that not'''  ''X''".

Precisely what axioms and rules must be added to the [[propositional calculus]] to create a usable system of modal logic is a matter of philosophical opinion, often driven by the theorems one wishes to prove. Many modal logics, known collectively as [[normal modal logic]]s, include the following rule and axiom:
* '''N''', ''Necessitation Rule'': If ''p'' is a [[theorem]] (of any system invoking '''N'''), then <math>\Box p</math> is likewise a theorem.
* '''K''', ''Distribution Axiom'': <!--[](''p'' → ''q'') → ([]p → []q)--> <math> \Box (p \rightarrow q)  \rightarrow (\Box p \rightarrow \Box q)</math>.

The weakest [[normal modal logic]], named ''K'' in honor of [[Saul Kripke]], is simply the [[propositional calculus]] augmented by <math> \Box </math>, the rule '''N''', and the axiom '''K'''. ''K'' is weak in that it fails to determine whether a proposition can be necessary but only contingently necessary. That is, it is not a theorem of ''K'' that if <!-- []p --> <math> \Box p </math> is true then <!-- [][]p --> <math> \Box \Box p </math> is true, i.e., that necessary truths are "necessarily necessary". If such perplexities are deemed forced and artificial, this defect of ''K'' is not a great one. In any case, different answers to such questions yield different systems of modal logic.

Adding axioms to ''K'' gives rise to other well-known modal systems. One cannot prove in ''K'' that if "''p'' is necessary" then ''p'' is true. The axiom '''T''' remedies this defect:
*'''T''', ''Reflexivity Axiom'': <!-- []p → p --> <math> \Box p \rightarrow p </math> (If ''p'' is necessary, then ''p'' is the case.) '''T''' holds in most but not all modal logics. Zeman (1973) describes a few exceptions, such as S1^0.
Other well-known elementary axioms are:
*'''4''': <math> \Box p \rightarrow \Box \Box p</math>
*'''B''': <math> p \rightarrow \Box \Diamond p</math>
*'''D''': <math> \Box p \rightarrow \Diamond p</math>
*'''E''': <math> \Diamond p \rightarrow \Box \Diamond p.</math>
These axioms yield the systems:
*''K'' := '''K''' + '''N'''
*''T'' := ''K'' + '''T'''
*''S4'' := ''T'' + '''4'''
*''S5'' :=  ''S4'' + '''B''' or ''T'' + '''E'''
*''D'' := ''K'' + '''D'''.
''K'' through ''S5'' form a nested hierarchy of systems, making up the core of [[normal modal logic]]. ''D'' is primarily of interest to those exploring the [[deontic logic|deontic]] interpretation of modal logic.

The commonly employed system ''S5'' simply makes all modal truths necessary. For example, if ''p'' is possible, then it is "necessary" that ''p'' is possible. Also, if ''p'' is necessary, then it is necessary that ''p'' is necessary. Although controversial, this is commonly justified on the grounds that ''S5'' is the system obtained if every possible world is possible relative to every other world. Other systems of modal logic have been formulated, in part because ''S5'' does not describe every kind of metaphysical modality of interest. This suggests that talk of possible worlds and their semantics may not do justice to all modalities.

==Development of modal logic ==
Although [[Aristotle]]'s logic is almost entirely concerned with the theory of the [[categorical syllogism]], there are passages in his work, such as the famous [[problem of the futures contingents|Sea-Battle Argument]] in ''[[De Interpretatione]]'' § 9, that are now seen as anticipations of modal logic and its connection with potentiality and time. Modal logic as a self-aware subject owes much to the writings of the [[Scholastics]], in particular [[William of Ockham]] and [[John Duns Scotus]], who reasoned informally in a modal manner, mainly to analyze statements about [[essence]] and [[accident (philosophy)|accident]].

[[C. I. Lewis]] founded modern modal logic in his 1910 Harvard thesis and in a series of scholarly articles beginning in 1912. This work culminated in his 1932 book ''Symbolic Logic'' (with C. H. Langford), which introduced the five systems ''S1'' through ''S5''. The contemporary era in modal logic began in 1959, when [[Saul Kripke]] (then only a 19 year old [[Harvard University]] undergraduate) introduced the now-standard [[Kripke semantics]] for modal logics. These are commonly referred to as "possible worlds" semantics. Kripke and [[A. N. Prior]] had previously corresponded at some length.

[[A. N. Prior]] created [[temporal logic]], closely related to modal logic, in 1957 by adding modal operators [F] and [P] meaning "henceforth" and "hitherto". [[Vaughan Pratt]] introduced [[dynamic logic]] in 1976. In 1977, [[Amir Pnueli]] proposed using temporal logic to formalise the behaviour of continually operating concurrent programs. Flavors of temporal logic include propositional dynamic logic (PDL), propositional linear temporal logic (PLTL), [[linear temporal logic]] (LTL), [[computational tree logic]] (CTL), [[Hennessy-Milner logic]], and ''T''.

The mathematical structure of modal logic, namely [[Boolean algebra (structure)|Boolean algebra]]s augmented with [[unary operation]]s (often called "modal algebras"), began to emerge with J. C. C. McKinsey's 1941 proof that ''S2'' and ''S4'' are decidable, and reached full flower in the work of [[Alfred Tarski]] and his student [[Bjarni Jonsson]] (Jonsson and Tarski 1951-52). This work revealed that ''S4'' and ''S5'' are models of [[interior algebra]], a proper extension of Boolean algebra originally designed to capture the properties of the [[interior operator|interior]] and [[closure operator]]s of [[topology]]. Texts on modal logic typically do little more than mention its connections with the study of [[Boolean algebra (structure)|Boolean algebra]]s and [[topology]]. For a thorough survey of the history of formal modal logic and of the associated mathematics, see [http://www.mcs.vuw.ac.nz/~rob/papers/modalhist.pdf Goldblatt (2006).]

== References ==
* Blackburn, Patrick, Maarten de Rijke, and Yde Venema (2001) ''Modal Logic''. Cambridge Univ. Press. ISBN 0-521-80200-8
* Blackburn, P., [[Johan van Benthem (logician)|van Benthem, J.,]] and Frank Wolter, eds. (2006) ''[http://www.csc.liv.ac.uk/~frank/MLHandbook/ Handbook of Modal Logic]''. North Holland.
* Chagrov, Aleksandr, and Michael Zakharyaschev (1997) ''Modal Logic''. Oxford Univ. Press. ISBN 0-19-853779-4
* Chellas, B. F. (1980) ''Modal Logic: An Introduction''. Cambridge Univ. Press. ISBN 0-521-22476-4
*Cresswell, M. J. (2001) "Modal Logic" in Goble, Lou, ed., ''The Blackwell Guide to Philosophical Logic''. Basil Blackwell: 136-58. ISBN 0-631-20693-0
* Fitting, Melvin, and R.L. Mendelsohn (1998) ''First Order Modal Logic''. Kluwer. ISBN 0-7923-5335-8
* Garson, James W. (2006) ''Modal Logic for Philosophers''. Cambridge Univ. Press. ISBN 0-521-68229-0. A thorough introduction to modal logic, with coverage of various derivation systems and a distinctive approach to the use of diagrams in aiding comprehension. 
* Girle, Rod (2000) ''Modal Logics and Philosophy''. Acumen (UK). ISBN 0-7735-2139-9. Proof by [[analytic tableau|refutation trees]]. A good introduction to the varied interpretations of modal logic.
* [http://www.mcs.vuw.ac.nz/~rob/ Goldblatt, Robert] (1992) "Logics of Time and Computation", 2nd ed., CSLI Lecture Notes No. 7. University of Chicago Press.
* —— (1993) ''Mathematics of Modality'', CSLI Lecture Notes No. 43. University of Chicago Press.
* —— (2006) "[http://www.mcs.vuw.ac.nz/~rob/papers/modalhist.pdf Mathematical Modal Logic: a View of its Evolution,]" in Gabbay, D. M., and Woods, John, eds., ''Handbook of the History of Logic, Vol. 6''. Elsevier BV.
*Goré, Rajeev (1999) "Tableau Methods for Modal and Temporal Logics" in D'Agostino, M., Dov Gabbay, R. Haehnle, and J. Posegga, eds., ''Handbook of Tableau Methods''. Kluwer: 297-396.
* Hughes, G. E., and M.J. Cresswell (1996) ''A New Introduction to Modal Logic''. Routledge. ISBN 0-415-12599-5
*[[Bjarni Jonsson|Jónsson, B.]] and [[Alfred Tarski]], 1951-52, "Boolean Algebra with Operators I and II", ''American Journal of Mathematics 73'': 891-939 and ''74'': 129-62.
*Kracht, Marcus (1999) ''Tools and Techniques in Modal Logic'', Studies in Logic and the Foundations of Mathematics No. 142. North Holland.
* [[John Lemmon|Lemmon, E. J.]] (with [[Dana Scott]]) (1977) ''An Introduction to Modal Logic'', American Philosophical Quarterly Monograph Series, no. 11 (Krister Segerberg, series ed.). Basil Blackwell.

Free and online:
* Zeman, J. J. (1973) ''[http://www.clas.ufl.edu/users/jzeman/modallogic/ Modal Logic.]'' Reidel. Employs [[Polish notation]].

==See also==
*[[Accessibility relation]]
*[[Counterpart theory]]
*[[De dicto and de re]]
*[[Description logic]]
*[[Doxastic logic]]
*[[Dynamic logic (modal logic)|Dynamic logic]]
*[[Epistemic logic]]
*[[Hybrid logic]]
*[[Interior algebra]]
*[[Interpretability logic]]
*[[Kripke semantics]]
*[[Possible worlds]]
*[[Problem of the futures contingents]]
*[[Provability logic]]
*[[Two dimensionalism]]
*[[Modal verb]]

==Notes==
{{reflist}}

==External links==
* [[Stanford Encyclopedia of Philosophy]]:
** "[http://plato.stanford.edu/entries/logic-modal Modal logic]" – by James Garson.
**"[http://plato.stanford.edu/entries/logic-provability/ Provability Logic]" – by Rineke Verbrugge.
* [[Edward N. Zalta]], 1995, "[http://mally.stanford.edu/notes.pdf Basic Concepts in Modal Logic.]"
* [[John McCarthy (computer scientist)|John McCarthy]], 1996, "[http://www-formal.stanford.edu/jmc/mcchay69/node22.html Modal Logic.]"
* [http://molle.sourceforge.net/ Molle] a Java prover for experimenting with modal logics
* Suber, Peter, 2002, "[http://www.earlham.edu/~peters/courses/logsys/nonstbib.htm#modal Bibliography of Modal Logic.]" 
* [http://www.cc.utah.edu/~nahaj/logic/structures/systems/index.html List of Logic Systems]  List of many modal logics with sources, by John Halleck.
* [http://aiml.net/ Advances in Modal Logic.] Biannual international conference and book series in modal logic.

==Acknowledgements==
This article includes material from the [[Free On-line Dictionary of Computing]], used with [[Wikipedia:Foldoc license|permission]] under the [[GFDL]].

{{portalpar|Logic}}
{{Logic}}

[[Category:Logic]]
[[Category:Modal logic| ]]
[[Category:Philosophical logic]]

[[ar:منطق طوري]]
[[da:Modallogik]]
[[de:Modallogik]]
[[es:Lógica modal]]
[[fa:منطق موجهات]]
[[fr:Logique modale]]
[[io:Modala logiko]]
[[is:Háttarökfræði]]
[[it:Logica modale]]
[[he:לוגיקה מודלית]]
[[hu:Modális logika]]
[[nl:Modale logica]]
[[ja:様相論理学]]
[[no:Modallogikk]]
[[nn:Modallogikk]]
[[pl:Logika modalna]]
[[pt:Lógica modal]]
[[ru:Модальная логика]]
[[sk:Modálna logika]]
[[fi:Modaalilogiikka]]
[[sv:Modallogik]]
[[zh:模态逻辑]]