next up previous
Next: Soundness of KT5-models Up: Kripke-type Semantics Previous: Kripke-type Semantics

Definition of Kripke-type models

Let W be any non-empty set (of possible worlds). A model M on W is a triple
Given any model M, we define a relation tex2html_wrap_inline478 as follows:


We will write ``tex2html_wrap_inline500'' if we wish to make M explicit. A formula tex2html_wrap_inline360 is said to be valid in M, denoted by tex2html_wrap_inline508, if tex2html_wrap_inline510 for all tex2html_wrap_inline512. (By tex2html_wrap_inline512, we mean tex2html_wrap_inline516.) Furthermore, we will employ the following notation:
A model M is a KT5-model if

(M1) tex2html_wrap_inline520

(M2) tex2html_wrap_inline522 for any tex2html_wrap_inline530 and tex2html_wrap_inline526,

(M3) tex2html_wrap_inline528 for any tex2html_wrap_inline530 and tex2html_wrap_inline532 such that tex2html_wrap_inline534,

(M4) r(S,t) is an equivalence relation for any tex2html_wrap_inline530 and tex2html_wrap_inline526.

A set tex2html_wrap_inline458 of well formed formulas is said to be realizable if there exists a KT-5 model M and tex2html_wrap_inline512 such that tex2html_wrap_inline548.

Yasuko Kitajima
Fri Jun 20 13:39:43 PDT 1997