In reading through Chellas' Modal Logic I'm trying to understand his proof of completeness. Here is my best outline of his proof:
If $\Sigma$ is any normal system of modal logic then it has a proper canonical standard model, and every proper canonical standard model is a canonical standard model. So every system has at least one canonical standard model. If $\mathcal{M}$ is a proper canonical standard model and $\mathcal{M}\in\mathrm{C}$ is a class of modals containing it, and $A$ any sentence, then $\vDash_{C}A \quad \Rightarrow \quad \vDash^{M}A \quad \Rightarrow\quad \vdash_{\Sigma}A$ so that $\Sigma$ is complete with respect to $C$.
Now of course my question may be premised on a misunderstanding of his proof, but if my understanding is correct, then this seems to prove that every modal logic system is complete, since every one has a proper canonical standard model.
Is it that we shouldn't be talking about the completeness of a system per se, but completeness only with respect to some class? So would that mean that we have to first pick a class and then, even though we know the system has a proper canonical model, we need to show that the proper canonical standard model that we come up with is actually in the class that we have chosen?
If that's right, then how would we for instance prove the completeness of $K5$, assuming it's complete? What class would we choose? I feel like I have some kind of fundamental misunderstanding about the goal or the method or both.
I'm trying to summarize the issue without too many details.
We have to start from the language of modal logic, with the "operator" $\Box$, and its semantical interpretation, following Kripke.
Of course, we want that the calculus for modal logic turns to be sound and complete with respect to semantics; and so it is.
The first step is to prove that every tautology is valid. The set of tautologies (taken as axioms) and the rule of inference modus ponens will constitute the basis of all modal logics. Thus, we have to show that all the tautologies are valid, and that the rule of modus ponens preserves validity.
The next step is to consider the system K (the "basic" system of modal logic, i.e. the weakest normal modal logic system). We prove that the logic K is sound, that is, that every theorem of K is valid. We do this by showing that the axiom $K$ is valid and that the rule of necessitation preserves validity. This, together with the previous demonstration that the tautologies are valid and that mp preserves validity, guarantees the soundness of K.
With Kripke models, we can also show the invalidity of some schema, like $\Box \varphi \to \Diamond \varphi$.
Also others schemata turn to be invalid :
or
or
But some of those schemata are still "interesting" from a modal point of view; thus, we have a further step. We look at some invalid schemata that nevertheless prove to be valid with respect to a certain class of models, in the sense of being true in all the models of a certain class. Some of these formula will be valid with respect to all models in which the accessibility relation meets a certain condition.
The schema $4$ proves to be valid with respect to the class of models having a transitive accessibility relation. Once we have seen that a schema $S$ is valid with respect to a certain interesting class $\mathsf C$ of models, we are able to show that the normal modal logic based on $S$ (i.e., having $S$ as an axiom schema) is sound with respect to $\mathsf C$, i.e., that every theorem of the logic based on S is valid with respect to $\mathsf C$.
For example, the modal logic K4 has the tautologies, instances of $K$, and instances of the $4$ schema as axioms, and has as theorems all of the formulas derivable from these by modus ponens and necessitation. We can prove that every theorem of the normal modal logic K4 is valid with respect to the class of transitive models. Then we show that K4 is complete with respect to the class of transitive models, showing that the formulas which are valid in the class of transitive models are theorems of K4.
Intuitively, adding axioms to the "basic" modal logic K, will restrict the "numbers" of models. The issue is to find a suitable "characterization" of this logic in terms of a class of models, i.e., the class of all modles with a "special" feature with regard to the accessibility relation.
See Modal Axioms and Conditions on Frames :