Completeness and Canonical Models

Definition of a complete Sigma consistent set

A set $\Gamma$source is complete $\Sigma$source-consistent if and only if it is $\Sigma$source-consistent and for every $!A$source, either $!A \in \Gamma$source or $\lnot !A \in \Gamma$source.

Properties of complete Sigma consistent sets

Suppose $\Gamma$source is complete $\Sigma$source-consistent. Then:

1. $\Gamma$source is deductively closed in $\Sigma$source.

2. $\Sigma \subseteq \Gamma$source.

3. $\lfalse \notin \Gamma$source

4. $\lnot!A \in \Gamma$source if and only if $!A \notin \Gamma$source.

5. $!A \land !B \in \Gamma$source iff $!A \in \Gamma$source and $!B \in \Gamma$source

6. $!A \lor !B \in \Gamma$source iff $!A \in \Gamma$source or $!B \in \Gamma$source

7. $!A \lif !B \in \Gamma$source iff $!A \notin \Gamma$source or $!B \in \Gamma$source

Proof

1. Suppose $\Gamma \Proves[\Sigma] !A$source but $!A \notin \Gamma$source. Then since $\Gamma$source is complete $\Sigma$source-consistent, $\lnot!A \in \Gamma$source. This would make $\Gamma$source inconsistent, since $!A, \lnot !A \Proves[\Sigma] \lfalse$source.

2. If $!A \in \Sigma$source then $\Gamma \Proves[\Sigma] !A$source, and $!A \in \Gamma$source by deductive closure, i.e., case the deductive closure clause for complete Sigma consistent sets.

3. If $\lfalse \in \Gamma$source, then $\Gamma \Proves[\Sigma] \lfalse$source, so $\Gamma$source would be $\Sigma$source-inconsistent.

4. If $\lnot!A \in \Gamma$source, then by consistency $!A \notin \Gamma$source; and if $!A \notin \Gamma$source then $!A \in \Gamma$source since $\Gamma$source is complete $\Sigma$source-consistent.

5. Exercise.

6. Suppose $!A \lor !B \in \Gamma$source, and $!A \notin \Gamma$source and $!B \notin \Gamma$source. Since $\Gamma$source is complete $\Sigma$source-consistent, $\lnot!A \in \Gamma$source and $\lnot !B \in \Gamma$source. Then $\lnot(!A \lor !B) \in \Gamma$source since $\lnot !A \lif (\lnot !B \lif \lnot (!A \lor !B))$source is a tautological instance. This would mean that $\Gamma$source is $\Sigma$source-inconsistent, a contradiction.

7. Exercise.

Exercise completing connective cases

probAnd,probOr,probIf,probIff Complete the proof of the proposition listing properties of complete Sigma consistent sets.

Lindenbaum Lemma

