# What is modal logic for?

I understand "pure" logic as a structural description of what a valid proof is but I have never understood the reasons for using modal logic.

What's an example typical of how modal logic is used?

## What is modal logic?

Modal logic is an extension of classic propositional and predicate logic that allows the use of modal operators. In others words, modal logic is everything classic logic is + modal operators. Modal operators express modality, such as:

• Necessity (denoted by □)
• Possibility (denoted by ◇)

The above possibilities are the only operators used in modal logic in the narrow sense. However, the term modal logic is often used to include other extensions, for instance temporal logic, that allows for the expression of past or future truths.

## Why is modal logic useful?

Classic logic is great for mathematics, but for the analysis of daily language and arguments, it lacks certain operators. There are many sentences that you can't express in classic logic that can be expressed in modal logic. Example: "I may get burned if I lie in the sun for too long". In classic logic, you can say: "I get burned if I lie in the sun for too long", but you can't express the possibility of getting burned. In classic logic, it's either true or false. In modal logic, you can also express the possibility or impossibility of a proposition being true or false.

• Thanks for your reply! To be honest I still don't understand: If you have the sentence in English why would translating into modal logic be a good idea? I feel like pigeon-holing a sentence into a formal logical statement would change its meaning! – user3085 Jan 31 '13 at 22:58
• You might want to extend your answer to include other "modes" that people sometimes study under the label "modal logic": epistemic logic, deontic logic, tense logic and so on. – Seamus Feb 1 '13 at 14:02
• @Seamus I intentionally refrained from doing so, because then this article would almost become a copy of the SEP, which seems pointless to me. I wanted to be as brief as possible here. – Ben Feb 1 '13 at 15:25
• @user58512 Dennis has replied to that question I see, so I won't reply extensively here. There are in short multiple reasons, the main one being that formal logic is less ambiguous than daily language. – Ben Feb 1 '13 at 15:29
• Well, I mean, I think it would be worth at least saying that there are modalities besides necessity and possibility that modal logic can capture. – Seamus Feb 1 '13 at 17:10

Extending previous answers by ChaosAndOrder and Dennis…

You seem to appreciate why "pure" logic (I take it that you mean classical first order logic) is useful in the context of mathematical logic, but you don't see the point in formalizing other modal notions in ordinary language. While presenting you the many applications of modal logic might convince you, it may be easier to indicate how modal logic was important in the development of the very field of mathematical logic that you seem to appreciate.

The formalization of modal logic has been a breakthrough in the development of model theory, one of the four branches of mathematical logic (the other being set theory, recursion theory and proof theory). See Kripke semantics for more details.

Modal logic has found some very natural applications in metalogic, such as provability logic (where □ means 'it is provable that'). A milestone in the analysis of provability is Solovay's arithmetical completeness theorem published in 1976.

Another interesting (but very advanced) example is the use of modal logic to study the relations between forcing extensions in set theory. See Hamkins & Loewe, The Modal Logic of Forcing, 2005:

What are the most general principles in set theory relating forceability and truth? As with Solovay's celebrated analysis of provability, both this question and its answer are naturally formulated with modal logic. We aim to do for forceability what Solovay did for provability. A set theoretical assertion psi is forceable or possible, if psi holds in some forcing extension, and necessary, if psi holds in all forcing extensions. In this forcing interpretation of modal logic, we establish that if ZFC is consistent, then the ZFC-provable principles of forcing are exactly those in the modal theory known as S4.2.

So, I will tailor my response to your comment to ChaosAndOrder.

The reason we want to utilize modal logic is to precisify ordinary language. Ordinary language is notoriously ambiguous and the analysis of ordinary language modal operators is fraught with difficulty.

By regimenting our discourse into formal (quantified) modal logic we can eliminate some of these ambiguities. We can distinguish between modality de dicto (applying to a whole proposition) and modality de re (applying to predicating a property of an individual). Ordinary English is almost systematically ambiguous between the two.

In general, the reason to formalize any natural language statements is to achieve a greater precision in our discourse and to remove (as much as is possible) indeterminacy and ambiguity.

As an aside, classical logic is not great for analysis of mathematical discourse. The model theory of mathematics bears a striking resemblance to possible worlds semantics for modal logic. While it is true that within a model mathematics behaves classically, when we assess claims like categoricity (all models are identical up to isomorphism) we are assessing claims that are quite plausibly modal.

Also, the characterization of validity in classical logic is often modal in some sense. How do we explain validity? It is impossible for the premises to be true and the conclusion false (or, if the premises are true the conclusion MUST be true as well). What this (arguably) shows us is that validity/logical consequence is a modal notion.

• Can you please elaborate a bit more on this (e.g. suggest further reading): "The model theory of mathematics bears a striking resemblance to possible worlds semantics for modal logic". Thx & +1. – Drux Feb 1 '13 at 12:48
• "While it is true that within a model mathematics behaves classically, when we assess claims like categoricity (all models are identical up to isomorphism) we are assessing claims that are quite plausibly modal." We can turn this around, and say that any time one is making claims of modality, one is talking about the space of possible models, and that a Theory of `X` is not so much "modal" as it is a subject which describes not just different ways of realizing `X` but the relationships (not just isomorphisms) between those. The question is: does 'modality' really provide additional clairity? – Niel de Beaudrap Feb 1 '13 at 12:58
• @Drux: Model theory for theories in classical logic interprets the theory in a model and so provides a situation for concrete facts for the theory, that is we have semantics. Kripke-Joyal extended this from classical to intuitionistic & modal logic where its usually called possible world semantics. – Mozibur Ullah Feb 1 '13 at 14:12
• @NieldeBeaudrap I'm not sure what the question is. It seems that what you're describing is something modal with a little extra (the relations between models which wouldn't have an equivalent in the semantics for modal logic). Is this right? When you ask 'does "modality" really provide additional clarity?', are you asking whether thinking of model theory for mathematics as akin to the possible worlds semantics for modal logic adds clarity? – Dennis Feb 1 '13 at 15:54
• @Drux When I have time later today (i.e., when I'm not prepping for the class I have to teach in an hour) I'll expand on my answer. Unless, of course, Mozibur's response cleared up any confusions. – Dennis Feb 1 '13 at 15:55