8  Completeness

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 every modal formula \(\varphi\),

\[ \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}\).

8.1 Canonical Models

First, some preliminary definitions.

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 necessitation.

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.

Theorem 8.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 \varphi\), we have \(\vdash_\Sigma (\boldsymbol{\alpha} \wedge \neg \varphi) \to \bot\). So, \(\Gamma, \neg \varphi\) is \(\Sigma\)-inconsistent.

(\(\Leftarrow\)) If \(\Gamma, \neg \varphi\) is \(\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} \neg (\boldsymbol{\alpha} \wedge \neg \varphi)\), whence \(\vdash_{\Sigma} \boldsymbol{\alpha} \to \varphi\) and \(\Gamma \vdash_\Sigma \varphi\).

\(\blacksquare\)

Maximal Consistency

A set of modal formulas \(\Gamma\) is maximal \(\Sigma\)-consistent if, and only if,

  1. \(\Gamma\) is \(\Sigma\)-consistent, and
  2. for each modal formula \(\varphi\), if \(\Gamma, \varphi\) is \(\Sigma\)-consistent, then \(\varphi \in \Gamma\).

Maximal \(\Sigma\)-consistent sets satisfy helpful decomposition principles.

Theorem 8.2 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.

For 1, 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\).

For 2, 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\).

(\(\Leftarrow\)) 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 3 is perfectly analogous.

\(\blacksquare\)

Accessibility

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,

\[ \begin{array}{lll}\Gamma R \Delta & \text{iff} & \{\varphi : \Box \varphi \in \Gamma\} \subseteq \Delta \\\end{array} \]

We will often make use of an alternative characterization of the relation just now introduced for a canonical model.

Theorem 8.3 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. We look at each direction in turn.

(\(\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\).

\(\blacksquare\)

Theorem 8.4 If \(\Sigma\) is a normal modal system and \(\Gamma\) is a maximal \(\Sigma\)-consistent set of modal formulas, then:

\[ \begin{array}{llll}4a. & \Diamond \varphi \in \Gamma & \text{iff} & \text{for some} \ \Delta, \ \Gamma R \Delta \ \text{and} \ \varphi \in \Delta\\ 4b. & \Box \varphi \in \Gamma & \text{iff} & \text{for every} \ \Delta, \ \text{if} \ \Gamma R \Delta, \ \text{then} \ \varphi \in \Delta \end{array} \]

Proof. We distinguish two directions.

(\(\Rightarrow\)) Consider the set of modal formulas

\[ \{\varphi\} \cup \{\psi: \Box \psi \in \Gamma\} \]

If that set is \(\Sigma\)-consistent, then it can be extended to a maximal \(\Sigma\)-consistent set \(\Delta\), and, by definition of \(R\), \(\Gamma R \Delta\). Since \(\varphi\) would be a member of \(\Delta\) as defined, by Theorem 8.3, \(\Diamond \varphi \in \Gamma\).

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\), and \(\Gamma\) is closed under derivability, 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\).

\(\blacksquare\)

We will now exploit the features of maximal \(\Sigma\)-consistent sets of modal formulas to define the canonical model for a modal system \(\Sigma\).

Canonical Models

The canonical model \(\mathcal{M}_\Sigma\) for a modal system \(\Sigma\) is a model of the form \(( W_\Sigma, R_\Sigma, V_\Sigma)\), where:

  1. \(W_\Sigma\) consists of all maximal \(\Sigma\)-consistent sets of modal formulas.

  2. For all maximal \(\Sigma\)-consistent sets \(\Gamma, \Delta\),

    \(\Gamma R_\Sigma \Delta\) iff \(\{\Diamond \varphi: \varphi \in \Delta \} \subseteq \Gamma\).

    That is, \(\Diamond \varphi \in \Gamma\) whenever \(\varphi \in \Delta\).

  3. 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.

Proposition 8.1 (Truth Lemma) For each maximal \(\Sigma\)-consistent set of modal formulas \(\Gamma\),

