SAKAI Masahiro - KripkeSemantics Diff
- Added parts are displayed like this.
- Deleted parts are displayed
like this.
= 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
== 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