01-operators.tex

\chapter{Modal Operators}\label{ch:operators}

\section{A new language}
\label{sec:intro}

% Modal Logic

Modal logic is an extension of propositional and predicate logic that is widely
used to reason about possibility and necessity, obligation and permission, the
flow of time, the processing of computer programs, and a range of other topics.
Each of these applications begins by adding new symbols to the formal language
of classical propositional or predicate logic. Before we explore such additions,
let's briefly review why we use formal languages in the first place.

% Validity

When reasoning about a given topic, we sometimes want to make sure that the
stated conclusions really follow from the stated premises. If they do, we say
that the reasoning is \emph{valid}. By this we mean that there is no conceivable
scenario in which the premises are true while the conclusions are false.

% Logical validity

Here is an example of a valid argument.
%
\begin{quote}
  All myriapods are oviparous.\\
  Some arthropods are myriapods.\\
  Therefore: Some arthropods are oviparous.
\end{quote}
%
You can tell that this argument is valid even if you don't understand the
zoological terms, because every argument of the same \emph{logical form} is
valid. The relevant logical form might be expressed as follows.
%
\begin{quote}
  All $F$ are $G$.\\
  Some $H$ are $F$.\\
  Therefore: Some $H$ are $G$.
\end{quote}
%
No matter what descriptive terms you plug in for $F$, $G$, and $H$, you get a
valid argument. The argument about myriapods is therefore not just valid, but
\emph{logically valid} -- valid in virtue of its logical form.

% The case for formal languages

In natural languages like English, the logical form of sentences is not always
transparent. `Every dog barked at a tree' can mean either that there is a single
tree at which every dog barked, or that for each dog there is a tree at which it
barked. The two readings have different logical consequences, so it would be
good to keep them apart. Worse, the meaning of logical expressions (`all',
`some', `and', etc.) in natural language is often unclear and complicated. `Paul
and Paula got married and had children' suggests that the marriage came before
the children. In `Paul went to the zoo and Paula stayed at home', the word `and'
does not seem to have this temporal meaning.

To get around these problems, we invent formal languages in which there are no
ambiguities of logical form and in which all logical expressions have
determinate, precise meanings. If we want to evaluate natural-language arguments
for logical validity, we first have to translate them into the formal language.
(Sometimes an argument will be valid on one translation and invalid on another.)
With some practice, one can also reason directly in a formal language.

% A modal argument

Now consider the following argument.
%
\begin{quote}
  It might be raining.\\
  It is certain that we will  get wet if it is raining.\\
  Therefore: We might get wet.
\end{quote}
%
The argument looks valid. Indeed, any argument of this form is plausibly valid:
\begin{quote}
  It might be that $A$.\\
  It is certain that $B$ if $A$.\\
  Therefore: It might be that $B$.
\end{quote}
But it's hard to bring out the validity of these arguments in classical
propositional or predicate logic. We need formal expressions corresponding to
`it might be that' and `it is certain that'. The languages of classical
logic do not have such expressions.

% The standard languages of modal logic

So let's add them. Let's invent a new formal language with two new logical
symbols. It doesn't matter what these look like; a popular choice is a
diamond $\Diamond$ and a box $\Box$. We use the diamond to formalize `it might be
that', and the box for `it is certain that'.

If we add these symbols to the language of propositional logic, we get the
standard language of modal propositional logic. If we add them to the language
of predicate logic, we get the standard language of modal predicate logic. We
will stick with propositional logics until chapter \ref{ch:qml}.

% Translating the modal argument

% We can translate the above argument into the language of modal propositional
% logic, using $r$ to mean that it is raining and $w$ that we will get wet.
% \begin{quote}
%   $\Diamond r$\\
%   $\Box(r \to w)$\\[-3mm]
%   \rule{2cm}{0.2mm}\\
%   $\Diamond w$
% \end{quote}

% A formal definition

Let's officially define the standard language of modal propositional logic.

\begin{definition}{The language $\L_{M}$}{LM}
  A \emph{sentence letter} of $\L_{M}$ is any lower-case letter of the Latin
  alphabet ($a,b,c,\ldots,z$), possibly followed by numerical subscripts
  ($a_{1}, p_{18}, \ldots$). 

  A \emph{sentence} of $\L_{M}$ is either a sentence letter of $\L_{M}$ or an
  expression of the form $\neg A$, $(A \land B)$, $(A \lor B)$, $(A \to B)$,
  $(A \leftrightarrow B)$, $\Box A$, or $\Diamond A$, where $A$ and $B$ are
  $\L_{M}$-sentences.
\end{definition}

% Some conventions

I use lower-case letters $a,b,c,\ldots$ as atomic $\L_{M}$-sentences and
upper-case letters $A,B,C,\ldots$ when I want to talk about arbitrary
$\L_{M}$-sentences. To reduce clutter, I generally omit outermost parentheses
and quotation marks when I mention $\L_{M}$-symbols or sentences: $p \land q$ is
treated as an abbreviation of `$(p \land q)$'.

\begin{exercise}
  Which of these are $\L_M$-sentences?
  \begin{exlist}
  \item $p$
  \item $\Diamond$
  \item $\Diamond p \lor (\Box p \to p)$
  \item $\Box \Box p$
  \item $\Box A \to A$
  \item $(\Diamond r \land \Diamond qr) \land \Diamond \Box\Diamond\Box p$
  \end{exlist}
\end{exercise}
\begin{solution}
  (a), (c), and (d) are $\L_{M}$-sentences, (b), (e), and (f) are not.
\end{solution}

% Outstanding tasks

Having new symbols is only the beginning. We also need to lay down 
rules for reasoning with these symbols. The rules should be motivated by
what the symbols are supposed to mean. So we shall also assign a more precise
meaning to the diamond and the box -- just as classical logic assigns a precise
meaning to the symbol $\land$ that may or may not exactly match the meaning of
`and' in English.

% Truth tables

The meaning of $\land$ can be given by a \emph{truth table}:
\begin{center}
  \begin{tabular}{cc|ccccc}
    A & B & $A \land B$ \\\hline
    T & T & T\\
    T & F & F\\
    F & T & F\\
    F & F & F
  \end{tabular}
\end{center}
This tells us how the truth-value of $A \land B$ depends on the truth-value of
$A$ and $B$: the compound sentence is true iff (if and only if) both of its
subsentences are true. If you know this, you know all there is to know about the
meaning of $\land$. (You can see, for example, that $A \land B$ does not imply
anything about the temporal order of $A$ and $B$.)

\begin{exercise}
  Draw the truth tables for $\neg, \lor, \to$, and $\leftrightarrow$.
\end{exercise}
\begin{solution}
  Here is a combined truth table for all the classical connectives: 
  \begin{center}
    \begin{tabular}{cc|ccccc}
      A & B & $\neg A$ & $A \land B$ & $A\lor B$ & $A\to B$ & $A\leftrightarrow B$\\\hline
      T & T & F & T & T & T & T\\
      T & F & F & F & T & F & F\\
      F & T & T & F & T & T & F\\
      F & F & T & F & F & T & T\\
    \end{tabular}
  \end{center}
\end{solution}

% Truth-functionality

The sentence operators (or connectives) of classical propositional logic
($\neg, \land, \lor, \to$, and $\leftrightarrow$) are all truth-functional. Recall
that an operator is \textbf{truth-functional} if the truth-value of a compound
sentence formed by applying the operator to other sentences is always determined
by the truth-value of these other sentences. The truth tables for the classical
operators spell out this dependence. They tell us how to compute the truth-value
of a compound sentence from the truth-values of its constituents.

% 'Might' is not truth-functional

