next up previous contents
Next: Axioms for dynamic-epistemic logic Up: Dynamic epistemic logic Previous: Dynamic epistemic logic   Contents

The language of dynamic-epistemic logic

% latex2html id marker 2179
[The language $\mathcal{L}_N^{DE}...
..._i \rangle
\alpha \in \mathcal{L}_N^{DE}$\par\end{enumerate}\par\end{definition}

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.

\begin{definition}[Knowledge-persistent formulae]
\par The sublanguage $\mathcal...
...pha\lor \beta), K_i\alpha \} \subseteq