The language of dynamic-epistemic logic

Conjunction and disjunction are defined as usual. $[F_i]\alpha$ abbreviates $\lnot \langle F_i \rangle \lnot \alpha$. The formula $\langle F_i \rangle \alpha$ is read: ``$\alpha$ is true after some course of thought of $i$'', $[F_i]\alpha$ means ``$\alpha$ is true after any course of thought of $i$''. (We could think of $\langle F_i \rangle$ and $[F_i]$ as the modalities ``at some future times'' and ``at all future times'' of temporal logic, but now time is subjective time, i.e., agent-dependent, generated by the agent's actions.) Note that we do not allow the operator $\langle F_i \rangle$ to occur inside the scope of any knowledge operator. The reason is that such expressions are indexicals: they contain temporal indexicals like ``later'' or ``always'' implicitly. We want to exclude indexical expressions from our language because they require special treatment, which could be very involved and may obscure more important points.