**Model Constructions**

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

The natural homomorphisms 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 and is a mapping such that

*f*preserves the accessibility relation, i.e.,*u R v*implies*f*(*u*)*R’**f*(*v*),- whenever
*f*(*u*)*R’**v*’, there is a*v*∈*W*such that*u R v*and*f*(*v*) =*v*’.

A p-morphism of Kripke models and is a p-morphism of their underlying frames, which satisfies

- if and only if, for any propositional variable
*p*.

P-morphisms are a special kind of bisimulations. In general, a **bisimulation** between frames and is a relation *B ⊆ W × W’*, which satisfies the following “zig-zag” property:

- if
*u B u’*and*u R v*, there exists*v’*∈*W’*such that*v B v’*and*u’ R’ v’*, - if
*u B u’*and*u’ R’ v’*, there exists*v*∈*W*such that*v B v’*and*u R v*.

A bisimulation of models is additionally required to preserve forcing of atomic formulas:

- if
*w B w’*, then if and only if, 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 using **unravelling**. Given a model and a fixed node *w*_{0} ∈ *W*, we define a model, where *W’* is the set of all finite sequences such that *w _{i} R w_{i+1}* for all

*i*<

*n*, and if and only if for a propositional variable

*p*. The definition of the accessibility relation

*R’*varies; in the simplest case we put

- ,

but many applications need the reflexive and/or transitive closure of this relation, or similar modifications.

**Filtration** is a usefull construction which uses to prove FMP for many logics. Let *X* be a set of formulas closed under taking subformulas. An *X*-filtration of a model is a mapping *f* from *W* to a model such that

*f*is a surjection,*f*preserves the accessibility relation, and (in both directions) satisfaction of variables*p*∈*X*,- if
*f*(*u*)*R’**f*(*v*) and, where, then .

It follows that *f* preserves satisfaction of all formulas from *X*. In typical applications, we take *f* as the projection onto the quotient of *W* over the relation

*u ≡*if and only if for all_{X}v*A*∈*X*, if and only if .

As in the case of unravelling, the definition of the accessibility relation on the quotient varies.

Read more about this topic: Kripke Semantics

### Famous quotes containing the word model:

“Socrates, who was a perfect *model* in all great qualities, ... hit on a body and face so ugly and so incongruous with the beauty of his soul, he who was so madly in love with beauty.”

—Michel de Montaigne (1533–1592)