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 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₀ ∈ 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 ≡_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.