The diamond operator can't be truth-functional if it is supposed to mean
anything like `it might be that' in English. To see why, note first that `it
might be that $P$' can be true if $P$ is true, but also if $P$ is false. `It
might be raining' doesn't entail that it is actually raining, nor that it isn't
raining. It merely says that our evidence is compatible with rain. Now, if the
diamond were truth-functional, then what would follow from the fact that
$\Diamond p$ is \emph{sometimes} true when $p$ is true? It would follow that
$\Diamond p$ is \emph{always} true when $p$ is true. (Make sure you understand
why.) Likewise, from the fact that $\Diamond p$ is sometimes true when $p$ is
false, it would follow that $\Diamond p$ is true whenever $p$ is false.
$\Diamond p$ would be a logical truth. But `it might be raining' is surely not a
logical truth.

% \begin{exercise}\label{ex:might-truth-func}
%   Explain why the $\Diamond$ operator that formalises `it might be that' is not truth-functional.
% \end{exercise}
% \begin{solution}
%   In most situations, there are false propositions $P$ for which `it might be
%   that $P$' is true (because we are not omniscient) and other false propositions
%   $Q$ for which `it might be that $Q$' is false (because there are at least some truths we actually know).
% \end{solution}

% Possible worlds

If an operator isn't truth-functional, its meaning can't be defined by a truth
table. The standard approach to defining the meaning of modal operators instead
involves the concept of possible worlds. Roughly, we'll interpret $\Diamond A$
as saying that $A$ is true at some possible world, and $\Box A$ as saying that
$A$ is true at all possible worlds. Much more on this later.

\begin{exercise}\label{ex:truth-func}
  Which of these English expressions are truth-functional?
  \begin{exlist}
  \item It used to be the case that \ldots
  \item It is widely known that \ldots
  \item It is false that \ldots
  \item It is necessary that \ldots
  \item I can see that \ldots
  \item God believes that \ldots
  \item Either 2+2=4 or it is practically feasible that \ldots
  \end{exlist}
\end{exercise}
\begin{solution}
  An operator $O$ is truth-functional if you can figure out the
  truth-value of $Op$ from the truth-value of $p$.

  (c) and (g) are truth-functional; (a), (b), (d), and (e) are not
  truth-functional.

  (f) is truth-functional if God is omniscient (and infallible); it is also
  truth-functional if God doesn't exist, or if God believes all and only false
  things; otherwise (f) is not truth-functional.
\end{solution}

\section{Flavours of modality}
\label{sec:flavours}

% Historically, modal logic grew out of the study of necessity and contingency,
% which medieval logicians regarded as ``modes of truth''. Hence the name `modal
% logic'. Today, the study of necessity and contingency is but one of many
% subfields within modal logic. To a first (and rough) approximation, any part of
% logic that involves \emph{non-truth-functional sentence operators} is part of
% modal logic.

% Epistemic modality

`It might be that' and `it is certain that' express an \emph{epistemic} kind of
possibility and necessity, related to evidence and knowledge. There are other
kinds -- or \emph{flavours} -- of possibility and necessity.

% Deontic modality

Consider `John must leave'. This expresses a kind of necessity, but it would
typically not be understood as a statement about the available evidence. On its
most natural interpretation, it says that some relevant norms require John to
leave. This flavour of necessity is called \emph{deontic} (from Greek
\emph{deontos}: `of that which is binding').

% Circumstancial modality

Other statements about possibility and necessity are neither deontic nor
epistemic. If I say that you can't travel from Auckland to Sydney by train, I
don't just mean that my information implies that you won't make that journey;
nor do I mean that you're not permitted to make it. Rather, I mean that relevant
circumstances in the world -- such as the presence of an ocean between Auckland
and Sydney -- preclude the journey. This flavour of modality is sometimes called
\emph{circumstantial}. It comes in many sub-flavours, depending on what kinds of
circumstances are in play.

% In natural language, modals often have a mixed flavour. E.g. "I have to go
% now", "I can pick you up from the station", "I can't stay", "I'll do it as
% soon as possible", "the food is edible".

% Flavoured logics

