The language of epistemic logic

Suppose that we have a group consisting of $N$ agents. Then we augment the language of propositional logic by $N$ knowledge operators $K_1,\ldots,K_N$ (one for each agent), and form formulae in the obvious way. A statement like $K_1\alpha$ is read ``agent 1 knows $\alpha$''<sup>2.1</sup>. The state that agent $1$ knows that agent $2$ knows $\alpha$ is formalized by $K_1K_2\alpha$. A formula like $K_1\alpha \land K_1(\alpha \to \beta) \to K_1\beta$ is interpreted: ``if agent $1$ knows $\alpha$ and $\alpha \to \beta$ then he knows $\beta$''.

Formally, the language $\mathcal{L}_N^K$ of modal epistemic logic is defined as follows:

The modal depth of a formula is defined by the following conditions: $depth(\phi)=0$ for all $\phi \in Atom$; $depth(\lnot \alpha)=depth(\alpha)$; $depth(\alpha \to \beta) = max(depth(\alpha), depth(\beta))$; and $depth(K_i\alpha) = depth(\alpha) + 1$.