What's the point of modal logic?

I was just reading about modal logic at wikipedia, and it seems that the usual approach is to introduce two new operations $\Diamond$ and $\square$ that mean 'possibly' and 'necessarily' respectively.

I don't get this. If I wanted to say 'it is possible that $x^2=2$' I would write 'there exists $x$ such that $x^2=2$.' What am I missing?

Edit: are we perhaps quantifying over models? So $\Diamond$ means 'there exists a model of the axioms such that' and $\square$ means 'for all models of the axioms it holds that'?


Simply put, modal logics are useful any time that you want to reason about truths that are, well, modal. The example you gave contrasts first order logic and modal logic, but a more common starting point is to build modal logics upon propositional logics.

One of the characteristics of modal logics is that the modal operator, often written $\Box$, is not truth functional. Since a propositional variable $P$ can only be true or false, there are only two truth functions that we can apply to it: the identity function (i.e., just $P$) and negation (i.e., $\lnot P$). (Actually, we could also apply "false everywhere" and "true everywhere" functions, but these aren't particularly interesting here.) Now, if $P$ stands for the proposition “I am wearing a hat,” then there is nothing about the logical content of that proposition that makes it necessarily true or false, although of course it actually must be true or false at a given time. If I ask you, “is it logically necessary that I am wearing a hat right now,” you would probably say no, even if at this moment I am, in fact, wearing a hat. Symbolically, you would probably affirm both $\lnot\Box P$ as well as $P$. It's not hard to see that it could be the other way round and you might affirm both $\lnot\Box P$ as well as $\lnot P$. $\Box \phi$ is a formula whose truth value is not a function of the truth of $\phi$. There may, of course, be some relationship between the truth value of some $\phi$ and the truth value of $\Box\phi$ (e.g., for contradictory $\phi$, we might expect that $\phi$ if and only if $\lnot\Box\phi$, and for tautologous $\phi$ that $\phi$ if and only if $\Box\phi$). These types of considerations lead people to different axiomatizations of modal logic.

When the modal operator is interpreted as something other than necessity, the distinction becomes even more pronounced. For instance, in deontic logic the modal operator $\Box$, which is often written $O$, is interpreted as obligation; that is, $O\phi$ means that “it is obligatory that $\phi$,” or “it ought to be the case that $\phi$.” This can be used to formalize and reason about the consistency and the consequences of ethical theories. Most axiomatizations of alethic modal logic include the theorem that $\Box P \to P$, that is, that if $P$ is necessary, then $P$ must also be true (how could it not be?). As our life experiences tell us, though, it's not the case that just because something ought to be true, that it is true, so $OP \to P$ does not hold, in general, in deontic logic.

With regards to your example that started in first-order logic (since you considered the possibility of asserting $\exists x.(x^2 = 2)$), let's consider some different formulae that involve $\exists x$, $x^2 = 2$, and $\Diamond$ (which is often taken as an abbreviation of $\lnot\Box\lnot$). Since $x$ is a variable, we need to quantify over it, so all three of these formulae include an existential quantification.

\begin{gather} \exists x.(x^2 = 2) \\ \Diamond \exists x.(x^2 = 2) \\ \exists x.\Diamond(x^2 = 2) \end{gather}

Under the alethic intepretation, where $\Box$ is logical necessity and $\Diamond$ is logical possibility, the first, $\exists x.(x^2 = 2)$, says that it happens to be the case that there is an $x$ such that $x^2 = 2$, but makes no claim about whether or not it is logically necessary or not. Just as most alethic modal logics will allow us to infer that if $P$ is necessary, then $P$ must be true, they will also permit that if $P$ is true, then $P$ is possible. In these logics, we at least know that $\exists x.(x^2 = 2)$ is logically possible.

The second says that it is logically possible that there is an $x$ such that $x^2 = 2$, but makes no claim about whether or not there actually is such an $x$. The fact that it is possible at least implies that it isn't logically necessary that there isn't such an $x$.

The third is probably the most subtle of the three sentences, and the interaction between first-order quantification and modal operators allows a variety of interpretations, but it says that it does happen to be true that there is an $x$ (so we can actually point to it, it's not just a possibly existing thing; it actually exists here) such that it's logically possible that $x^2 = 2$.

With mathematically oriented sentences, the distinction between logical necessity and truth might become blurred, because we tend to think of mathematical truths as logical necessities. (We proved them logically, after all, right?) However, if you go back and consider the sentences

\begin{gather} \exists p.\mathit{wearingHat}(p) \\ \Diamond \exists p.\mathit{wearingHat}(p) \\ \exists p.\Diamond\mathit{wearingHat}(p) \end{gather}

you may find the difference enlightening. The first says that some man is wearing a hat, the second that there could be a man who is wearing a hat, the third that there is a man who could be wearing a hat. Now try the same with the deontic interpretation where $\Diamond$ is permissibility. The first says the same, that some man is wearing a hat, the second that its permissible that there is a man wearing a hat, and the third says that some particular man is permitted to wear a hat!

With regard to your edit about whether $\Box$ is quantifying over models: the Kripke semantics for modal logic comes very close to quantifying over models. In the Kripke semantics for modal logic, there is a set of possible worlds $\cal W$ and a distinguished world $w_0$. Each world provides an interpretation for the non modal sentences. (That is, if we're in a propositional modal logic, each world has a truth assignment. If we're in a first-order modal logic, each world has first-order interpretation, and so on.) There is also a binary relation $R$ on $\cal W$ called the accessibility relation. When $R(x,y)$, we say that $y$ is accessible from $x$. In this framwork, $\Box\phi$ is true in a world $w$ if and only if $\phi$ (without the $\Box$) is true in every world accessible from $w$. $\Diamond\phi$ is true in $w$ if and only if $\phi$ is true in some world accessible from $w$. Different modal axioms imply different conditions on $R$, or alternatively, different structure in $R$ implies that different modal theorems hold. For instance, the formula

$$ \Box P \to P \tag{K} $$

which is typically accepted in alethic logic (if something is logically necessary, then it is true), means that $R$ must be reflexive (i.e., $R(w,w)$ for every world $w$). Can you see why?


Another interpretation would be temporal logic: If you interpret $\Diamond$ as "eventually" and $\square$ as "always", this allows you to describe the properties of systems with evolving state. See http://en.wikipedia.org/wiki/Temporal_logic; this kind of logic is used in some areas of computer science (model checking in particular).


While "it is possible that" and "it is necessary that" are the common interpretation of the $\Diamond$ and $\Box$ operators of modal logic, these are by no means the only interpretations. From a mathematical point of view, provability logic (see also the Stanford Encyclopedia of Philosophy) is quite important in the analysis of sufficiently strong formal systems (such as Peano Arithmetic) (where $\Diamond$ is interpreted as "it is consistent that" and $\Box$ as "it is provable that"). This has also been adapted by Joel David Hamkins and Benedikt Löwe to the study of forcing in set theory.