Each of these flavours of modality corresponds to a branch of modal logic.
\emph{Epistemic logic} formalizes reasoning about knowledge and information.
\emph{Deontic logic} deals with norms, permissions, and obligations. A third
branch of modal logic might be called \emph{circumstantial logic}, but nobody
uses that label. Some authors speak of \emph{alethic modal logic} (from
\emph{aletheia}: `truth'), but this label is also not used widely, and it is
used for different things by different authors.

% The division into epistemic, deontic, and alethic logic was made popular in \cite{wright51essay}

% Metaphysical modality

Confusingly, some philosophers use `modal logic' for the logic of a certain
sub-flavour of circumstantial modality, known as \emph{metaphysical} modality.
Metaphysical modality is concerned with what is or isn't compatible with the
nature of things. We will follow the more common practice of using `modal logic'
as an umbrella term that covers all the applications I have mentioned, as well
as many others.

% Preview

We will take a closer look at epistemic logic in chapter \ref{ch:epistemic} and
at deontic logic in chapter \ref{ch:deontic}. In chapter \ref{ch:time} we are
going to study a branch of modal logic called \emph{temporal logic} that is
concerned with reasoning about time. Chapter \ref{ch:conditionals} is on
\emph{conditional logic}. Here we will introduce (non-truth-functional)
two-place operators that are meant to formalise certain `if \ldots then \ldots'
constructions in English. In chapter \ref{ch:proofs}, we will briefly look at
\emph{provability logic}, which investigates formal properties of mathematical
provability. What unifies the different branches of modal logic is not a
particular subject matter, but a loosely defined collection of abstract ideas
and techniques that turn out to be useful in all these applications.

% Boxes and diamonds

When we study some flavour of possibility or necessity, the diamond $\Diamond$
is generally used for the relevant kind of possibility and the box $\Box$ for
the corresponding kind of necessity. In this context, you may pronounce the
diamond `it is possible that' and the box `it is necessary that'. In general,
however, I would recommend pronouncing the diamond `diamond' and the box `box'.

% A variety of logics

Different interpretations of the box and the diamond often motivate different
rules for reasoning with these expressions. Consider, for example, the inference
from $\Box p$ to $p$. If the box expresses a circumstantial kind of necessity,
then this inference is plausibly valid: if the circumstances ensure that
something is the case, then it really is the case. On a deontic reading of the
box, by contrast, the inference is invalid. We can easily imagine scenarios in
which, say, it is required that all library books are returned on time
($\Box p$) and yet it is not the case that all library books are returned on
time ($\neg p$).

So we can't say, once and for all, whether $\Box p$ entails $p$. We will develop
different ``logics'' or ``systems'' of modal logic. In some systems, the inference is
valid, in others it is invalid.

% English modals

The diamond and the box are sentence operators. English expressions for
necessity and possibility often don't have this form. We can talk about what's
necessary or possible using `must', `might', or `can', which are (auxiliary)
verbs. We can also use adjectives like `feasible', `certain', and 'obligatory',
or adverbs like `possibly', `certainly', and `inevitably'.

% Translating from English

When translating from English into $\L_{M}$, it is often helpful to first
paraphrase the English sentence with `it is necessary that' and `it is possible
that' (or other suitable sentence operators). For example,
\begin{quote}
  You can't go from Auckland to Sydney by train
\end{quote}
might be paraphrased as
\begin{quote}
  It is not possible [in light of relevant circumstances] that you go from
  Auckland to Sydney by train
\end{quote}
An adequate translation is $\neg\Diamond p$, where $p$ represents `you go from
Auckland to Sydney by train' and the diamond represents the relevant kind of
circumstantial possibility.

\begin{exercise}
  Translate the following sentences, as well as possible, into $\L_{M}$,
  assuming that the diamond expresses epistemic possibility (`it might be that')
  and the box epistemic necessity (`it must be that').
  \begin{exlist}
  \item I may have offended the principal.
  \item It can't be raining.
  \item Perhaps there is life on Mars.
  \item If the murderer escaped through the window, there must be
    traces on the ground.
    % Against narrow scope: e->[]t together with <>-t logically
    % entails -e. And in the context, <>-t is plausibly true. But it
    % would be wrong to infer -e.
  \item If the murderer escaped through the window, there might be
    traces on the ground.
  \end{exlist}
\end{exercise}
\begin{solution}
  \begin{sollist}
    \item $\Diamond p$ \quad  $p$: I offended the principal.
    \item $\neg \Diamond p$ \quad  $p$: It is raining.
    \item $\Diamond p$ \quad  $p$: There is life on Mars.
    \item $\Box(p \to q)$ \quad  $p$: The murderer escaped through the window; $q$: There are traces on the ground.
    \item $\Diamond(p \land q)$ \quad $p$: The murderer escaped through the window; $q$: There are traces on the ground.
  \end{sollist}
\end{solution}

\begin{exercise}
  Translate the following sentences, as well as possible, into $L_{M}$, assuming
  that the diamond expresses deontic possibility (`it is permitted that') and
  the box deontic necessity (`it is obligatory that').
  \begin{exlist}
  \item I must go home.
  \item You don't have to come.
  \item You can't have another beer.
  \item If you don't have a ticket, you must pay a fine.
  % This plausibly has two readings, one with an epistemic must, another with
  % the deontic must restricted by the conditional. How do they come apart?
  % Imagine everyone who doesn't have to pay a fine is handed a "ticket" for the
  % no-fine queue. There is no rule that those without a ticket have to pay a
  % fine. Then [](~t -> f) is plausibly false, but ~t -> []f is true. For the
  % converse direction, normally we'd assume that it's a matter or law that
  % whoever doesn't have a ticket must pay a fine. So [](~t -> f) would seem
  % correct. In that case ~t -> []f often will also seem fine, because we are
  % restricting the domain of relevant worlds by the facts about whether you
  % have a ticket: i.e., given that ~t is true, it is also true among the worlds
  % over which the box ranges, and so []f will be true. To make the narrow-scope
  % reading false, we'd have to imagine a scenario in which we don't hold fixed
  % whether you have a ticket when we evaluate the modal.
  % 
  % \item You need a special visa to enter Chukotka.
  \end{exlist}
\end{exercise}
\begin{solution}
  \begin{sollist}
    \item $\Box p$ \quad  $p$: I go home.
    \item $\neg \Box p$ \quad  $p$: You come.
    \item $\neg\Diamond p$ \quad  $p$: You have another beer.
    \item $\Box(\neg p \to q)$ \quad  $p$: You have a ticket; $q$: You pay a fine.
  \end{sollist}
\end{solution}

\begin{exercise}
  Translate the following sentences, as well as possible, into $L_{M}$, assuming
  that the diamond expresses (some relevant sub-flavour of) circumstantial
  possibility and the box circumstantial necessity.
  \begin{exlist}
  \item I could have studied architecture.
  % \item It's impossible for me to both cook and entertain the children.
  \item The bridge is fragile.
  \item I can't hear you if you're talking to me from the kitchen. 
  \item If you have a smartphone, you can use an electronic ticket.
  % Here `can' plausibly expresses some kind of circumstantial possibility.
  % Again, we have to choose between two formalizations: $\Diamond(p \to q)$ and
  % $p \to \Diamond q$, where $p$ represents you having a smartphone and $q$
  % using an electronic ticket. In this case, the second formalization is
  % arguably better. The statement plausibly does say that if you have a
  % smartphone, then the following is possible, in a relevant circumstantial
  % sense: you use an electronic ticket.
    
  \end{exlist} 
\end{exercise}
\begin{solution}
  \begin{sollist}
    \item $\Diamond p$ \quad  $p$: I study architecture.
    % Notice the fake past in the English sentence.
    \item $\Diamond p$ \quad  $p$: The bridge collapses.
    \item $\neg\Diamond(p \land q)$ \quad  $p$: You are talking to me from the kitchen; $q$: I hear you.
    \item $p \to \Diamond q$ \quad $p$: You have a smartphone; $q$: You use an electronic ticket.
  \end{sollist}
\end{solution}

% Conditionals

Special care is required when translating English sentences that contain both
modal expressions and an `if' clause. The surface form of English can be
misleading. A good strategy is to first rephrase the English sentence so that it
no longer contains any conditional expression, then translate that paraphrase.
The paraphrase, and therefore the translation, will often sound rather unlike
the original sentence, but that's OK. What's important is that it has the same
truth-conditions. There should be no conceivable scenario in which the original
sentence is true and the paraphrase (or translation) false, or the other way
round.

\section{The turnstile}
\label{sec:turnstile}

In section \ref{sec:intro}, I said that an argument is valid if there is no
conceivable scenario in which the premises are true and the conclusion is false.
An argument is logically valid, I said, if it is valid ``in virtue of its
logical form''. Can we make this more precise?

Consider this English argument.
%
\begin{quote}
  Some cats are black.\\
  Therefore: Some animals are black.
\end{quote}
%
The argument is valid, but not logically valid. Its validity turns on the
meaning of `cat', which we don't consider a logical expression.

To bring out how the argument's validity depends on the meaning of `cat', we can
imagine a language that is much like English except that `cat' means
\emph{chair}. In this language, the argument just displayed is invalid. It is
invalid because there are conceivable scenarios in which there are black chairs
but no black animals. In any such scenario, the argument's premise is true (in
our imaginary language) while the conclusion is false.

When we say that an argument is valid ``in virtue of its logical form'', we mean
that its validity does not depend on the meaning of the non-logical expressions.
In other words, there is no conceivable scenario in which the premises are true
and the conclusion is false, \emph{no matter what meaning we assign to the
  non-logical expressions}.

The concept of validity for arguments is closely related to that of entailment.
If an argument is valid, we say that the premises entail the conclusion. If an
argument is logically valid, we say that the premises logically entail the
conclusion. In logic, we're interested in logical entailment. We adopt the
following definition.

\begin{definition}{}{entailment-informal}
  Some sentences $\Gamma$ ('gamma') \textbf{(logically) entail} a sentence $A$
  iff there is no conceivable scenario in which all sentences in $\Gamma$ are
  true and $A$ is false, under any interpretation of the non-logical
  expressions.
\end{definition}

Instead of saying that the sentences $\Gamma$ logically entail $A$, we also say
that $A$ is a \emph{logical consequence of} $\Gamma$, or that $A$
\emph{logically follows from} $\Gamma$. Two sentences are \emph{(logically)
  equivalent} if either logically follows from the other.

Logicians often use the symbol `$\models$' (the ``double-barred turnstile'') for
entailment. The claim that $\Box (p \to q)$ and $\Box p$ together entail $q$,
for example, could be expressed as
\begin{equation*}
  \Box (p \to q), \Box p \models q.
\end{equation*}

This is not a sentence of $\L_{M}$. The comma and the turnstile belong to
the \textbf{meta-language} we use to talk about the \textbf{object language}
$\L_M$. (The rest of our meta-language is mostly English.) We use the turnstile
to express a certain relationship between $\L_M$-sentences, not to construct
further $\L_{M}$-sentences.

\begin{exercise}
  % If we are allowed to re-interpret the non-logical expressions, do we even need
  % to consider alternative scenarios? 
  What do you think of this simpler alternative to definition
  \ref{def:entailment-informal}? ``Sentences $\Gamma$ entail a sentence $A$ iff
  there is no interpretation of non-logical expressions that renders all
  sentences in $\Gamma$ true and $A$ false.''
\end{exercise}
\begin{solution}
  The proposed definition is equivalent to definition
  \ref{def:entailment-informal} for many languages, but not for all. Consider
  the sentence $\exists x \exists y \neg(x = y)$ in the language of predicate
  logic. If we treat the identity symbol as logical, this sentence contains no
  non-logical expressions at all. And the sentence is true, because there is in
  fact more than one object. So the sentence is true under any interpretation of
  its non-logical vocabulary. But it's not logically true; it doesn't logically
  follow from any premises whatsoever. The sentence is false in any scenario in
  which there is only one object.
  % For another example, if there is actually just one object, then the proposed
  % definition would imply that Fa entails Fb. 
\end{solution}

The following fact about logical consequence often proves useful.

\begin{observation}{semantic-deduction-theorem}
  If $A$ and $B$ are sentences and $\Gamma$ is a (possibly empty) list of sentences, then
  \vspace{-1mm}
  \[
    \Gamma,A \models B \text{ \;iff\; }\Gamma \models A \to B.
  \]
  \vspace{-5mm}
\end{observation}
%
\begin{proof}
  \emph{Proof}. Look at the statement on the right-hand side of the `iff'.
  `$\Gamma \models A \to B$' says that there is no conceivable scenario in which
  all sentences in $\Gamma$ are true while $A\to B$ is false, under any
  interpretation of the non-logical expressions. By the truth-table for `$\to$',
  $A\to B$ is false iff $A$ is true and $B$ is false. So we can rephrase the
  statement on the right-hand side as saying that there is no conceivable
  scenario and interpretation that makes all sentences in $\Gamma$ true and
  $A$ true and $B$ false. That's just what the statement on the left-hand
  side asserts. \qed
\end{proof}

Observation \ref{obs:semantic-deduction-theorem} tells us that if we start with
a claim of the form $A_{1},A_{2},A_{3}\ldots \models B$, we can always generate
an equivalent claim by moving the turnstile to the left of the sentence that
precedes it and putting an arrow in its original place. For example, instead of
\begin{equation*}
  \Box (p \to q), \Box p \models \Box q
\end{equation*}
we can equivalently say
\begin{equation*}
  \Box (p \to q) \models \Box p \to \Box q.
\end{equation*}
We can go further to
\begin{equation*}
  \models \Box (p \to q) \to (\Box p \to \Box q).
\end{equation*}
This says that $\Box (p \to q) \to (\Box p \to \Box q)$ logically follows from
no premises at all. A sentence that follows from no premises is called
\emph{logically true} or \emph{(logically) valid}.

(So an \emph{argument} is called valid if the conclusion follows from the
premises, while a \emph{sentence} is called valid if it follows from no
premises.)

Sentence validity is implicitly covered by definition
\ref{def:entailment-informal}, using an empty list of sentences for $\Gamma$.
But it's worth making the definition more explicit.
%
\begin{definition}{}{valid-informal}
  A sentence $A$ is \textbf{valid} (for short, $\models A$) iff there is no
  conceivable scenario in which $A$ is false, under any interpretation of the
  non-logical expressions.
\end{definition}

Make sure you don't confuse the arrow with the turnstile. It's not just that the
two symbols belong to different languages -- one to $\L_{M}$, the other to our
meta-language. They also have very different meanings. $p \to q$ is true iff
either $p$ is false or $q$ is true (or both). $p \models q$, on the other hand,
is true iff there is no conceivable scenario in which $p$ is true and $q$ is
false, under any interpretation of $p$ and $q$. Nonetheless, there is an
important connection between the arrow and the turnstile: $A \models B$ is
\emph{true} iff $A \to B$ is \emph{valid}.

The definitions of this section are still somewhat imprecise. Eventually we will
want to prove various claims about entailment and validity. To this end, we will
need to give rigorous meanings to `conceivable scenario' and `interpretation of
non-logical expressions'. Let's leave this task until the next chapter.

% \begin{exercise}
%   We can generalise our interpretation of the double-barred turnstile. Let's
%   read `$\ldots \models \ldots$' as saying that there is no scenario and
%   interpretation (of the non-logical expressions) that makes everything on the
%   left of the turnstile true while making everything on the right false. On this
%   interpretation, what do the following statements mean? (a)
%   `$p \lor \neg p \models$' (b) `$p \models p,q$', (c) `$\models$'? Which of
%   them are true?
% \end{exercise}

\section{Duality}%
\label{sec:duality}

% Two translations

`Neville can't be the murderer', says Watson. His claim could be paraphrased as
`it is not possible that Neville is the murderer'. This suggests that
$\neg\Diamond p$ is an adequate translation (where $p$ expresses that Neville is
the murderer). But Watson's claim might also be paraphrased as `it is certain
that Neville is not the murderer', which we might translate as $\Box\neg p$.

% Equivalence

The two paraphrases are plausibly equivalent. In general, `it is not
(epistemically) possible that $A$' seems to say the same as `it is certain that
not $A$'. Similarly, `it is not certain that $A$' arguably says the same as `it
is possible that not $A$'.

% Dual1 and Dual2

Whether or not the equivalence holds in English, we stipulate that it holds in
$\L_{M}$: for any $\L_{M}$-sentence $A$,
%
\begin{principles}
\pri{Dual1}{\neg \Diamond A \text{ is equivalent to } \Box \neg A};\\
\pri{Dual2}{\neg \Box A \text{ is equivalent to } \Diamond \neg A}.
\end{principles}

% Dual operators

Operators that stand in the relationship expressed by \pr{Dual1} and \pr{Dual2}
are called \textbf{duals} of each other. There is a convention in modal logic to
use the symbols $\Box$ and $\Diamond$ only for concepts that are duals of each
other.

\begin{exercise}
  Find all pairs of duals among the following English expressions.
  \begin{exlist}
  \item It is necessary that \ldots
  \item It is impossible that \ldots
  \item It is possible that \ldots
  \item It is possibly not the case that \ldots
  % \item It is neither necessary nor impossible that \ldots
  \item It was at some point the case that \ldots
  \item It will at some point be the case that \ldots
  \item It has always been the case that \ldots
  \item It will always be the case that \ldots
  \item The law requires that \ldots
  \item The law does not require that \ldots
  \item The law allows that \ldots
  \item It is true that \ldots
  \item It is false that \ldots
  \end{exlist}
\end{exercise}
\begin{solution}
  The following pairs are duals: (a) and (c), (b) and (d), (e) and
  (g), (f) and (h), (i) and (k), (l) and (l), (m) and (m).
\end{solution}

% An equivalence

\pr{Dual1} implies that $\neg\Diamond\neg p$ is equivalent to $\Box\neg\neg p$,
choosing $\neg p$ as the sentence $A$. In standard modal logic, logically
equivalent expressions are interchangeable.\label{claim:replacement} So we can
simplify $\Box \neg\neg p$ to $\Box p$, drawing on the equivalence between
$\neg\neg p$ and $p$. So $\neg\Diamond\neg p$ is equivalent to
$\Box p$.

% Generalised equivalences

The same reasoning could be applied to any other sentence $A$ in place of
$p$. \pr{Dual1} therefore implies that for any sentence $A$,
\[
   \Box A\text{ is equivalent to }\neg\Diamond\neg A.
\]
In the same way, \pr{Dual2} implies that (for any sentence $A$)
\[
   \Diamond A\text{ is equivalent to }\neg\Box\neg A.
\]

% Redundancy

This shows that the box and the diamond can be defined in terms of one another.
We could have used a language whose only primitive modal operator is the box,
and read $\Diamond A$ as an abbreviation of $\neg\Box\neg A$. Alternatively, we
could have used the diamond as the only primitive modal operator and read
$\Box A$ as an abbreviation of $\neg\Diamond\neg A$.

\begin{exercise}
  Which of these sentences are equivalent to $\Diamond\Diamond \neg p$? (a)
  $\Diamond \neg \Diamond p$, (b) $\Diamond\neg \Box p$, (c)
  $\neg\Box\Diamond p$, (d) $\neg\Diamond\Box p$, (e) $\neg\Box\Box p$
\end{exercise}
\begin{solution}
  (b) and (e) are equivalent to $\Diamond\Diamond \neg p$, (a), (c), and (d) are
  not.
  
  As a rule, you can always replace a modal operator by its dual, insert a
  negation on both sides, and remove any double negations to get an equivalent
  sentence.
\end{solution}

% Does 'possible' imply 'not necessary'?

A digression: you might think that there is another connection between `possible' and
`necessary'. When we say that something is possible (or that it might be the
case), we often convey that it is not necessary (or not certain). This suggests
that $\Diamond p$ entails $\neg \Box p$. We've just assumed, however, that
$\Diamond p$ is equivalent to $\neg \Box \neg p$. If $\Diamond p$ entails
$\neg \Box p$, we would have to conclude that $\neg\Box\neg p$ entails
$\neg\Box p$. By contraposition, we could infer that $\Box p$ entails
$\Box \neg p$. But `it is necessary that $P$' surely doesn't entail `it is
necessary that not-$P$'!

% A choice

We have to reject either the duality of `possible' and `necessary' or the
apparent entailment from `possible' to `not necessary'. On reflection, the case
for duality is stronger. There is a good explanation of why `possible' often
\emph{appears} to entail `not necessary' even if it actually doesn't.

% An example.

Take an example. Suppose Watson says `Neville might be the murderer'. Let's
assume that `might' is the dual of `certain', so that `it might be that $P$' is
equivalent to `it is not certain that not $P$'. On this interpretation, what
Watson said -- that Neville might be the murderer -- is merely that it isn't
certain that Neville is \emph{not} the murderer. It may well be certain that
Neville \emph{is} the murderer. Why, then, does his statement convey that
Neville's guilt is an open question?

% A pragmatic explanation

Well, suppose Watson had known that Neville is the murderer. In that case, he
shouldn't have said `Neville might be the murderer'. These words would still
have been true -- or so we assume -- but they would not have been helpful.
Watson would have been in a position to say something more informative: that
Neville is the murderer, or that he is known to be the murderer. We generally
assume that speakers are trying to be helpful, that they are not hiding relevant
information. Assuming that Watson is trying to be helpful, his \emph{statement}
that Neville might be the murderer implies that he considers Neville's guilt an
open question. This follows not from \emph{what he said}, but from the fact
\emph{that he said it}, together with the assumption that he is trying to be
helpful.

% Scalar implicature

This kind of effect is studied in the field of pragmatics, where it is known as
a \emph{scalar implicature}. Scalar implicatures arise when an utterance of a
logically weaker sentence conveys that a certain stronger sentence is false.
`Some students passed the test', for example, conveys that not all students
passed the test, although the statement would be true even if all students had
passed. In that case, however, it would not have been helpful: the speaker
should have used `all students passed'.
End of digression.

% Schemas

I want to say a little more about duality. To do so, I need to introduce the
concept of a schema.

% I already mentioned that I use upper-case letters $A,B,C,\ldots$ when I want to
% talk about arbitrary $\L_{M}$-sentences. Above, for example, I said that we
% could have read $\Diamond A$ as an abbreviation of $\neg\Box\neg A$. By this, I
% mean that we could have read $\Diamond p$ as an abbreviation of
% $\neg\Box\neg p$, $\Diamond (p \lor q)$ as an abbreviation of
% $\neg\Box\neg (p \lor q)$, and so on, for all $\L_{M}$-sentences. The
% expressions `$\Diamond A$' and `$\neg\Box\neg A$' are schemas.

Formally, a \textbf{schema} (for $\L_{M}$-sentences) is simply an
$\L_{M}$-sentence with upper-case schematic variables in place of sentence
letters. Every $\L_{M}$-sentence that results from a schema by (uniformly)
replacing the schematic variables with object-language sentences is called an
\textbf{instance} of the schema.

% An example

$\Box A \to A$, for example, is a schema. Three of its instances are
$\Box p \to p$ and $\Box (p \lor q) \to (p \lor q)$ and
$\Box \Box p \to \Box p$. The sentence $\Box p \to q$ is not an instance: the
same schematic variable must always be replaced by the same object-language
sentence. (That's what I meant by ``uniformly''.)

\begin{exercise}
  Which of the following expressions are instances of
  $\Box(A\to \Diamond (A \land B))$?
  \begin{exlist}
  \item $\Box(p \to \Diamond (q\land p))$
  \item $\Box(\Diamond p \to \Diamond (\Diamond p\land p))$
  \item $\Box\Box(p \to \Diamond (p \land q))$
  \item $\Box((p \to \Diamond (p \land q)) \to \Diamond((p \to \Diamond (p \land q)) \land \Diamond p))$
  \item $\Box((A\land C) \to \Diamond ((A\land C) \land (B\land C)))$
  \end{exlist}
\end{exercise}
\begin{solution}
  (b) and (d)
\end{solution}

% Use of schemas

Schemas are useful when we want to talk about all $\L_{M}$-sentences of a
certain form. In the next section, for example, we are going to define a system
of modal logic by giving a list of schemas all instances of which are considered
valid.

% Dual schemas

Now compare the schemas $\Box A \to A$ and $A \to \Diamond A$. Given the duality
of the box and the diamond, and the fact that logically equivalent expressions
can be freely exchanged for one another, we can show that \emph{every instance
  of one of them is equivalent to an instance of the other}. In this sense, the
two schemas are equivalent. And because their equivalence relies on the duality
of the box and the diamond, the two schemas are called duals of one another.

% Proof of duality

To see why every instance of $\Box A \to A$ is equivalent to an instance of
$A \to \Diamond A$, take a simple instance: $\Box p \to p$. By the truth-table
for the arrow, this is equivalent to $\neg p \to \neg \Box p$. By \pr{Dual2},
$\neg \Box p$ is equivalent to $\Diamond \neg p$. So $\neg p \to \neg \Box p$ is
equivalent to $\neg p \to \Diamond \neg p$. And this is an instance of
$A \to \Diamond A$. The same line of reasoning obviously works for any other
sentence in place of $p$, and a similar line of reasoning shows the converse,
that every instance of $A \to \Diamond A$ is equivalent to an instance of
$\Box A \to A$.

% Instances not equivalent

It's crucial that we're talking about schemas here. We have not shown that the
\emph{sentence} $\Box p \to p$ is equivalent to $p \to \Diamond p$. In fact, the
duality principles and the replacement of equivalents don't suffice to show that
these sentences are equivalent.

% Equivalence of axioms

The equivalence of the \emph{schemas}, however, is enough to show that it
doesn't matter which of them we use when we list schemas to define a logic. We
can say that all instances of $\Box A \to A$ are valid in a certain logic, or we
can say that all instances of $A \to \Diamond A$ are valid -- it amounts to the
same thing, because every instance of either schema is equivalent to an instance
of the other.

% Generalising 

The equivalence between $\Box A \to A$ and $A \to \Diamond A$ is an example of
a more general pattern. Any schema with an arrow ($\to$ or $\leftrightarrow$) as
the only truth-functional operator can be converted into an equivalent schema --
its \textbf{dual} -- by swapping antecedent and consequent and replacing every
box with a diamond and every diamond with a box. 

% More generally, the dual of a schema with -> as its main connective and no
% other -> is the schema in which antecedent and consequent are interchanged and
% & and v and [] and <> are swapped by one another. (To find the dual of e.g. GL
% first replace an embedded -> by not or.)

\begin{exercise}
 Find the duals of (a) $\Box A \to \Box\Box A$, (b) $\Diamond A \to \Box\Diamond A$, (c) $\Box A \to \Diamond A$.
\end{exercise}
\begin{solution}
  (a) $\Diamond\Diamond A \to \Diamond A$, (b) $\Diamond\Box A \to \Box A$, (c)
  $\Box A \to \Diamond A$.
\end{solution}

\begin{exercise}
  A proposition is \emph{contingent} if it neither necessary nor impossible. Let
  $\nabla$ be a sentence operator for `it is contingent that'. Reading the box as `it is necessary that' and the diamond as `it is possible that', try to find
  \begin{exlist}
    \item a sentence whose only modal operator is $\Box$ that is equivalent to
    $\nabla p$;
    \item a sentence whose only modal operator is $\Diamond$ that is equivalent to
    $\nabla p$;
    \item a sentence whose only modal operator is $\nabla$ that is equivalent to $\Box p$.
  \end{exlist}
\end{exercise}
\begin{solution}
  (a) $\neg \Box p \land \neg\Box\neg p$; (b)
  $\Diamond p \land \Diamond \neg p$; (c) $\neg\nabla p \land p$. The last
  answer assumes that every necessary proposition is true. Without that
  assumption there is no answer to (c). % as shown in \cite{cresswell1988necessity}
\end{solution}

\section{A system of modal logic}%
\label{sec:systems}

Whether a sentence is logically valid, or logically entailed by other sentences,
never depends on the meaning of the non-logical expressions. But it may well
depend on the meaning of the logical expressions. In modal logic, the box and
the diamond are treated as logical expressions, but their interpretation varies
from application to application. Sometimes the box means epistemic necessity,
sometimes it means deontic necessity, sometimes it means something else. As I
mentioned in section \ref{sec:flavours}, this has the consequence that we need
to distinguish different ``systems of modal logic''. In some applications, we
want $\Box p$ to entail $p$, in others we don't.

Suppose, now, that we want to fully spell out one of these ``systems''. We want
to completely specify which $\L_{M}$-sentences are valid, and which are entailed
by which others, on a particular understanding of the modal operators.

There are many ways of approaching this task. We could, for example, define
precise notions of conceivable scenarios and interpretations and apply the
definitions of the previous section. But let's choose a more direct route. When
we think about circumstantial necessity, we can intuitively see that $\Box p$
entails $p$, without going through sophisticated considerations about scenarios
and interpretations. Assume, then, that we simply start with direct judgements
about entailment and validity.

We still face a problem. There are infinitely many $\L_{M}$-sentences. We can't
look at every sentence and argument one by one. We need to find some
shortcuts.

We can begin by drawing on a consequence of observation
\ref{obs:semantic-deduction-theorem}. Above I said that in order to spell out a
system of modal logic, we need to specify (i) which $\L_{M}$-sentences are valid
and (ii) which $\L_{M}$-sentences are entailed by which others. Observation
\ref{obs:semantic-deduction-theorem} tells us that we can ignore part (ii) of
the task. Once we have fixed which sentences are valid, we have implicitly
also fixed which sentences entail which others. If, for example, we decide
that $\Box p \to p$ is valid, we have also decided that $\Box p$ entails $p$.

Our task of spelling out a system of modal logic therefore reduces to
the task of specifying which $\L_{M}$-sentences are valid. That's why a
\textbf{system of modal logic} is usually defined simply as a set of
$\L_{M}$-sentences.

To make this more concrete, let's look at a particular sub-flavour of
circumstantial necessity, sometimes called \emph{historical necessity}.
Something is historically necessary if it is ``settled'': it is true and there
is nothing anyone can do about it. Facts about the past are plausibly settled.
Nothing we can do is going to make a difference to what happened yesterday. By
contrast, some facts about the future are intuitively ``open''.

Let's use the box to formalise this (admittedly vague) concept of historical
necessity. So $\Box p$ says that $p$ is settled. Since the diamond is the dual
of the box, $\Diamond p$ expresses that it not settled that $p$ is false. In
other words, $p$ is either open or settled as true.

% Don't say: <>p means that p is open: otherwise []p -> <>p looks implausible.
% 'open' conveys 'could be made true and could be made false'.

Our task is to specify all $\L_{M}$-sentences that are valid on this
understanding of the box and the diamond. This will give us a system of modal
logic, a set of $\L_{M}$-sentences that are valid on a certain interpretation of
the box and the diamond. We want to know which sentences are in the system --
for short, which sentences are ``in'' -- and which are not.

If the box expresses historical necessity then $\Box p$ clearly entails $p$. So
$\Box p \to p$ is in. There is nothing special here about the sentence $p$.
Whatever is settled is true. Every instance of the schema $\Box A \to A$ is in.
(As mentioned in section \ref{sec:duality}, it follows that every instance of
$A \to \Diamond A$ is in as well.)

In the same vein, we may now look at other schemas. Arguably, all instances of
the following schemas -- listed here with their conventional names -- are valid,
and therefore in our target system:
%
\begin{principles}
  \pri{Dual}{\neg\Diamond A \leftrightarrow \Box\neg A}\\
  \pri{T}{\Box A \to A}\\
  \pri{K}{\Box(A\to B) \to (\Box A \to \Box B)}\\
  \pri{4}{\Box A \to \Box \Box A}\\
  \pri{5}{\Diamond A \to \Box \Diamond A}
\end{principles}

\pr{Dual} corresponds to the duality principle \pr{Dual1} from section
\ref{sec:duality}. Its instances are guaranteed to be valid by the fact that we
have introduced the diamond as the dual of the box.

We've already talked about \pr{T}.

\pr{K} is a little easier to understand as a claim about entailment:
\[
  \Box(A \to B), \Box A \models \Box B.
\]
On our present interpretation, this says that if a material conditional $A\to B$
is settled, and its antecedent $A$ is settled, then its consequent $B$ is
guaranteed to be settled as well. Why should we accept this? Let $A$ and
$B$ be arbitrary propositions, and assume that $A\to B$ and $A$ are both
settled. It follows that they are both true. Since $A\to B$ and $A$ entail $B$,
it follows that $B$ is true as well. Could it be that $B$ is true but open?
Arguably not: If we could bring about a situation in which $B$ is false then we
could also bring about a situation in which either $A\to B$ or $A$ is false,
since one of these is guaranteed to be false in any situation in which $B$ is
false. The assumption that $A\to B$ and $A$ are settled therefore implies that
$B$ is settled. So all instances of \pr{K} are in.

% If we read settled as 'unaffected by our beliefs, desires, and intentions',
% then Lycan claims that (K) is implausible. (Lycan 1994:186f., drawing on
% Slote 1982)

\pr{4} and \pr{5} assert that facts about what is settled are themselves
settled. \pr{4} says that if something is settled then it is settled that it is
settled. \pr{5} says that if something is not settled then it is settled that it
is not settled. Here it is important that we adopt a consistent point of view.
It is easy to think of situations in which something is open to us (say, we
could read a certain letter) and we can do something (say, burn the letter) that
would make it no longer open. This doesn't contradict \pr{5}, since \pr{5}
concerns what is open and settled \emph{now}. If something is now open, then
arguably there is nothing we can do that would change the fact that it is now
open. Likewise, if something is now settled, then arguably there is nothing we
can do that would change the fact that it is now settled.

I could have listed further schemas. For example, whenever a conjunction is
settled, then both its conjuncts are plausibly settled as well. So every
instance of $\Box(A\land B) \to (\Box A \land \Box B)$ should be in. There are,
in fact, infinitely many further schemas, not covered by the five above, whose
instances belong to our target system.

That's the bad news. The good news is that we don't need to list any of them. We
can replace the whole lot by specifying two rules for generating new sentences
from sentences we have already classified as ``in''.

The first of these rules captures the plausible thought that anything that
follows from a valid sentence by classical (non-modal) propositional logic is
itself valid. Since we've decided that $\Box p \to p$ is valid (in the logic of
historical necessity), we can, for example, infer that $(\Box p \to p) \lor q$
is also valid, because $A \lor B$ follows from $A$ in classical propositional
logic.
% By adopting this rule, we effectively assume that (i) the meaning of the
% truth-functional connectives is given by their standard truth tables, and that
% (ii) every sentence is either true or false and not both.
Our system of modal
logic thereby becomes an \textbf{extension} of classical propositional
logic. \label{claim:extension}

To state the rule concisely, let $\Gamma \models_{0} A$ mean that $A$ follows
from $\Gamma$ in classical propositional logic -- as can be determined, for
example, by the truth table method. Then our rule says that for any list of
sentences $\Gamma$ and any sentence $A$,
%
\begin{principles}
  \pri{CPL}{\text{If }\Gamma \models_{0} A\text{ and all members of }\Gamma\text{ are in, then }A\text{ is in}.}
\end{principles}

As a special case, \pr{CPL} implies that every propositional tautology is
``in'', since tautologies follow in classical propositional logic from any
premises whatsoever (and even from no premises).

Our second rule reflects the idea that all logical truths are settled: For any
sentence $A$,
%
\begin{principles}
  \pri{Nec}{\text{If $A$ is in, then }\Box A\text{ is in}.}
\end{principles}

% It is easy to see that these two rules generate infinitely many sentence schemas
% from any basis of axioms. Indeed (Nec) alone tells us that since (e.g.) all
% instances of []A->A are in S, so are all instances of []([]A->A), all instances
% of [][]([]A->A), and so on.

And now we're done. I claim -- and this may seem rather mysterious at the moment
-- that there is a natural understanding of historical necessity (of `settled')
on which the sentences that are valid in the logic of historical necessity are
precisely the sentences that can be generated from instances of \pr{T}, \pr{K},
\pr{4}, \pr{5} and \pr{Dual} by \pr{CPL} and \pr{Nec}. (In fact, \pr{4} is
redundant: any instance of \pr{4} can be derived from the remaining axioms and
rules.)

The system of modal logic defined by these schemas and  rules is perhaps the
best known of all systems of modal logic. Its conventional name is `S5' because
it was introduced as the fifth system in an influential list of systems
published by C.I.\ Lewis and C.H.\ Langford in 1932.

Other systems of modal logic can be defined by different schemas or rules.
Lewis and Langford's system S4, for example, is defined by \pr{T},
\pr{K}, \pr{4}, \pr{Dual}, \pr{CPL} and \pr{Nec}, without
\pr{5}. This system is adequate for other interpretations of the box and the
diamond, where we don't want to treat all instances of \pr{5} as valid.

\begin{exercise}
  Instead of reading the box as `it is settled that', we might give it one of these interpretations (with the diamond defined as the box's dual):
  \begin{exlist}
    \item it is true that
    \item it is false that
    \item it is either true or false that
    \item it is logically true that
  \end{exlist}
  \medskip\noindent%
  For each of these interpretations, evaluate whether the schemas \pr{T}, \pr{K}, \pr{4}, \pr{5}, and the rules \pr{CPL} and \pr{Nec} are plausible. 
\end{exercise}
\begin{solution}
  \begin{sollist}
  \item All of them.
  \item Only \pr{K} and \pr{CPL}.
  \item All except \pr{T}.
  \item All of them.
  % This is discussed in Burgess 1999, Which modal logic is the right one. The
  % idea goes back to Hallden 1963 and further to Carnap 1946.) See Schurz 2001
  % for arguments that the logic of validity is much stronger than S5: see
  % Kracht and Kutz 2007:964.

  % For (K): If a conditional $A \to B$ is true in virtue of its form, and so is
  % $A$, we can conclude that $B$ is true in virtue of its form? Arguably yes.
  % Intuitively, if $A$ is true in any conceivable scenario under any
  % interpretation of the sentence letters, and $A\to B$ is true in any
  % conceivable scenario under any interpretation of the sentence letters, then
  % so is $B$ -- for $B$ is bound to be true in any scenario in which $A$ and
  % $A \to B$ are both true.

  % What about \pr{4}? Take an example. $p\lor \neg p$ is logically true; so
  % $\Box (p \lor \neg p)$ is true. You don't need to know what $p$ means in
  % order to see that $\Box (p\lor \neg p)$ is true, nor do you need to know any
  % substantive facts about the world: the statement is true in virtue of its
  % logical form. So $\Box\Box (p \lor \neg p)$ is true as well. In general, if
  % $A$ is true in virtue of its form, then $\Box A$ is also true in virtue of
  % its form. So $\Box A$ does entail $\Box\Box A$.

  % Next, \pr{5} says that if $\neg A$ is not true in virtue of its form, then
  % it is true in virtue its form that $\neg A$ is not true in virtue of its
  % form. This isn't easy to understand, but the following line of thought shows
  % that it is plausible.

  % Suppose the antecedent of \pr{5} is true: $\neg A$ is not true in virtue of
  % its form. If a sentence is not true in virtue of its form, then evidently
  % any sentence of the same form also isn't true in virtue of its form. So,
  % given that $\neg A$ is not true in virtue of its form, one can tell merely
  % by the logical form of $\neg A$ that $\neg A$ is not true in virtue of its
  % form -- in other words, that $\Box \neg A$ is false. So one can tell merely
  % by the logical form of $\Box \neg A$ that it is false. And so one can tell
  % merely by the logical form of $\neg \Box \neg A$ -- equivalently,
  % $\Diamond A$ -- that it is true. So from the assumption $\Diamond A$ we can
  % logically infer $\Box \Diamond A$. So \pr{5} is valid.
\end{sollist}
\end{solution}

Remember that a system of modal logic is just a set of $\L_{M}$-sentences. I
have defined the system S5 in terms of \pr{T}, \pr{K}, \pr{4}, \pr{5}, or
\pr{Dual}, \pr{CPL} and \pr{Nec}, but the same system can be defined by many
other combinations of schemas and rules. (Lewis and Langford used a very
different definition.)

The schemas and rules that I have chosen are called an \textbf{axiomatisation}
of S5. The schemas -- or more precisely, their instances -- are called
\textbf{axioms} because they are the starting points if we want to show that a
sentence is in the system.

% This style of axiomatising modal logics goes back to G\"odel 1933: Eine
% interpretation des intuitionistischen aus- sagenkalkuls. In Ergebnisse eines
% mathematisches Kolloquiums, volume 4, pages 39-40.

To illustrate this point, think of how we could show that
$\Box(p \land q) \to \Box p$ is in S5 (that it is ``S5-valid''). The sentence is
not an instance of any of the schemas I have listed. Instead, we may start with
the non-modal sentence $(p \land q) \to p$. This is a propositional tautology,
so \pr{CPL} tells us that it is in S5. By \pr{Nec}, it follows that
$\Box((p \land q) \to p)$ is in S5 as well. Since all instance of
\pr{K} are in S5, the system contains
\[
  \Box((p \land q) \to p) \to (\Box(p \land q) \to \Box p).
\]
By Modus Ponens, $\Box((p \land q) \to p)$ and
$\Box((p \land q) \to p) \to (\Box(p \land q) \to \Box p)$ entail our target
sentence $\Box(p \land q) \to \Box p$. By \pr{CPL}, this means the target
sentence is also in S5.

Here is a more streamlined presentation of this line of reasoning.
%
\begin{alignat*}{2}
  1.\quad& (p \land q) \to p &\quad& \text{(CPL)}\\
  2.\quad& \Box((p \land q) \to p) &\quad& \text{(1, Nec)}\\
  3.\quad& \Box((p \land q) \to p) \to( \Box(p \land q) \to \Box p) &\quad& \text{(K)}\\
  4.\quad& \Box(p \land q) \to \Box p &\quad& \text{(2, 3, CPL)}
\end{alignat*}

We can use the same streamlined format to show that, say,
$\Box p \to \Diamond p$ is S5-valid.
%
\begin{alignat*}{2}
  1.\quad& \Box \neg p \to \neg p &\quad& \text{(T)}\\
  2.\quad& \neg\Diamond p \leftrightarrow \Box \neg p &\quad& \text{(Dual)}\\
  3.\quad& \neg\Diamond p \to \neg p &\quad& \text{(1, 2, CPL)}\\
  4.\quad& p \to \Diamond p &\quad& \text{(3, CPL)}\\
  5.\quad& \Box p \to p &\quad& \text{(T)}\\
  6.\quad& \Box p \to \Diamond p &\quad& \text{(4, 5, CPL)}
\end{alignat*}

These annotated lists look a lot like proofs. They \emph{are} proofs. Every
axiomatisation of a logical system defines a corresponding \textbf{axiomatic
  calculus}. A proof in an axiomatic calculus is simply a list of sentences each
of which is either an axiom or follows from earlier sentences in the list by one
of the rules. (The annotations on the right are not officially part of the proof.
They are added to help understand where the lines come from.)

\begin{exercise}
  Try to find axiomatic proofs showing that the following sentences are in S5.
  \begin{exlist}
    \item $\Box(\Box p \to p)$
    \item $(\Box p \land \Box q) \to \Box(p \land q)$
    \item $\Diamond \neg p \leftrightarrow \neg \Box p$
    % exercise: prove 4 from KT5
  \end{exlist}
\end{exercise}
\begin{solution}
  \begin{sollist}
    
    \item 
    \begin{alignat*}{2}
      1.\quad& \Box p \to p &\quad& \text{(T)}\\
      2.\quad& \Box(\Box p \to p) &\quad& \text{(1, Nec)}
    \end{alignat*}
    
    \item 
    \begin{alignat*}{2}
      1.\quad& p \to (q \to (p \land q)) &\quad& \text{(CPL)}\\
      2.\quad& \Box (p \to (q \to (p \land q))) &\quad& \text{(1, Nec)}\\
      3.\quad& \Box (p \to (q \to (p \land q))) \to (\Box p \to \Box (q \to (p \land q))) &\quad& \text{(K)}\\
      4.\quad& \Box p \to \Box (q \to (p \land q))) &\quad& \text{(2, 3, CPL)}\\
      5.\quad& \Box (q \to (p \land q))) \to (\Box q \to \Box (p\land q))  &\quad& \text{(K)}\\
      6.\quad& \Box p \to (\Box q \to \Box (p\land q))  &\quad& \text{(4, 5, CPL)}\\
      7.\quad& (\Box q \land \Box q) \to \Box (p\land q)  &\quad& \text{(6, CPL)}
    \end{alignat*}

    \item 
    \begin{alignat*}{2}
      1.\quad& \neg \Diamond \neg p \leftrightarrow \Box \neg\neg p &\quad& \text{(Dual)}\\
      2.\quad& \neg\neg \Diamond \neg p \leftrightarrow \neg \Box \neg\neg p &\quad& \text{(1, CPL)}\\
      3.\quad& \Diamond \neg p \leftrightarrow \neg \Box \neg\neg p &\quad& \text{(2, CPL)}\\
      4.\quad& \neg\neg p \to p &\quad& \text{(CPL)}\\
      5.\quad& \Box(\neg\neg p \to p) &\quad& \text{(4, Nec)}\\
      6.\quad& \Box(\neg\neg p \to p) \to (\Box \neg\neg p \to \Box p)&\quad& \text{(K)}\\
      7.\quad& \Box \neg\neg p \to \Box p&\quad& \text{(5, 6, CPL)}\\
      8.\quad& p \to \neg\neg p &\quad& \text{(CPL)}\\
      9.\quad& \Box(p \to \neg\neg p) &\quad& \text{(8, Nec)}\\
      10.\quad& \Box(p \to \neg\neg p) \to (\Box p \to \Box \neg\neg p)&\quad& \text{(K)}\\
      11.\quad& \Box p \to \Box \neg\neg p &\quad& \text{(9, 10, CPL)}\\
      12.\quad& \Box \neg\neg p \leftrightarrow \Box p &\quad& \text{(7, 11, CPL)}\\
      13.\quad& \neg \Box \neg\neg p \leftrightarrow \neg \Box p &\quad& \text{(12, CPL)}\\
      14.\quad& \Diamond \neg p \leftrightarrow \neg \Box p &\quad& \text{(3, 13, CPL)}
    \end{alignat*}
    
  \end{sollist}
\end{solution}

\begin{exercise}
  In the axiomatic calculus for S5, \pr{Nec} allows us to derive $\Box A$
  from $A$. Someone might object that this inference is obviously invalid, since
  a sentence might be true without being necessarily true. Can you explain why
  \pr{Nec} is an acceptable rule in the axiomatic calculus for S5?
\end{exercise}
\begin{solution}
  In an axiomatic calculus, every line in a proof is either an axiom or follows
  from an earlier line by one of the rules. \pr{Nec} therefore assumes that
  whenever a sentence $A$ is \emph{provable in the axiomatic calculus}, then it
  is necessarily true (reading the box as `it is necessary that'). 

  The rules of the axiomatic calculus cannot be used to directly derive
  assumptions from arbitrary premises. To show that $A$ entails $B$, you have to
  prove $A \to B$.
\end{solution}

The axiomatic method is the oldest formal method of proof. It has many virtues,
but user-friendliness is not among them. Even simple facts are often hard to
prove in an axiomatic calculus. In the next chapter, we will meet a different
method that is much easier to use.


% \begin{exercise}
%   Suppose the world is deterministic, so that everything that is going to happen
%   is entailed by the past state of the universe together with the laws of
%   nature. Intuitively, we can't affect the past, nor the laws of nature. Both
%   are settled. Explain why this entails that everything that is true is settled
%   ($A \to \Box A$), assuming that the logic of historical necessity is S5.
% \end{exercise}
% \begin{solution}
%   Let $p$ specify the past state of the universe and $q$ the laws. By
%   assumption, any true proposition $A$ about the past is settled, If $A$ is
%   about the future then it is entailed by $p$ and $q$, both of which are
%   settled. In S5, $\Box p$
% \end{solution}

  
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "logic2.tex"
%%% End: