Chapter 42 Introducing modal logic
Modal logic (ML) is the logic of modalities, ways in which a statement can be true. Necessity and possibility are two such modalities: a statement can be true, but it can also be necessarily true (true no matter how the world might have been). For instance, logical truths are not just true because of some accidental feature of the world, but true come what may. A possible statement may not actually be true, but it might have been true. We use $\mathrm{\square}$ to express necessity, and $\mathrm{\u25c7}$ to express possibility. So you can read $\mathrm{\square}\mathcal{A}$ as It is necessarily the case that $\mathcal{A}$, and $\mathrm{\u25c7}\mathcal{A}$ as It is possibly the case that $\mathcal{A}$.
There are lots of different kinds of necessity. It is humanly impossible for me to run at 100mph. Given the sorts of creatures that we are, no human can do that. But still, it isn’t physically impossible for me to run that fast. We haven’t got the technology to do it yet, but it is surely physically possible to swap my biological legs for robotic ones which could run at 100mph. By contrast, it is physically impossible for me to run faster than the speed of light. The laws of physics forbid any object from accelerating up to that speed. But even that isn’t logically impossible. It isn’t a contradiction to imagine that the laws of physics might have been different, and that they might have allowed objects to move faster than light.
Which kind of modality does ML deal with? All of them! ML is a very flexible tool. We start with a basic set of rules that govern $\mathrm{\square}$ and $\mathrm{\u25c7}$, and then add more rules to fit whatever kind of modality we are interested in. In fact, ML is so flexible that we do not even have to think of $\mathrm{\square}$ and $\mathrm{\u25c7}$ as expressing necessity and possibility. We might instead read $\mathrm{\square}$ as expressing provability, so that $\mathrm{\square}\mathcal{A}$ means It is provable that $\mathcal{A}$, and $\mathrm{\u25c7}\mathcal{A}$ means It is not refutable that $\mathcal{A}$. Similarly, we can interpret $\mathrm{\square}$ to mean $S$ knows that $\mathcal{A}$ or $S$ believes that $\mathcal{A}$. Or we might read $\mathrm{\square}$ as expressing moral obligation, so that $\mathrm{\square}\mathcal{A}$ means It is morally obligatory that $\mathcal{A}$, and $\mathrm{\u25c7}\mathcal{A}$ means It is morally permissible that $\mathcal{A}$. All we would need to do is cook up the right rules for these different readings of $\mathrm{\square}$ and $\mathrm{\u25c7}$.
A modal formula is one that includes modal operators such as $\mathrm{\square}$ and $\mathrm{\u25c7}$. Depending on the interpretation we assign to $\mathrm{\square}$ and $\mathrm{\u25c7}$, different modal formulas will be provable or valid. For instance, $\mathrm{\square}\mathcal{A}\to \mathcal{A}$ might say that “if $\mathcal{A}$ is necessary, it is true”, if $\mathrm{\square}$ is interpreted as necessity. It might express “if $\mathcal{A}$ is known, then it is true”, if $\mathrm{\square}$ expresses known truth. Under both these interpretations, $\mathrm{\square}\mathcal{A}\to \mathcal{A}$ is valid: All necessary propositions are true come what may, so are true in the actual world. And if a proposition is known to be true, it must be true (one can’t know something that’s false). However, when $\mathrm{\square}$ is interpreted as “it is believed that” or “it ought to be the case that”, $\mathrm{\square}\mathcal{A}\to \mathcal{A}$ is not valid: We can believe false propositions. Not every proposition that ought to be true is in fact true, e.g., “Every murderer will be brought to justice.” This ought to be true, but it isn’t.
We will consider different kinds of systems of ML. They differ in the rules of proof allowed, and in the semantics we use to define our logical notions. The different systems we’ll consider are called $\mathbf{K}$, $\mathbf{T}$, $\mathrm{\mathbf{S}\U0001d7d2}$, and $\mathrm{\mathbf{S}\U0001d7d3}$. $\mathbf{K}$ is the basic system; everything that is valid or provable in $\mathbf{K}$ is also provable in the others. But there are some things that $\mathbf{K}$ does not prove, such as the formula $\mathrm{\square}A\to A$ for sentence letter $A$. So $\mathbf{K}$ is not an appropriate modal logic for necessity and possibility (where $\mathrm{\square}\mathcal{A}\to \mathcal{A}$ should be provable). This is provable in the system $\mathbf{T}$, so $\mathbf{T}$ is more appropriate when dealing with necessity and possibiliity, but less appropriate when dealing with belief or obligation, since then $\mathrm{\square}\mathcal{A}\to \mathcal{A}$ should not (always) be provable. The perhaps best system of ML for necessity and possibility, and in any case the most widely accepted, is the strongest of the systems we consider, $\mathrm{\mathbf{S}\U0001d7d3}$.
42.1 The Language of ML
In order to do modal logic, we have to do two things. First, we want to learn how to prove things in ML. Second, we want to see how to construct interpretations for ML. But before we can do either of these things, we need to explain how to construct sentences in ML.
The language of ML is an extension of TFL. We could have started with FOL, which would have given us Quantified Modal Logic (QML). QML is much more powerful than ML, but it is also much, much more complicated. So we are going to keep things simple, and start with TFL.
Just like TFL, ML starts with an infinite stock of atoms. These are written as capital letters, with or without numerical subscripts: $A$, $B$, …${A}_{1}$, ${B}_{1}$, …We then take all of the rules about how to make sentences from TFL, and add two more for $\mathrm{\square}$ and $\mathrm{\u25c7}$:

1.
Every atom of ML is a sentence of ML.

2.
If $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$ is a sentence of ML, then $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\neg}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$ is a sentence of ML.

3.
If $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$ and $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$ are sentences of ML, then $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\wedge $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$ is a sentence of ML.

4.
If $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$ and $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$ are sentences of ML, then $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\vee $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$ is a sentence of ML.

5.
If $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$ and $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$ are sentences of ML, then $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\to $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$ is a sentence of ML.

6.
If $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$ and $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}$ are sentences of ML, then $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$($}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\leftrightarrow $}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{B}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$)$}$ is a sentence of ML.

7.
If $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$ is a sentence of ML, then $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\square}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$ is a sentence of ML.

8.
If $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$ is a sentence of ML, then $\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathrm{\u25c7}$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$$}\colorbox[rgb]{0.992156862745098,0.956862745098039,0.980392156862745}{$\mathcal{A}$}$ is a sentence of ML.

9.
Nothing else is a sentence of ML.
Here are some examples of ML sentences:
$A$  
$P\vee Q$  
$\mathrm{\square}A$  
$C\vee \mathrm{\square}D$  
$\mathrm{\square}\mathrm{\square}(A\to R)$  
$\mathrm{\square}\mathrm{\u25c7}(S\wedge (Z\leftrightarrow (\mathrm{\square}W\vee \mathrm{\u25c7}Q)))$ 