Editing Kripke semantics (section)

===Canonical models===

For any normal modal logic, ''L'', a Kripke model (called the '''canonical model''') can be constructed that refutes precisely the non-theorems of
''L'', by an adaptation of the standard technique of using [[maximal consistent set]]s as models. Canonical Kripke models play a 
role similar to the [[Lindenbaum–Tarski algebra]] construction in algebraic
semantics.

A set of formulas is ''L''-''consistent'' if no contradiction can be derived from it using the theorems of ''L'', and Modus Ponens. A ''maximal L-consistent set'' (an ''L''-''MCS''
for short) is an ''L''-consistent set that has no proper ''L''-consistent superset.

The '''canonical model''' of ''L'' is a Kripke model
<math>\langle W,R,\Vdash\rangle</math>, where ''W'' is the set of all ''L''-''MCS'',
and the relations ''R'' and <math>\Vdash</math> are as follows:
: <math>X\;R\;Y</math> if and only if for every formula <math>A</math>, if <math>\Box A\in X</math> then <math>A\in Y</math>,
: <math>X\Vdash A</math> if and only if <math>A\in X</math>.
The 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 that satisfies ''P'',
* for any normal modal logic ''L'' that 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
[[compactness theorem|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 [[decision problem|undecidable]] whether a given axiom is
canonical. We know a nice sufficient condition: [[Henrik Sahlqvist]] identified a broad class of formulas (now called
[[Sahlqvist formula]]s) such that
* a Sahlqvist formula is canonical,
* the class of frames corresponding to a Sahlqvist formula is [[first-order logic|first-order]] definable,
* there is an algorithm that 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.