\[ \begin{array}{lll}\mathcal{M}_\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} \mathcal{M}_\Sigma, \Gamma \Vdash \varphi & \text{iff} & \varphi \in \Gamma. \end{array} \]
    Base Case:

    \[ \begin{array}{llll} \mathcal{M}_\Sigma, \Gamma \Vdash p & \text{iff} & \Gamma \in V_\Sigma(p) & \\ & \text{iff} & p \in \Sigma. & \textsf{Def} \ V_\Sigma \end{array} \]


    Inductive Step for \(\neg\):

    \[ \begin{array}{llll} \mathcal{M}_\Sigma, \Gamma \Vdash \neg \varphi & \text{iff} &\mathcal{M}_\Sigma, \Gamma \nVdash \varphi & \\ & \text{iff} & \varphi \notin \Gamma& \text{Inductive Hypothesis} \\ & \text{iff} & \neg \varphi \in \Gamma & \textsf{Thm} \ 8.2, 2 \\ \end{array} \]


    Inductive Step for \(\to\):

    \[ \begin{array}{llll} \mathcal{M}_\Sigma, \Gamma \Vdash \varphi \to \psi& \text{iff} & \mathcal{M}_\Sigma, \Gamma \nVdash \varphi \ \text{or} \ \mathcal{M}_\Sigma, \Gamma \Vdash \psi & \\ & \text{iff} & \varphi \notin \Gamma \ \text{or} \ \psi \in \Gamma& \text{Inductive Hypothesis} \\ & \text{iff} & \varphi \to \psi \in \Gamma & \textsf{Thm} \ 8.2, 3 \\ \end{array} \]

    Inductive Step for \(\Box\):

    \[ \begin{array}{llll} \mathcal{M}_\Sigma, \Gamma \Vdash \Box \varphi & \text{iff} & \text{for all} \ \Delta \in W_{\Sigma}, \text{if} \ R_\Sigma \Gamma \Delta, \text{then} \ \mathcal{M}_\Sigma, \Delta \Vdash \varphi & \\ & \text{iff} & \text{for all} \ \Delta \in W_{\Sigma}, \text{if} \ R_\Sigma \Gamma \Delta, \text{then} \ \varphi \in \Delta & \text{Inductive Hypothesis} \\ & \text{iff} & \Box \varphi \in \Gamma & \textsf{Thm} \ 8.3, \ 8.4b\\ \end{array} \]


We conclude that \(V\) verifies exactly those formulas in \(\Sigma\). So, it follows that \(\Sigma\) is satisfiable.

\(\blacksquare\)

8.2 Completeness for Canonical Systems

We are finally in a position to prove a completeness theorem for \(\textsf{K}\).

Theorem 8.5 For each modal formulas \(\varphi\), if \(\models \varphi\), then \(\vdash_\textsf{K} \varphi\). That is, if \(\varphi\) is valid in every frame, then \(\varphi\) is a theorem of \(\textsf{K}\).

