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 w0 ∈ W, we define a model, where W’ is the set of all finite sequences such that wi R wi+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 ≡X v if and only if for all 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 (15331592)