Suppose that we have a group consisting of agents. Then we augment
the language of propositional logic by knowledge operators
(one for each agent), and form formulae in the
obvious way. A statement like is read ``agent 1 knows
''^{2.1}. The state that agent knows
that agent knows is formalized by . A
formula like
is
interpreted: ``if agent knows and
then
he knows ''.

Formally, the language of modal epistemic logic is defined as follows:

The modal depth of a formula is defined by the following conditions: for all ; ; ; and .

2001-04-05