Let W be any non-empty set (of possible worlds). A model M
on W is a triple
where
and
Given any model M, we define a relation 
as follows:
We will write ``
''
if we wish to make M explicit. A formula 
is
said to be valid in M, denoted by 
, if
for all 
.
(By , we mean 
.) Furthermore,
we will employ the following notation:
A model M is a KT5-model if
(M1) 
(M2) 
for any 
and 
,
(M3) 
for any and 
such that 
,
(M4) r(S,t) is an equivalence relation for any and .
A set 
of well formed formulas is said to be
realizable if there exists a KT-5 model M
and such that 
.