KripkeSemantics

frame

A frame is a pair <S,R> where S is a set and R a binary relation on S (R⊆S×S)

p-morphism

Let <S1,R1> and <S2,R2> be frames. A p-morphism f: <S1,R1> → <S2,R2> is a function f: S1→S2 satisfying:

• s R1 t implies f(s) R2 f(t)
• g(s) R2 u implies the existence of t wuch that s R1 t and f(t)=u