Editing Kripke semantics (section)

===Multimodal logics===
{{See also|Multimodal logic}}

Kripke semantics has a straightforward generalization to logics with
more than one modality. A Kripke frame for a language with
<math>\{\Box_i\mid\,i\in I\}</math> as the set of its necessity operators
consists of a non-empty set ''W'' equipped with binary relations
''R<sub>i</sub>'' for each ''i''&nbsp;∈&nbsp;''I''. The definition of a
satisfaction relation is modified as follows:

: <math>w\Vdash\Box_i A</math> if and only if <math>\forall u\,(w\;R_i\;u\Rightarrow u\Vdash A).</math>

A simplified semantics, discovered by Tim Carlson, is often used for
polymodal [[provability logic]]s. A '''Carlson model''' is a structure
<math>\langle W,R,\{D_i\}_{i\in I},\Vdash\rangle</math>
with a single accessibility relation ''R'', and subsets
''D<sub>i</sub>''&nbsp;⊆&nbsp;''W'' for each modality. Satisfaction is
defined as

: <math>w\Vdash\Box_i A</math> if and only if <math>\forall u\in D_i\,(w\;R\;u\Rightarrow u\Vdash A).</math>

Carlson models are easier to visualize and to work with than usual
polymodal Kripke models; there are, however, Kripke complete polymodal
logics which are Carlson incomplete.