Suppose a modal formula \(\varphi\) is not a theorem of \(\textsf{K}\). Then its negation \(\neg \varphi\) will be \(\textsf{K}\)-consistent. That means that we may use Lindenbaum’s lemma to extend \(\{\neg \varphi\}\) to a maximal \(\textsf{K}\)-consistent set \(\Gamma\). Now, note that \(\Gamma\) is one of the worlds of the canonical model for \(\textsf{K}\), \((W_\textsf{K}, R_\textsf{K}, V_\textsf{K})\), and, by the Truth Lemma, we know that \(\neg \varphi\) will be true at \(\Gamma\) in the canonical model for \(\textsf{K}\). Therefore, \(\varphi\) fails at a world in the canonical model for \(\textsf{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 \(\textsf{KT}\) if \(\models_{\text{ref}} \varphi\). That is, if a formula \(\varphi\) is valid in every reflexive frame, then \(\varphi\) is a theorem of \(\textsf{KT}\).

We argue for the contrapositive. Suppose a modal formula \(\varphi\) is not a theorem of \(\textsf{KT}\). Then its negation \(\neg \varphi\) will be \(\textsf{KT}\)-consistent. We will argue that \(\neg \varphi\) is true at a world of the canonical model for \(\textsf{KT}\). That will mean that \(\varphi\) is false at a world of the canonical model for \(\textsf{KT}\). Recall that we want to establish the completeness of \(\textsf{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.

The observation that \(\varphi\) fails at the canonical model for \(\textsf{KT}\) will suffice to that purpose only if the canonical model for \(\textsf{KT}\) is reflexive.

To complete the proof, we must verify that the canonical frame for \(\textsf{KT}\) is reflexive: for all maximal \(\textsf{KT}\)-consistent sets of modal formulas \(\Gamma\), \(\Gamma R_{\textsf{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 \(\textsf{KT}\), which is reflexive.

Theorem 8.6 For each modal formulas \(\varphi\), if \(\models_{\text{ref}} \varphi\), then \(\vdash_\textsf{KT} \varphi\). That is, if \(\varphi\) is valid in every reflexive frame, then \(\varphi\) is a theorem of \(\textsf{KT}\).

Proof. We know that if \(\varphi\) is not a theorem of \(\textsf{KT}\), then \(\varphi\) is not valid in the canonical frame for \(\textsf{KT}\).

We proceed to verify that the canonical frame for \(\textsf{KT}\) is reflexive:

  • For every \(\Gamma \in W_{\textsf{KT}}\), \(\Gamma R_{\textsf{KT}} \Gamma\).

    Given how we defined \(W_{\textsf{KT}}\) and the accessibility relation \(R_{KT}\) on \(W_{\textsf{KT}}\), this is tantamount to the claim:

  • For every maximal \(\textsf{KT}\)-consistent set \(\Gamma\), if \(\varphi \in \Gamma\), then \(\Diamond \varphi \in \Gamma\).

    Let \(\Gamma\) be a maximal \(\textsf{KT}\)-consistent set and suppose \(\varphi \in \Gamma\). Since \(\vdash_{\textsf{KT}} \varphi \to \Diamond \varphi\), it follows that \(\varphi \to \Diamond \varphi \in \Gamma\). But by maximal \(\textsf{KT}\)-consistency, we infer that \(\Diamond \varphi \in \Gamma\).

\(\blacksquare\)

Canonicity

An axiom is canonical if, for every substitution instance \(\varphi\) of the axiom, for any normal system \(\Sigma\), \(\vdash_\Sigma \varphi\) only if \(\mathcal{M}_{\Sigma} \models \varphi\). That is, \(\varphi\) is a theorem of \(\Sigma\) only if \(\varphi\) is valid in the canonical model for \(\Sigma\).

A normal modal system \(\Sigma\) is canonical iff for all \(\varphi\) such that \(\vdash_\Sigma \varphi\), \(\mathcal{M}_{\Sigma} \models \varphi\) . That is, the canonical frame for \(\Sigma\) validates every theorem of \(\Sigma\).

We now argue that each of the axioms listed below are canonical.

Proposition 8.2 If \(\Sigma\) is a normal system, which includes every substitution instance of the relevant axiom, then \(\mathcal{M}_\Sigma\) validates the formula. In other words, \(R_{\Sigma}\) satisfies the condition associated with the axiom.

Axiom Condition on \(R_\Sigma\)
\(\textsf{D}\) \(\Box p \to \Diamond p\) serial on \(W_\Sigma\)
\(\textsf{T}\) \(\Box p \to p\) reflexive on \(W_\Sigma\)
\(\textsf{B}\) \(p \to \Box \Diamond p\) symmetric on \(W_\Sigma\)
\(\textsf{4}\) \(\Box p \to \Box \Box p\) transitive on \(W_\Sigma\)
\(\textsf{5}\) \(\Diamond p \to \Box \Diamond p\) euclidean on \(W_\Sigma\)

Proof. We unpack the argument for each axiom.

  • \(\textsf{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:

    • for all \(\Gamma \in W_{\Sigma}\) there is some \(\Delta \in W_{\Sigma}\) such that \(\Gamma R_{\Sigma} \Delta\).

      This is tantamount to the claim:

    • \(\{\varphi: \Box \varphi \in \Gamma\} \subseteq \Delta\) for some \(\Delta \in W_{\Sigma}\).

      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\). Being maximal \(\Sigma\)-consistent, \(\Gamma\) 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\), we have \((\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.

  • \(\textsf{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:

    • For all \(\Gamma, \Delta \in W_{\Sigma}\), if \(\Gamma R_{\Sigma} \Delta\), then \(\Delta R_{\Sigma} \Gamma\).

      This is tantamount to the claim:

    • For all maximal \(\Sigma\)-consistent sets \(\Gamma\), \(\Delta\), if \(\{\varphi: \Box \varphi \in \Gamma\} \subseteq \Delta\), then \(\{\Diamond \varphi: \varphi \in \Gamma\} \subseteq \Delta\).

      To prove that conditional, assume the antecedent for two maximal \(\Sigma\)-consistent sets \(\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.

  • \(\textsf{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:

    • For all \(\Gamma, \Delta, \Theta \in W_{\Sigma}\), \(\Gamma R_{\Sigma} \Delta\) and \(\Delta R_\Sigma \Theta\), then \(\Gamma R_{\Sigma} \Theta\).

      This is tantamount to the claim:

    • For all maximal \(\Sigma\)-consistent sets \(\Gamma\), \(\Delta\), if \(\{\varphi: \Box \varphi \in \Gamma\} \subseteq \Delta\) and \(\{\varphi: \Box \varphi \in \Delta\} \subseteq \Theta\), then \(\{ \varphi: \Box \varphi \in \Gamma\}\subseteq \Delta\).

      To prove that conditional, assume the antecedent for maximal \(\Sigma\)-consistent sets \(\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.

  • \(\textsf{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:

    • For all \(\Gamma, \Delta, \Theta \in W_{\Sigma}\), \(\Gamma R_{\Sigma} \Delta\) and \(\Gamma R_\Sigma \Theta\), then \(\Delta R_{\Sigma} \Theta\).

      This is tantamount to the claim:

    • For all maximal \(\Sigma\)-consistent sets \(\Gamma\), \(\Delta\), if \(\{\varphi: \Box \varphi \in \Gamma\} \subseteq \Delta\) and \(\{\Diamond \varphi: \varphi \in \Theta\} \subseteq \Gamma\), then \(\{\Diamond \varphi: \varphi \in \Theta\}\subseteq \Delta\).

      To prove that conditional, assume the antecedent for maximal \(\Sigma\)-consistent sets \(\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.