canonical model is a model of L, as every L-MCS contains all theorems of L. By Zorn's lemma, each L-consistent set is contained in an L-MCS, in particular every formula unprovable in L has a counterexample in the canonical model. The main application of canonical models are completeness proofs. Properties of the canonical model of K immediately imply completeness of K with respect to the class of all Kripke frames. This argument does not work for arbitrary L, because there is no guarantee that the underlying frame of the canonical model satisfies the frame conditions of L. We say that a formula or a set X of formulas is canonical with respect to a property P of Kripke frames, if X is valid in every frame which satisfies P, for any normal modal logic L which contains X, the underlying frame of the canonical model of L satisfies P. A union of canonical sets of formulas is itself canonical. It follows from the preceding discussion that any logic axiomatized by a canonical set of formulas is Kripke complete, and compact. The axioms T, 4, D, B, 5, H, G (and thus any combination of them) are canonical. GL and Grz are not canonical, because they are not compact. The axiom M by itself is not canonical (Goldblatt, 1991), but the combined logic S4.1 (in fact, even K4.1) is canonical. In general, it is undecidable whether a given axiom is canonical. We know a nice sufficient condition: H. Sahlqvist identified a broad class of formulas (now called Sahlqvist formulas) such that: a Sahlqvist formula is canonical, the class of frames corresponding to a Sahlqvist formula is first-order definable, there is an algorithm which computes the corresponding frame condition to a given Sahlqvist formula. This is a powerful criterion: for example, all axioms listed above as canonical are (equivalent to) Sahlqvist formulas. A logic has the finite model property (FMP) if it is complete with respect to a class of finite frames. An application of this notion is the decidability question: it follows from Post's theorem that a recursively axiomatized modal logic L which has FMP is decidable, provided it is decidable whether a given finite frame is a model of L. In particular, every finitely axiomatizable logic with FMP is decidable. There are various methods for establishing FMP for a given logic. Refinements and extensions of the canonical model construction often