What is modal logic for?

Question

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?

Answer 1

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.

Further reading:

• SEP
• Lecture notes of a Stanford course on modal logic
• Youtube course on modal logic

Answer 2

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.

Answer 3

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.