We have explored a landscape of normal modal systems characterizing different classes of frames. We now outline a method for the justification of the fact that a normal modal system \(\Sigma\) characterizes a class of frames \(\mathcal{C}\) by which, we mean, as usual that for all modal formulas, \[ \begin{array}{lll} \vdash_\Sigma \varphi & \text{if, and only if,} & \models_{\mathcal{C}} \varphi \end{array} \] That is, \(\Sigma\) proves all (Completeness) and only (Soundness) formulas, which are valid in all frames in \(\mathcal{C}\). One direction (Soundness) requires one to verify that the axioms of \(\Sigma\) are valid in all frames in \(\mathcal{C}\), and that the rules of inference of \(\Sigma\) preserve validity in all frames in \(\mathcal{C}\).
We will now focus on the other direction (Completeness), which we approach by contraposition: if \(\varphi\) is not a theorem of \(\Sigma\), then \(\varphi\) is not valid in every frame in \(\mathcal{C}\). That is, we will build a special model based on a frame \((W, R)\) in \(\mathcal{C}\) in which the formula \(\varphi\) fails. The model in question will be what is known as the canonical model for the system \(\Sigma\), and the main task will often be to verify that the canonical model for \(\Sigma\) is based on a frame in \(\mathcal{C}\).
First, some preliminary definitions.
Definition 11.1 (Derivability) A modal formula \(\varphi\) is \(\Sigma\)-derivable from \(\Gamma\), written \(\Gamma \vdash_\Sigma \varphi\), if, and only if, there is a finite conjunction \(\boldsymbol{\alpha}\) of formulas \(\alpha_1, \dots , \alpha_n \in \Gamma\) for which: \[ \vdash_{\Sigma} \boldsymbol{\alpha} \to \varphi \]
Notice that this is not quite how we defined derivability in propositional logic since we make no allowance for premises in a derivation. To allow for premises would lead to undesirable results in the presence of the rule of necessitation.
Definition 11.2 (Consistency) A set of modal formulas \(\Gamma\) is \(\Sigma\)-consistent if, and only if, \(\Gamma \nvdash_\Sigma \bot\). That is, there is no finite conjunction \(\boldsymbol{\alpha}\) of formulas \(\alpha_1, \dots , \alpha_n \in \Gamma\) for which: \[ \vdash_{\Sigma} \boldsymbol{\alpha} \to \bot \] Otherwise, we call \(\Gamma\), \(\Sigma\)-inconsistent. We will write that a modal formula \(\varphi\) is \(\Sigma\)-consistent if its singleton set \(\{\varphi\}\) is \(\Sigma\)-consistent, that is, if \(\nvdash_{\Sigma} \varphi \to \bot\).
We will exploit the fact that \(\Sigma\)-consistent sets of modal formulas have a number of helpful features we record now.
Proposition 11.1 For all modal formulas \(\varphi\) in \(\mathcal{L}^\Box\), \[ \begin{array}{lll} \Gamma \vdash_\Sigma \varphi & \text{if, and only if,} & \Gamma, \neg \varphi \ \text{is} \ \Sigma\text{-inconsistent}. \end{array} \]
Proof. We look at each direction in turn.
(\(\Rightarrow\)) If \(\Gamma \vdash_\Sigma \varphi\), then \(\Gamma, \neg \varphi \vdash_\Sigma \varphi\). Since \(\vdash_\Sigma (\boldsymbol{\alpha} \wedge \neg \varphi) \to \neg \varphi\), we have \(\vdash_\Sigma (\boldsymbol{\alpha} \wedge \neg \varphi) \to \bot\). So, \(\Gamma, \neg \varphi\) is \(\Sigma\)-inconsistent.
(\(\Leftarrow\)) If \(\Gamma, \{ \neg \varphi\}\) \(\Sigma\)-inconsistent, for some conjunction \(\boldsymbol{\alpha}\) of members of \(\Gamma\), we have \(\vdash_{\Sigma} \boldsymbol{\alpha} \wedge \neg \varphi \to \bot\). Since \(\vdash_{\Sigma} \neg \bot\), we have that \(\vdash_{\Sigma} \boldsymbol{\alpha} \to \varphi\) and \(\Gamma \vdash_\Sigma \varphi\).
Definition 11.3 (Maximal Consistency) A set of modal formulas \(\Gamma\) is maximal \(\Sigma\)-consistent if, and only if,
Maximal \(\Sigma\)-consistent sets satisfy a variety of helpful decomposition principles.
Lemma 11.1 If \(\Sigma\) is a normal modal system and \(\Gamma\) is a maximal \(\Sigma\)-consistent set of modal formulas, then: \[ \begin{array}{llll} 1. \Gamma \vdash_\Sigma \varphi & \text{iff} & \varphi \in \Gamma \\ 2. \neg \varphi \in \Gamma & \text{iff} & \varphi \notin \Gamma\\ 3. \varphi \to \psi \in \Gamma & \text{iff} & \varphi \notin \Gamma \ \text{or} \ \psi \in \Gamma \\ \end{array} \]
Proof. We look at each claim in turn.
There are two directions.
(\(\Rightarrow\)) If \(\Gamma \vdash_\Sigma \varphi\), then \(\Gamma, \neg \varphi\) is \(\Sigma\)-inconsistent. On the other hand, if \(\varphi \notin \Gamma\), then, by definition of maximal \(\Sigma\)-consistency, \(\Gamma, \varphi\) would be \(\Sigma\)-inconsistent making \(\Gamma\) \(\Sigma\)-inconsistent. So, \(\varphi \in \Gamma\).
(\(\Leftarrow\)) If \(\varphi \in \Gamma\), then \(\Gamma \vdash_{\Sigma} \varphi\) since \(\vdash_{\Sigma} \varphi \to \varphi\).
We look at each direction in turn.
(\(\Rightarrow\)) If \(\neg \varphi \in \Gamma\), then \(\Gamma \vdash_\Sigma \neg \varphi\). So, if \(\Gamma\) is \(\Sigma\)-consistent, then \(\varphi \notin \Gamma\).
(\(\Leftrightarrow\)) If \(\varphi \notin \Gamma\), then \(\Gamma, \varphi\) is \(\Sigma\)-inconsistent. So, \(\Gamma, \neg \neg \varphi\) is \(\Sigma\)-inconsistent, and by Proposition 5.1 \(\Gamma \vdash_\Sigma \neg \varphi\).
The proof of part 3 is analogous.
Definition 11.4 Given two maximal \(\Sigma\)-consistent sets of modal formulas \(\Gamma\) and \(\Delta\), we write \(\Gamma R \Delta\) iff for each modal formula \(\varphi\) in \(\Delta\), \(\Diamond \varphi\) is in \(\Gamma\). Or, in other words, \(\Gamma R \Delta\) iff \(\{\Diamond \varphi : \varphi \in \Delta\} \subseteq \Gamma\).
We will often make use of an alternative characterization of the relation just now introduced for a canonical model.
Lemma 11.2 For all maximal \(\Sigma\)-consistent sets \(\Gamma, \Delta\), \[ \begin{array}{lll} \{\Diamond \varphi : \varphi \in \Delta\} \subseteq \Gamma & \text{iff} & \{\varphi : \Box \varphi \in \Gamma\} \subseteq \Delta \\ \end{array} \]
Proof. (\(\Rightarrow\)) Suppose \(\{\Diamond \varphi : \varphi \in \Delta\} \subseteq \Gamma\). Suppose now that \(\Box \varphi \in \Gamma\). For a reductio, suppose \(\varphi \notin \Delta\). In that case, \(\neg \varphi \in \Delta\), which means, by assumption, that \(\Diamond \neg \varphi \in \Gamma\). Since \(\Diamond\) is \(\neg \Box \neg\), we have that \(\neg \Box \neg \neg \varphi \in \Gamma\). Since \(\vdash_\Sigma \neg \Box \neg \neg \varphi \leftrightarrow \neg \Box \varphi\), we have \(\neg \Box \varphi \in \Gamma\) and \(\Box \varphi \notin \Gamma\), which completes the reductio.
(\(\Leftarrow\)) Suppose \(\{\varphi : \Box \varphi \in \Gamma\} \subseteq \Delta\). We argue for the contrapositive: if \(\Diamond \varphi \notin \Gamma\), then \(\varphi \notin \Delta\). Suppose that \(\Diamond \varphi \notin \Gamma\). Since \(\Diamond\) is \(\neg \Box \neg\), we have that \(\neg \Box \neg \varphi \notin \Gamma\). By maximal \(\Sigma\)-consistency of \(\Gamma\), \(\Box \neg \varphi \in \Gamma\), which, by assumption, requires \(\neg \varphi \in \Delta\). It follows that \(\varphi \notin \Delta\).
Lemma 11.3 If \(\Sigma\) is a normal modal system and \(\Gamma\) is a maximal \(\Sigma\)-consistent set of modal formulas, then: \[ \begin{array}{llll} 3. & \Diamond \varphi \in \Gamma & \text{iff} & \text{for some} \ \Delta, \ \Gamma R \Delta \ \text{and} \ \varphi \in \Delta\\ \end{array} \]
Proof. We distinguish two directions:
(\(\Rightarrow\)) Consider the set of modal formulas \[ \{\varphi\} \cup \{\psi: \Box \psi \in \Gamma\} \] Notice that if \(\Delta\) is a maximal \(\Sigma\)-consistent, which includes that union as a subset, then \(\Gamma R \Delta\), and we would be done.
We now argue that the set given above is \(\Sigma\)-consistent.
Suppose not. Then there is a conjunction \(\psi_1 \wedge \dots \wedge \psi_n\) of modal formulas with \(\Box \psi_1, \dots, \Box \psi_n \in \Gamma\) such that \[ \vdash_{\Sigma} \varphi \wedge (\psi_1 \wedge \dots \wedge \psi_n) \to \bot \] Thus: \[ \vdash_{\Sigma} (\psi_1 \wedge \dots \wedge \psi_n) \to \neg \varphi \] Since \(\Sigma\) is a normal modal system, we have: \[ \vdash_{\Sigma} \Box \psi_1 \wedge \dots \wedge \Box \psi_n \to \Box \neg \varphi \] Since \(\Gamma\) is maximal \(\Sigma\)-consistent, it contains every theorem of \(\Sigma\). Therefore: \[ (\Box \psi_1 \wedge \dots \wedge \Box \psi_n) \to \Box \neg \varphi \in \Gamma \] Because \(\Box \psi_1 \dots \Box \psi_n \in \Gamma\), by lemma 5.1, we infer: \[ (\Box \psi_1 \wedge \dots \wedge \Box \psi_n) \in \Gamma \] \[ \Box \neg \varphi \in \Gamma \] But since \(\Diamond\) abbreviates \(\neg \Box \neg\), \(\Box \neg \varphi\) is equivalent to \(\neg \Diamond \varphi\), and given the \(\Sigma\)-consistency of \(\Gamma\), we have thereby contradicted the assumption that \[ \Diamond \varphi \in \Gamma. \] We conclude that the set \[ \{\varphi\} \cup \{\psi: \Box \psi \in \Gamma\} \] is \(\Sigma\)-consistent and can be extended to a maximal \(\Sigma\)-consistent set \(\Delta\). It follows that \(\Gamma R \Delta\) and \(\varphi \in \Delta\).
(\(\Leftarrow\)) This direction is trivial once we unpack the definition of \(\Gamma R \Delta\).
We will now exploit the features of maximal \(\Sigma\)-consistent sets of modal formulas to define the canonical model for a modal system \(\Sigma\).
Definition 11.5 (Canonical Model) The canonical model \(M_\Sigma\) for a modal system \(\Sigma\) is a model of the form \(( W_\Sigma, R_\Sigma, V_\Sigma)\), where:
\(W_\Sigma\) consists of all maximal \(\Sigma\)-consistent sets of modal formulas,
for all maximal \(\Sigma\)-consistent sets \(\Gamma, \Delta\),
\(\Gamma R_\Sigma \Delta\) if, and only if, \(\{\Diamond \varphi: \varphi \in \Delta \} \subseteq \Gamma\). That is, \(\Diamond \varphi \in \Gamma\) whenever \(\varphi \in \Delta\).
for each propositional variable \(p\),
\(V_{\Sigma}(p) = \{\Gamma \in W_\Sigma : p \in \Gamma \}\).
The interest of canonical models is that they are governed by the truth lemma according to which a world in the canonical model for \(\Sigma\) verifies a modal formula \(\varphi\) if, and only if, that very formula is a member of the world conceived as a maximal \(\Sigma\)-consistent set of modal formulas.
Lemma 11.4 (Truth Lemma) For each maximal \(\Sigma\)-consistent set of modal formulas \(\Gamma\), \[ \begin{array}{lll} (W_\Sigma, R_\Sigma, V_\Sigma), \Gamma \Vdash \varphi & \text{iff} & \varphi \in \Gamma\\ \end{array} \]
The justification for the truth lemma is an induction of the complexity of modal formulas.
We use an induction on the complexity of \(\varphi\) to establish:
\[
\begin{array}{lll}
(W_\Sigma, R_\Sigma, V_\Sigma), \Gamma \Vdash \varphi & \text{iff} & \varphi \in \Gamma.
\end{array}
\]
- Base Case:
\[
\begin{array}{llll}
(W_\Sigma, R_\Sigma, V_\Sigma), \Gamma \Vdash p & \text{iff} & \Gamma \in V_\Sigma(p) & \\
& \text{iff} & p \in \Sigma. & \text{definition of} \ V_\Sigma
\end{array}
\]
- Inductive Step for \(\neg\):
\[
\begin{array}{llll}
(W_\Sigma, R_\Sigma, V_\Sigma), \Gamma \Vdash \neg \varphi & \text{iff} &(W_\Sigma, R_\Sigma, V_\Sigma), \Gamma \nVdash \varphi & \\
& \text{iff} & \varphi \notin \Gamma& \text{Inductive Hypothesis} \\
& \text{iff} & \neg \varphi \in \Gamma & \text{Lemma 5.1, 2} \\
\end{array}
\]
- Inductive Step for \(\to\):
\[ \begin{array}{llll} (W_\Sigma, R_\Sigma, V_\Sigma), \Gamma \Vdash \varphi \to \psi& \text{iff} & (W_\Sigma, R_\Sigma, V_\Sigma), \Gamma \nVdash \varphi \ \text{or} \ (W_\Sigma, R_\Sigma, V_\Sigma), \Gamma \Vdash \psi & \\ & \text{iff} & \varphi \notin \Gamma \ \text{or} \ \psi \in \Gamma& \text{Inductive Hypothesis} \\ & \text{iff} & \varphi \to \psi \in \Gamma & \text{Lemma 5.1, 3} \\ \end{array} \]
\[
\begin{array}{llll}
(W_\Sigma, R_\Sigma, V_\Sigma), \Gamma \Vdash \Box \varphi & \text{iff} & (W_\Sigma, R_\Sigma, V_\Sigma), \Delta \Vdash \varphi \ \text{whenever} \ \Gamma R_\Sigma \Delta & \\
& \text{iff} & \varphi \in \Delta \ \text{whenever} \ \Gamma R_\Sigma \Delta & \text{Inductive Hypothesis} \\
& \text{iff} & \Box \varphi \in \Gamma & \text{Lemmas 5.2 and 5.4} \\
\end{array}
\]
We conclude that \(V\) verifies exactly those formulas in \(\Sigma\). So, it follows that \(\Sigma\) is satisfiable.
We are finally in a position to prove the completeness theorem for K.
Theorem 11.1 (Completeness Theorem for K) For each modal formulas \(\varphi\), if \(\models \varphi\), then \(\vdash_K \varphi\). That is, if \(\varphi\) is valid in every frame, then \(\varphi\) is a theorem of K.
Proof. We argue by contraposition. Suppose a modal formula \(\varphi\) is not a theorem of \(K\). Then its negation \(\neg \varphi\) will be \(K\)-consistent. That means that we may use Lindenbaum’s lemma to extend \(\{\neg \varphi\}\) to a maximal \(K\)-consistent set \(\Gamma\). Now, note that \(\Gamma\) is one of the worlds of the canonical model for \(K\), \((W_K, R_K, V_K)\), and, by the Truth Lemma, we know that \(\neg \varphi\) will be true at \(\Gamma\) in the canonical model for \(K\). Therefore, \(\varphi\) fails at a world in the canonical model for \(K\). We conclude that \(\varphi\) is not valid in every frame.
There are further completeness theorems for the normal modal systems in the landscape we have considered. One example is the observation, for example, that a modal formula \(\varphi\) is a theorem of \(KT\) if \(\models_{\text{ref}} \varphi\). That is, if a formula \(\varphi\) is valid in every reflexive frame, then \(\varphi\) is a theorem of \(KT\).
We argue for the contrapositive. Suppose a modal formula \(\varphi\) is not a theorem of \(KT\). Then its negation \(\neg \varphi\) will be \(KT\)-consistent. We will argue that \(\neg \varphi\) is true at a world of the canonical model for \(KT\). That will mean that \(\varphi\) is false at a world of the canonical model for \(KT\). Recall that we want to establish the completeness of \(KT\) with respect to the class of reflexive frames, which means that we should verify that \(\varphi\) fails at some world of some reflexive model. Our observation that \(\varphi\) fails at the canonical model for \(KT\) will suffice to that purpose only if the canonical model for \(KT\) is reflexive.
To complete the proof, we must verify that the canonical frame for \(KT\) is reflexive: for all maximal \(KT\)-consistent sets of modal formulas \(\Gamma\), \(\Gamma R_{KT} \Gamma\). That will establish that \(\varphi\) is not valid in every reflexive frame, e.g., \(\varphi\) is not valid in the canonical frame for \(KT\), which is reflexive.
Theorem 11.2 (Completeness Theorem for KT) For each modal formulas \(\varphi\), if \(\models_{\text{ref}} \varphi\), then \(\vdash_K \varphi\). That is, if \(\varphi\) is valid in every reflexive frame, then \(\varphi\) is a theorem of \(KT\).
Proof. We know that if \(\varphi\) is not a theorem of \(KT\), then \(\varphi\) is not valid in the canonical frame for \(KT\).
We proceed to verify that the canonical frame for \(KT\) is reflexive:
Given how we defined \(R_{KT}\), this is tantamount to the claim:
But since \(\vdash_{KT} \varphi \to \Diamond \varphi\), it follows that \(\varphi \to \Diamond \varphi \in \Gamma\) and since \(\Gamma\) is closed under \(KT\)-derivability, if \(\Gamma \vdash \Diamond \varphi\), then \(\Diamond \varphi \in \Gamma\). So, if \(\varphi \in \Gamma\), then \(\Gamma \vdash \Diamond \varphi\) and \(\Diamond \varphi \in \Gamma\).
In order to facilitate the proof of completeness theorems for further normal modal systems, we will argue that there is a correlation between the derivability of all substitution instances of certain axioms and certain features of the accessibility relation for the canonical model for a modal system.
Proposition 11.2 The canonical model for a normal modal system \(\Sigma\) satisfies each condition listed below if it includes as axioms all substitution instances of the corresponding axiom.
| Axiom | Condition on \(R_\Sigma\) | |
|---|---|---|
| \(D\) | \(\Box p \to \Diamond p\) | serial on \(W_\Sigma\) |
| \(T\) | \(\Box p \to p\) | reflexive on \(W_\Sigma\) |
| \(B\) | \(p \to \Box \Diamond p\) | symmetric on \(W_\Sigma\) |
| \(4\) | \(\Box p \to \Box \Box p\) | transitive on \(W_\Sigma\) |
| \(5\) | \(\Diamond p \to \Box \Diamond p\) | euclidean on \(W_\Sigma\) |
Proof. We unpack the argument for each axiom.
\(D\) / \(R_\Sigma\) is serial on \(W_\Sigma\)
Suppose \(\Sigma\) proves every substitution instance of the formula \(\Box p \to \Diamond p\). We proceed to verify that the canonical frame for \(\Sigma\) is serial:
This is tantamount to the claim:
It will suffice to prove that \(\{\varphi: \Box \varphi \in \Gamma\}\) is \(\Sigma\)-consistent.
Suppose not. Then there is a conjunction \(\varphi_1 \wedge \dots \wedge \varphi_n\) of modal formulas with \(\Box \varphi_1, \dots, \Box \varphi_n \in \Gamma\) such that \[ \vdash_{\Sigma} (\varphi_1 \wedge \dots \wedge \dots \wedge \varphi_n) \to \bot \] Since \(\Sigma\) is a normal modal system, we have: \[ \vdash_{\Sigma} \Box (\varphi_1 \wedge \dots \wedge \Box \varphi_n) \to \Box \bot \] Since \(\Gamma\) is maximal \(\Sigma\)-consistent, it contains every theorem of \(\Sigma\). Therefore: \[ (\Box \varphi_1 \wedge \dots \wedge \Box \varphi_n) \to \Box \bot \in \Gamma \] Because \(\Box \varphi_1 \dots \Box \varphi_n \in \Gamma\), by lemma 5.1, we infer: \[ (\Box \varphi_1 \wedge \dots \wedge \Box \varphi_n) \in \Gamma \] \[ \Box \bot \in \Gamma \] But since \(\vdash_{\Sigma} \Box \bot \to \diamond \bot\), \[ \Diamond \bot \in \Gamma. \] Unfortunately, since \(\vdash_{\Sigma} \Box \neg \bot\), \[ \neg \Diamond \bot \in \Gamma, \] which would make \(\Gamma\) \(\Sigma\)-inconsistent. We conclude that the original set is \(\Sigma\)-consistent and can be extended to a maximal \(\Sigma\)-consistent set.
\(B\) / \(R_\Sigma\) is symmetric on \(W_\Sigma\)
Suppose \(\Sigma\) proves every substitution instance of the formula \(p \to \Box \Diamond p\). We proceed to verify that the canonical frame for \(\Sigma\) is symmetric:
This is tantamount to the claim:
To prove that conditional, assume the antecedent for arbitrary \(\Gamma, \Delta\): \(\{\varphi: \Box \varphi \in \Gamma\} \subseteq \Delta\). We want to establish the consequent: if \(\varphi \in \Gamma\), then \(\Diamond \varphi \in \Delta\). Let \(\varphi \in \Gamma\). Since \(\Gamma \vdash_\Sigma \varphi \to \Box \Diamond \varphi\), we find that \(\Box \Diamond \varphi \in \Gamma\). So, since \(\Gamma R_\Sigma \Delta\), it follows that \(\Diamond \varphi \in \Delta\) as desired.
\(4\) / \(R_\Sigma\) is transitive on \(W_\Sigma\)
Suppose \(\Sigma\) proves every substitution instance of the formula \(\Box p \to \Box \Box p\). We proceed to verify that the canonical frame for \(\Sigma\) is euclidean:
This is tantamount to the claim:
To prove that conditional, assume the antecedent for arbitrary \(\Gamma, \Delta, \Theta\): \(\{\varphi: \Box \varphi \in \Gamma\} \subseteq \Delta\) and \(\{\varphi: \Box \varphi \in \Delta\} \subseteq \Theta\). We want to establish the consequent: if \(\Box \varphi \in \Gamma\), then \(\varphi \in \Theta\).
If \(\Box \varphi \in \Gamma\), then since \(\vdash_{\Sigma} \Box \varphi \to \Box \Box \varphi\) and \(\Box \varphi \to \Box \Box \varphi \in \Gamma\), it follows that \(\Box \Box \varphi \in \Gamma\). Since \(\Gamma R_\Sigma \Delta\), it follows that \(\Box \varphi \in \Delta\), and since \(\Delta R_\Sigma \Theta\), we conclude that \(\varphi \in \Theta\) as desired.
\(5\) / \(R_\Sigma\) is euclidean on \(W_\Sigma\)
Suppose \(\Sigma\) proves every substitution instance of the formula \(\Diamond p \to \Box \Diamond p\). We proceed to verify that the canonical frame for \(\Sigma\) is euclidean:
This is tantamount to the claim:
To prove that conditional, assume the antecedent for arbitrary \(\Gamma, \Delta, \Theta\): \(\{\varphi: \Box \varphi \in \Gamma\} \subseteq \Delta\) and \(\{\Diamond \varphi: \varphi \in \Theta\} \subseteq \Gamma\). We want to establish the consequent: if \(\varphi \in \Theta\), then \(\Diamond \varphi \in \Delta\). Let \(\varphi \in \Theta\). Since \(\Gamma R_\Sigma \Theta\), \(\Diamond \varphi \in \Gamma\). Since \(\Gamma \vdash_\Sigma \Diamond \varphi \to \Box \Diamond \varphi\), we find that \(\Box \Diamond \varphi \in \Gamma\). So, since \(\Gamma R_\Sigma \Delta\), it follows that \(\Diamond \varphi \in \Delta\) as desired.