Kripke Semantics - Model Constructions

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 vW 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 vW 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 w0W, 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 pX,
  • 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 AX, 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)