Editing Kripke semantics (section)

==Model constructions==

As in classical [[model theory]], there are methods for
constructing a new Kripke model from other models.

The natural [[homomorphism]]s in Kripke semantics are called
'''p-morphisms''' (which is short for ''pseudo-epimorphism'', but the
latter term is rarely used). A p-morphism of Kripke frames
<math>\langle W,R\rangle</math> and <math>\langle W',R'\rangle</math> is a mapping
<math>f\colon W\to W'</math> such that
* ''f'' preserves the accessibility relation, i.e., ''u&nbsp;R&nbsp;v'' implies ''f''(''u'')&nbsp;''R’''&nbsp;''f''(''v''),
* whenever ''f''(''u'')&nbsp;''R’''&nbsp;''v''’, there is a ''v''&nbsp;∈&nbsp;''W'' such that ''u&nbsp;R&nbsp;v'' and ''f''(''v'')&nbsp;=&nbsp;''v''’.
A p-morphism of Kripke models <math>\langle W,R,\Vdash\rangle</math> and
<math>\langle W',R',\Vdash'\rangle</math> is a p-morphism of their
underlying frames <math>f\colon W\to W'</math>, which
satisfies
: <math>w\Vdash p</math> if and only if <math>f(w)\Vdash'p</math>, for any propositional variable ''p''.

P-morphisms are a special kind of [[bisimulation]]s. In general, a
'''bisimulation''' between frames <math>\langle W,R\rangle</math> and
<math>\langle W',R'\rangle</math> is a relation
''B&nbsp;⊆&nbsp;W&nbsp;×&nbsp;W’'', which satisfies
the following “zig-zag” property:
* if ''u&nbsp;B&nbsp;u’'' and ''u&nbsp;R&nbsp;v'', there exists ''v’''&nbsp;∈&nbsp;''W’'' such that ''v&nbsp;B&nbsp;v’'' and ''u’&nbsp;R’&nbsp;v’'',
* if ''u&nbsp;B&nbsp;u’'' and ''u’&nbsp;R’&nbsp;v’'', there exists ''v''&nbsp;∈&nbsp;''W'' such that ''v&nbsp;B&nbsp;v’'' and ''u&nbsp;R&nbsp;v''.
A bisimulation of models is additionally required to preserve forcing
of [[atomic formula]]s:
: if ''w&nbsp;B&nbsp;w’'', then <math>w\Vdash p</math> if and only if <math>w'\Vdash'p</math>, for any propositional variable ''p''.
The key property which follows from this definition is that
bisimulations (hence also p-morphisms) of models preserve the
satisfaction of ''all'' formulas, not only propositional variables.

We can transform a Kripke model into a [[tree (graph theory)|tree]] using
'''unravelling'''. Given a model <math>\langle W,R,\Vdash\rangle</math> and a fixed
node ''w''<sub>0</sub>&nbsp;∈&nbsp;''W'', we define a model
<math>\langle W',R',\Vdash'\rangle</math>, where ''W’'' is the
set of all finite sequences
<math>s=\langle w_0,w_1,\dots,w_n\rangle</math> such
that ''w<sub>i</sub>&nbsp;R&nbsp;w<sub>i+1</sub>'' for all
''i''&nbsp;<&nbsp;''n'', and <math>s\Vdash p</math> if and only if
<math>w_n\Vdash p</math> for a propositional variable
''p''. The definition of the accessibility relation ''R’''
varies; in the simplest case we put
:<math>\langle w_0,w_1,\dots,w_n\rangle\;R'\;\langle w_0,w_1,\dots,w_n,w_{n+1}\rangle</math>,
but many applications need the reflexive and/or transitive closure of
this relation, or similar modifications.

'''Filtration''' is a useful construction which one can use to prove [[Kripke semantics#Finite model property|FMP]] for many logics. Let ''X'' be a set of
formulas closed under taking subformulas. An ''X''-filtration of a
model <math>\langle W,R,\Vdash\rangle</math> is a mapping ''f'' from ''W'' to a model
<math>\langle W',R',\Vdash'\rangle</math> such that
* ''f'' is a [[surjection]],
* ''f'' preserves the accessibility relation, and (in both directions) satisfaction of variables ''p''&nbsp;∈&nbsp;''X'',
* if ''f''(''u'')&nbsp;''R’''&nbsp;''f''(''v'') and <math>u\Vdash\Box A</math>, where <math>\Box A\in X</math>, then <math>v\Vdash A</math>.
It follows that ''f'' preserves satisfaction of all formulas from
''X''. In typical applications, we take ''f'' as the projection
onto the [[quotient set|quotient]] of ''W'' over the relation
: ''u&nbsp;≡<sub>X</sub>&nbsp;v'' if and only if for all ''A''&nbsp;∈&nbsp;''X'', <math>u\Vdash A</math> if and only if <math>v\Vdash A</math>.
As in the case of unravelling, the definition of the accessibility
relation on the quotient varies.