[Lindenbaum's Lemma] If $\Gamma$source is $\Sigma$source-consistent then there is a complete $\Sigma$source-consistent set $\Delta$source extending $\Gamma$source.

Proof

Let $!A_0$source, $!A_1$source, dots be an exhaustive listing of all formulas of the language (repetitions are allowed). For instance, start by listing $\Obj p_0$source, and at each stage $n \ge 1$source list the finitely many formulas of length $n$source using only variables among $\Obj p_0$source, dots, $\Obj p_n$source. We define sets of formulas $\Delta_n$source by induction on $n$source, and we then set $\Delta = \bigcup_n \Delta_n$source. We first put $\Delta_0 = \Gamma$source. Supposing that $\Delta_n$source has been defined, we define $\Delta_{n+1}$source by:

Now let $\Delta = \bigcup_{n=0}^\infty \Delta_n$source.

We have to show that this definition actually yields a set $\Delta$source with the required properties, i.e., $\Gamma \subseteq \Delta$source and $\Delta$source is complete $\Sigma$source-consistent.

It's obvious that $\Gamma \subseteq \Delta$source, since $\Delta_0 \subseteq \Delta$source by construction, and $\Delta_0 = \Gamma$source. In fact, $\Delta_n \subseteq \Delta$source for all $n$source, since $\Delta$source is the union of all $\Delta_n$source. (Since in each step of the construction, we add a formula to the set already constructed, $\Delta_n \subseteq \Delta_{n+1}$source, so since $\subseteq$source is transitive, $\Delta_n \subseteq \Delta_{m}$source whenever $n \le m$source.) At each stage of the construction, we either add $!A_n$source or $\lnot !A_n$source, and every formula appears (at least once) in the list of all $!A_n$source. So, for every $!A$source either $!A \in \Delta$source or $\lnot !A \in \Delta$source, so $\Delta$source is complete by definition.

Finally, we have to show, that $\Delta$source is $\Sigma$source-consistent. To do this, we show that (a) if $\Delta$source were $\Sigma$source-inconsistent, then some $\Delta_n$source would be $\Sigma$source-inconsistent, and (b) all $\Delta_n$source are $\Sigma$source-consistent.

So suppose $\Delta$source were $\Sigma$source-inconsistent. Then $\Delta \Proves[\Sigma] \lfalse$source, i.e., there are $!A_1$source, dots, $!A_k \in \Delta$source such that $\Sigma \Proves !A_1 \lif (!A_2 \lif \cdots (!A_k \lif \lfalse)\dots)$source. Since $\Delta = \bigcup_{n=0}^\infty \Delta_n$source, each $!A_i \in \Delta_{n_i}$source for some $n_i$source. Let $n$source be the largest of these. Since $n_i \le n$source, $\Delta_{n_i} \subseteq \Delta_n$source. So, all $!A_i$source are in some $\Delta_n$source. This would mean $\Delta_n \Proves[\Sigma] \lfalse$source, i.e., $\Delta_n$source is $\Sigma$source-inconsistent.

To show that each $\Delta_n$source is $\Sigma$source-consistent, we use a simple induction on $n$source. $\Delta_0 = \Gamma$source, and we assumed $\Gamma$source was $\Sigma$source-consistent. So the claim holds for $n = 0$source. Now suppose it holds for $n$source, i.e., $\Delta_n$source is $\Sigma$source-consistent. $\Delta_{n+1}$source is either $\Delta_n \cup \{!A_n\}$source if that is $\Sigma$source-consistent, otherwise it is $\Delta_n \cup \{\lnot!A_n\}$source. In the first case, $\Delta_{n+1}$source is clearly $\Sigma$source-consistent. However, by the proposition on consistency factsthe consistency alternative for a formula and its negation, either $\Delta_n \cup \{!A_n\}$source or $\Delta_n \cup \{\lnot!A_n\}$source is consistent, so $\Delta_{n+1}$source is consistent in the other case as well.

Provability characterized by complete extensions

$\Gamma \Proves[\Sigma] !A$source if and only if $!A \in \Delta$source for each complete $\Sigma$source-consistent set $\Delta$source extending $\Gamma$source (including when $\Gamma = \emptyset$source, in which case we get another characterization of the modal system $\Sigma$source.)

Proof

Suppose $\Gamma \Proves[\Sigma] !A$source, and let $\Delta$source be any complete $\Sigma$source-consistent set extending $\Gamma$source. If $!A \notin \Delta$source then by maximality $\lnot!A \in \Delta$source and so $\Delta \Proves[\Sigma] !A$source (by monotonicity) and $\Delta \Proves[\Sigma] \lnot!A$source (by reflexivity), and so $\Delta$source is inconsistent. Conversely if $\Gamma \Proves/[\Sigma] !A$source, then $\Gamma \cup \{ \lnot!A\}$source is $\Sigma$source-consistent, and by Lindenbaum's Lemma there is a complete consistent set $\Delta$source extending $\Gamma \cup \{ \lnot!A \}$source. By consistency, $!A \notin \Delta$source.

Explain

When we construct a model $\mModel{M^\Sigma}$source whose set of worlds is given by the complete $\Sigma$source-consistent sets $\Delta$source in some normal modal logic $\Sigma$source, we will also need to define an accessibility relation $R^\Sigma$source between such “worlds.” We want it to be the case that the accessibility relation (and the assignment $V^\Sigma)$source are defined in such a way that $\mSat{M^\Sigma}{!A}[\Delta]$source iff $!A \in \Delta$source. How should we do this?

Once the accessibility relation is defined, the definition of truth at a world ensures that $\mSat{M^\Sigma}{\Box!A}[\Delta]$source iff $\mSat{M^\Sigma}{!A}[\Delta']$source for all $\Delta'$source such that $R^\Sigma\Delta\Delta'$source

. The proof that $\mSat{M^\Sigma}{!A}[\Delta]$source iff $!A \in \Delta$source requires that this is true in particular for formulas starting with a modal operator, i.e., $\mSat{M^\Sigma}{\Box!A}[\Delta]$source iff $\Box !A \in \Delta$source . Combining this requirement with the definition of truth at a world for $\Box !A$source yields:

Consider the left-to-right direction: it says that if $\Box !A \in \Delta$source, then $!A \in \Delta'$source for any $!A$source and any $\Delta'$source with $R^\Sigma\Delta\Delta'$source. If we stipulate that $R^\Sigma\Delta\Delta'$source iff $!A \in \Delta'$source for all $\Box!A \in \Delta$source, then this holds. We can write the condition on the right of the “iff” more compactly as: $\Setabs{!A}{\Box!A \in \Delta} \subseteq \Delta'$source.

So the question is: does this definition of $R^\Sigma$source in fact guarantee that $\Box !A \in \Delta$source iff $\mSat{M^\Sigma}{\Box !A}[\Delta]$source? Does it also guarantee that $\Diamond !A \in \Delta$source iff $\mSat{M^\Sigma}{\Diamond !A}[\Delta]$source? The next few results will establish this.

Box and diamond operations on sets of formulas

If $\Gamma$source is a set of formulas, let

Lifting a derivation under necessity

If $\Gamma \Proves[\Sigma] !A$source then $\Box\Gamma \Proves[\Sigma] \Box !A$source.

Proof

If $\Gamma \Proves[\Sigma] !A$source then there are $!B_1$source, dots, $!B_k \in \Gamma$source such that $\Sigma \Proves !B_1 \lif (!B_2 \lif \cdots (!B_n \lif !A)\cdots)$source. Since $\Sigma$source is normal, by rule RK, $\Sigma \Proves \Box!B_1 \lif (\Box!B_2 \lif \cdots (\Box!B_n \lif \Box!A)\cdots)$source, where obviously $\Box!B_1$source, dots, $\Box!B_k \in \Box\Gamma$source. Hence, by definition, $\Box\Gamma \Proves[\Sigma] \Box !A$source.

Derivation from inverse-box premises

If $\Box^{-1} \Gamma \Proves[\Sigma] !A$source then $\Gamma \Proves[\Sigma] \Box!A$source.

Proof

Suppose $\Box^{-1}\Gamma \Proves[\Sigma] !A$source; then by the lemma lifting a derivation into boxed premises and conclusion, $\Box\Box^{-1}\Gamma \Proves \Box!A$source. But since $\Box\Box^{-1}\Gamma \subseteq \Gamma$source, also $\Gamma \Proves[\Sigma] \Box!A$source by monotonicity.

Complete-set characterization of necessity

If $\Gamma$source is complete $\Sigma$source-consistent, then $\Box !A \in \Gamma$source if and only if for every complete $\Sigma$source-consistent $\Delta$source such that $\Box^{-1} \Gamma \subseteq \Delta$source, it holds that $!A \in \Delta$source.

Proof

Suppose $\Gamma$source is complete $\Sigma$source-consistent. The “only if” direction is easy: Suppose $\Box !A \in \Gamma$source and that $\Box^{-1}\Gamma \subseteq \Delta$source. Since $\Box!A \in \Gamma$source, $!A \in \Box^{-1}\Gamma \subseteq \Delta$source, so $!A \in \Delta$source.

For the “if” direction, we prove the contrapositive: Suppose $\Box!A \notin \Gamma$source. Since $\Gamma$source is complete $\Sigma$source-consistent, it is deductively closed, and hence $\Gamma \Proves/[\Sigma] \Box !A$source. By the lemma deriving a boxed conclusion from inverse-box premises, $\Box^{-1}\Gamma \Proves/[\Sigma] !A$source. By the proposition on consistency factsthe consistency fact for adding a negated formula, $\Box^{-1}\Gamma \cup \{ \lnot!A \}$source is $\Sigma$source-consistent. By Lindenbaum's Lemma, there is a complete $\Sigma$source-consistent set $\Delta$source such that $\Box^{-1}\Gamma \cup \{ \lnot!A \} \subseteq \Delta$source. By consistency, $!A \notin \Delta$source.

Equivalence of box and diamond accessibility conditions

Suppose $\Gamma$source and $\Delta$source are complete $\Sigma$source-consistent. Then $\Box^{-1}\Gamma \subseteq \Delta$source if and only if $\Diamond\Delta \subseteq \Gamma$source.

Proof

“Only if” direction: Assume $\Box^{-1}\Gamma \subseteq \Delta$source and suppose $\Diamond!A \in \Diamond\Delta$source (i.e., $!A \in \Delta$source). In order to show $\Diamond!A \in \Gamma$source, it suffices to show $\Box\lnot!A \notin \Gamma$source, for then by maximality, $\lnot\Box\lnot !A \in \Gamma$source. Now, if $\Box\lnot!A \in \Gamma$source then by hypothesis $\lnot!A \in \Delta$source, against the consistency of $\Delta$source (since $!A \in \Delta$source). Hence $\Box\lnot!A \notin \Gamma$source, as required.

“If” direction: Assume $\Diamond\Delta \subseteq \Gamma$source. We argue contrapositively: suppose $!A \notin \Delta$source in order to show $\Box!A \notin \Gamma$source. If $!A \notin \Delta$source then by maximality $\lnot!A \in \Delta$source and so by hypothesis $\Diamond\lnot!A \in \Gamma$source. But in a normal modal logic $\Diamond\lnot!A$source is equivalent to $\lnot\Box !A$source, and if the latter is in $\Gamma$source, by consistency $\Box!A \notin\Gamma$source, as required.

Complete-set characterization of possibility

If $\Gamma$source is complete $\Sigma$source-consistent, then $\Diamond !A \in \Gamma$source if and only if for some complete $\Sigma$source-consistent $\Delta$source such that $\Diamond\Delta \subseteq \Gamma$source, it holds that $!A \in \Delta$source.

Proof

Suppose $\Gamma$source is complete $\Sigma$source-consistent. $\Diamond!A \in \Gamma$source iff $\lnot\Box\lnot !A \in \Gamma$source by Dual and closure. $\lnot\Box\lnot !A \in \Gamma$source iff $\Box\lnot !A \notin \Gamma$source by the proposition listing properties of complete Sigma consistent setsthe negation clause for complete Sigma consistent sets since $\Gamma$source is complete $\Sigma$source-consistent. By the complete-consistent-set characterization of necessity, $\Box\lnot !A \notin \Gamma$source iff, for some complete $\Sigma$source-consistent $\Delta$source with $\Box^{-1}\Gamma \subseteq \Delta$source, $\lnot!A \notin \Delta$source. Now consider any such $\Delta$source. By the equivalence between the inverse-box and diamond accessibility conditions, $\Box^{-1}\Gamma \subseteq \Delta$source iff $\Diamond\Delta \subseteq \Gamma$source. Also, $\lnot !A \notin \Delta$source iff $!A \in \Delta$source by the proposition listing properties of complete Sigma consistent setsthe negation clause for complete Sigma consistent sets. So $\Diamond!A \in \Gamma$source iff, for some complete $\Sigma$source-consistent $\Delta$source with $\Diamond\Delta \subseteq \Gamma$source, $!A \in \Delta$source.

Exercise proving the alternate modal characterization

Show that if $\Gamma$source is complete $\Sigma$source-consistent, then $\Diamond !A \in \Gamma$source if and only if there is a complete $\Sigma$source-consistent $\Delta$source such that $\Box^{-1}\Gamma \subseteq \Delta$source and $!A \in \Delta$source.

Do this without using the equivalence between the inverse-box and diamond accessibility conditions.

Definition of the canonical model

Let $\Sigma$source be a normal modal logic. The canonical model for $\Sigma$source is $\mModel{M}^\Sigma = \tuple{W^\Sigma, R^\Sigma, V^\Sigma}$source, where:

1. $W^\Sigma = \Setabs{ \Delta }{\Delta \text{ is complete $\Sigma$-consistent} }$source.

2. $R^\Sigma \Delta\Delta'$source holds if and only if $\Box^{-1}\Delta \subseteq \Delta'$source .

3. $V^\Sigma(p) = \Setabs{\Delta}{p \in \Delta}$source.

Truth Lemma

[Truth Lemma] For every formula $!A$source, $\mSat{M^\Sigma}{!A}[\Delta]$source if and only if $!A \in \Delta$source.

Proof

By induction on $!A$source.

1. Case: $!A \ident \lfalse$source

   $\mSat/{M^\Sigma}{\lfalse}[\Delta]$source by the definition of truth at a world in a modal model, and $\lfalse \notin \Delta$source by the proposition listing properties of complete Sigma consistent setsthe falsity clause for complete Sigma consistent sets.

2. Case: $!A \ident p$source

   $\mSat{M^\Sigma}{p}[\Delta]$source iff $\Delta \in V^\Sigma(p)$source by the definition of truth at a world in a modal model. Also, $\Delta \in V^\Sigma(p)$source iff $p \in \Delta$source by definition of $V^\Sigma$source.

3. Case: $!A \ident \lnot !B$source

   $\mSat{M^\Sigma}{\lnot !B}[\Delta]$source iff $\mSat/{M^\Sigma}{!B}[\Delta]$source (the definition of truth at a world in a modal model) iff $!B \notin \Delta$source (by inductive hypothesis) iff $\lnot !B \in \Delta$source (by the proposition listing properties of complete Sigma consistent setsthe negation clause for complete Sigma consistent sets).

4. Case: $!A \ident !B \land !C$source

   Exercise.

5. Case: $!A \ident !B \lor !C$source

   $\mSat{M^\Sigma}{!B \lor !C}[\Delta]$source iff $\mSat{M^\Sigma}{!B}[\Delta]$source or $\mSat{M^\Sigma}{!C}[\Delta]$source (by the definition of truth at a world in a modal model) iff $!B \in \Delta$source or $!C \in \Delta$source (by inductive hypothesis) iff $!B \lor !C \in \Delta$source (by the proposition listing properties of complete Sigma consistent setsthe disjunction clause for complete Sigma consistent sets).

6. Case: $!A \ident !B \lif !C$source

   Exercise.

7. Case: $!A \ident \Box !B$source

   First suppose that $\mSat{M^\Sigma}{\Box !B}[\Delta]$source. By the definition of truth at a world in a modal model, for every $\Delta'$source such that $R^\Sigma \Delta\Delta'$source, $\mSat{M^\Sigma}{!B}[\Delta']$source. By inductive hypothesis, for every $\Delta'$source such that $R^\Sigma \Delta\Delta'$source, $!B \in \Delta'$source. By definition of $R^\Sigma$source, for every $\Delta'$source such that $\Box^{-1} \Delta \subseteq \Delta'$source, $!B \in \Delta'$source. By the complete-consistent-set characterization of necessity, $\Box !B \in \Delta$source.

   Now assume $\Box !B \in \Delta$source. Let $\Delta' \in W^\Sigma$source be such that $R^\Sigma \Delta\Delta'$source, i.e., $\Box^{-1}\Delta \subseteq \Delta'$source. Since $\Box !B \in \Delta$source, $!B \in \Box^{-1} \Delta$source. Consequently, $!B \in \Delta'$source. By inductive hypothesis, $\mSat{M^\Sigma}{!B}[\Delta']$source. Since $\Delta'$source is arbitrary with $R^\Sigma \Delta\Delta'$source, for all $\Delta' \in W^\Sigma$source such that $R^\Sigma \Delta\Delta'$source, $\mSat{M^\Sigma}{!B}[\Delta']$source. By the definition of truth at a world in a modal model, $\mSat{M^\Sigma}{\Box !B}[\Delta]$source.

8. Case: $!A \ident \Diamond !B$source

   Exercise.

Exercise completing Truth Lemma cases

probFalse,probTrue,probNot,proband,probOr,probIf,probIff,probBox,probDiamond Complete the proof of the Truth Lemma.

Definition of determination by a model

A model $\mModel{M}$source determines a normal modal logic $\Sigma$source precisely when $\mSat{M}{!A}$source if and only if $\Sigma \Proves !A$source, for all formulas $!A$source.

Determination by the canonical model

[Determination] $\mSat{M^\Sigma}{!A}$source if and only if $\Sigma \Proves !A$source.

Proof

If $\mSat{M^\Sigma}{!A}$source, then for every complete $\Sigma$source-consistent $\Delta$source, we have $\mSat{M^\Sigma}{!A}[\Delta]$source. Hence, by the Truth Lemma, $!A \in \Delta$source for every complete $\Sigma$source-consistent $\Delta$source, whence by the complete-consistent-set characterization of provability (with $\Gamma = \emptyset$source), $\Sigma \Proves !A$source.

Conversely, if $\Sigma \Proves !A$source then by the proposition listing properties of complete Sigma consistent setsthe deductive closure clause for complete Sigma consistent sets, every complete $\Sigma$source-consistent $\Delta$source contains $!A$source, and hence by the Truth Lemma, $\mSat{M^\Sigma}{!A}[\Delta]$source for every $\Delta \in W^\Sigma$source, i.e., $\mSat{M^\Sigma}{!A}$source.

Completeness of basic modal logic K

The basic modal logic LogK is complete with respect to the class of all models, i.e., if $\Entails !A$source then $\Log{K} \Proves !A$source.

Proof

Contrapositively, if $\Log{K} \Proves/ !A$source then by Determination $\mSat/{M^{\Log{K}}}{!A}$source and hence $!A$source is not valid.

Canonical correspondence theorem

If a normal modal logic $\Sigma$source contains one of the formulas on the left-hand side of the table of basic modal correspondence facts, then the canonical model for $\Sigma$source has the corresponding property on the right-hand side.

Basic correspondence facts table

[htp] centering

captionBasic correspondence facts.

Proof

We take each of these up in turn.

Suppose $\Sigma$source contains AxD, and let $\Delta \in W^\Sigma$source; we need to show that there is a $\Delta'$source such that $R^\Sigma \Delta\Delta'$source. It suffices to show that $\Box^{-1}\Delta$source is $\Sigma$source-consistent, for then by Lindenbaum's Lemma, there is a complete $\Sigma$source-consistent set $\Delta' \supseteq \Box^{-1}\Delta$source, and by definition of $R^\Sigma$source we have $R^\Sigma \Delta\Delta'$source. So, suppose for contradiction that $\Box^{-1}\Delta$source is not $\Sigma$source-consistent, i.e., $\Box^{-1}\Delta \Proves[\Sigma] \lfalse$source. By the lemma deriving a boxed conclusion from inverse-box premises, $\Delta \Proves[\Sigma] \Box\lfalse$source, and since $\Sigma$source contains AxD, also $\Delta \Proves[\Sigma] \Diamond\lfalse$source. But $\Sigma$source is normal, so $\Sigma \Proves \lnot\Diamond \lfalse$source (the normal-modal theorem that falsity is not possible), whence also $\Delta \Proves[\Sigma] \lnot\Diamond \lfalse$source, against the consistency of $\Delta$source.

Now suppose $\Sigma$source contains AxT, and let $\Delta \in W^\Sigma$source. We want to show $R^\Sigma \Delta\Delta$source, i.e., $\Box^{-1}\Delta \subseteq \Delta$source. But if $\Box!A \in \Delta$source then by AxT also $!A \in \Delta$source, as desired.

Now suppose $\Sigma$source contains AxB, and suppose $R^\Sigma \Delta\Delta'$source for $\Delta$source, $\Delta' \in W^\Sigma$source. We need to show that $R^\Sigma \Delta'\Delta$source, i.e., $\Box^{-1}\Delta' \subseteq \Delta$source. By the equivalence between the inverse-box and diamond accessibility conditions, this is equivalent to $\Diamond\Delta \subseteq \Delta'$source. So suppose $!A \in \Delta$source. By AxB, also $\Box\Diamond!A \in \Delta$source. By the hypothesis that $R^\Sigma \Delta\Delta'$source , we have that $\Box^{-1}\Delta \subseteq \Delta'$source, and hence $\Diamond!A \in \Delta'$source, as required.

Now suppose $\Sigma$source contains Ax4, and suppose $R^\Sigma \Delta_1\Delta_2$source and $R^\Sigma \Delta_2\Delta_3$source. We need to show $R^\Sigma \Delta_1\Delta_3$source. From the hypothesis we have both $\Box^{-1}\Delta_1 \subseteq \Delta_2$source and $\Box^{-1}\Delta_2 \subseteq \Delta_3$source. In order to show $R^\Sigma \Delta_1\Delta_3$source it suffices to show $\Box^{-1}\Delta_1 \subseteq \Delta_3$source. So let $!B \in \Box^{-1}\Delta_1$source, i.e., $\Box!B \in \Delta_1$source. By Ax4, also $\Box\Box!B \in \Delta_1$source and by hypothesis we get, first, that $\Box!B \in \Delta_2$source and, second, that $!B \in \Delta_3$source, as desired.

Now suppose $\Sigma$source contains Ax5, suppose $R^\Sigma \Delta_1\Delta_2$source and $R^\Sigma \Delta_1\Delta_3$source. We need to show $R^\Sigma \Delta_2\Delta_3$source. The first hypothesis gives $\Box^{-1}\Delta_1 \subseteq \Delta_2$source , and the second hypothesis is equivalent to $\Diamond\Delta_3 \subseteq \Delta_1$source , by the equivalence between the inverse-box and diamond accessibility conditions . To show $R^\Sigma \Delta_2\Delta_3$source , by the equivalence between the inverse-box and diamond accessibility conditions, it suffices to show $\Diamond\Delta_3 \subseteq \Delta_2$source. So let $\Diamond!A \in \Diamond\Delta_3$source, i.e., $!A \in \Delta_3$source. By the second hypothesis $\Diamond!A \in \Delta_1$source and by Ax5, $\Box\Diamond!A \in \Delta_1$source as well. But now the first hypothesis gives $\Diamond!A \in \Delta_2$source, as desired.

Determination by intersected model classes

Let $\mClass{C}_\Ax{D}$source, $\mClass{C}_\Ax{T}$source, $\mClass{C}_\Ax{B}$source, $\mClass{C}_\Ax{4}$source, and $\mClass{C}_\Ax{5}$source be the class of all serial, reflexive, symmetric, transitive, and euclidean models (respectively). Then for any schemas $!A_1$source, dots, $!A_n$source among AxD, AxT, AxB, Ax4, and Ax5, the system $\Log{K}!A_1 \dots !A_n$source is determined by the class of models $\mClass{C} = \mClass{C}_{!A_1} \cap \dots \cap \mClass{C}_{!A_n}$source.

Additional canonical-frame correspondences

Let $\Sigma$source be a normal modal logic; then:

1. If $\Sigma$source contains the schema $\Diamond!A \lif \Box !A$source then the canonical model for $\Sigma$source is partially functional.

2. If $\Sigma$source contains the schema $\Diamond!A \liff \Box !A$source then the canonical model for $\Sigma$source is functional.

3. If $\Sigma$source contains the schema $\Box\Box!A \lif \Box !A$source then the canonical model for $\Sigma$source is weakly dense.

(see the table of additional frame correspondences for definitions of these frame properties).

Proof

1. Suppose that $\Sigma$source contains the schema $\Diamond !A \lif \Box !A$source, to show that $R^\Sigma$source is partially functional we need to prove that for any $\Delta_1$source, $\Delta_2$source, $\Delta_3 \in W^\Sigma$source, if $R^\Sigma \Delta_1\Delta_2$source and $R^\Sigma \Delta_1\Delta_3$source then $\Delta_2=\Delta_3$source. Since $R^\Sigma \Delta_1\Delta_2$source we have $\Box^{-1}\Delta_1 \subseteq \Delta_2$source and since $R^\Sigma \Delta_1\Delta_3$source also $\Box^{-1}\Delta_1 \subseteq \Delta_3$source . The identity $\Delta_2=\Delta_3$source will follow if we can establish the two inclusions $\Delta_2 \subseteq \Delta_3$source and $\Delta_3 \subseteq \Delta_2$source. For the first inclusion, let $!A \in \Delta_2$source; then $\Diamond!A \in \Delta_1$source, and by the schema and deductive closure of $\Delta_1$source also $\Box!A \in \Delta_1$source, whence by the hypothesis that $R^\Sigma \Delta_1\Delta_3$source, $!A \in \Delta_3$source. The second inclusion is similar.

2. This follows immediately from part the first additional canonical-frame property and the seriality proof in the canonical-frame correspondence theorem.

3. Suppose $\Sigma$source contains the schema $\Box\Box!A \lif \Box!A$source and to show that $R^\Sigma$source is weakly dense, let $R^\Sigma \Delta_1\Delta_2$source. We need to show that there is a complete $\Sigma$source-consistent set $\Delta_3$source such that $R^\Sigma \Delta_1\Delta_3$source and $R^\Sigma \Delta_3\Delta_2$source. Let:

   $$\Gamma = \Box^{-1}\Delta_1 \cup \Diamond\Delta_2.$$source

   It suffices to show that $\Gamma$source is $\Sigma$source-consistent, for then by Lindenbaum's Lemma it can be extended to a complete $\Sigma$source-consistent set $\Delta_3$source such that $\Box^{-1}\Delta_1 \subseteq \Delta_3$source and $\Diamond\Delta_2 \subseteq \Delta_3$source, i.e., $R^\Sigma \Delta_1\Delta_3$source and $R^\Sigma \Delta_3\Delta_2$source (by the equivalence between the inverse-box and diamond accessibility conditions) .

   Suppose for contradiction that $\Gamma$source is not consistent. Then there are formulas $\Box!A_1$source, dots, $\Box!A_n \in \Delta_1$source and $!B_1$source, dots, $!B_m \in \Delta_2$source such that

   $$!A_1, \dots, !A_n, \Diamond!B_1, \dots, \Diamond!B_m \Proves[\Sigma] \lfalse.$$source

   Since $\Diamond (!B_1 \land \dots \land !B_m) \to (\Diamond!B_1 \land \dots \land \Diamond!B_m)$source is derivable in every normal modal logic, we argue as follows, contradicting the consistency of $\Delta_2$source:

   $$!A_1, \dots, !A_n, & \Diamond!B_1, \dots, \Diamond!B_m \Proves[\Sigma] \lfalse \\ !A_1, \dots,!A_n & \Proves[\Sigma] (\Diamond!B_1 \land \dots \land \Diamond!B_m) \lif \lfalse\\ & \qquad\text{by the deduction theorem}\\ & \qquad\text{\olref[prf][prp]{prop:derivabilityfacts}\olref[prf][prp]{prop:derivabilityfacts-deduction}, and \Taut} \\ !A_1, \dots,!A_n & \Proves[\Sigma] \Diamond(!B_1 \land \dots \land !B_m) \lif \lfalse\\ & \qquad \text{since $\Sigma$ is normal} \\ !A_1, \dots,!A_n & \Proves[\Sigma] \lnot\Diamond (!B_1 \land \dots \land !B_m)\\ & \qquad\text{by \PL} \\ !A_1, \dots,!A_n & \Proves[\Sigma] \Box\lnot (!B_1 \land \dots \land !B_m)\\ & \qquad\text{$\Box\lnot$ for $\lnot\Diamond$} \\ \Box!A_1, \dots,\Box!A_n & \Proves[\Sigma] \Box\Box \lnot (!B_1 \land \dots \land !B_m)\\ & \qquad\text{by \olref[mod]{lem:box1}} \\ \Box!A_1, \dots,\Box!A_n & \Proves[\Sigma] \Box\lnot (!B_1 \land \dots \land !B_m)\\ &\qquad\text{by schema $\Box\Box!A \lif \Box!A$} \\ \Delta_1 & \Proves[\Sigma] \Box\lnot (!B_1 \land \dots \land !B_m)\\ &\qquad\text{by monotonicity, \olref[prf][prp]{prop:derivabilityfacts}\olref[prf][prp]{prop:derivabilityfacts-monotonicity}} \\ & \Box\lnot (!B_1 \land \dots \land !B_m) \in \Delta_1\\ &\qquad\text{by deductive closure}; \\ & \lnot (!B_1 \land \dots \land !B_m) \in \Delta_2\\ &\qquad \text{since } R^\Sigma \Delta_1\Delta_2.$$source
   References in this expression: the proposition on derivability facts, the deduction-theorem clause of the derivability facts, the lemma lifting a derivation into boxed premises and conclusion, the proposition on derivability facts, the monotonicity clause of the derivability facts.