next up previous contents
Next: Systems with the directedness Up: Dynamic epistemic logic Previous: Systems of dynamic-epistemic logic   Contents

Some features of dynamic-epistemic logic


\begin{theorem}[Consistency] \par The systems \textbf{DEK$_N$}, \textbf{DEK$^*_N$}, \textbf{DES4$_N$}, and \textbf{DES4$^*_N$} are consistent. \par\end{theorem}


\begin{proof} \par As \textbf{DEK$_N$}, \textbf{DEK$^*_N$} and \textbf{DES4$_N$}... ...e, a formula like $\alpha\land \lnot \alpha$\ cannot be derived. \par\end{proof}

The following theorem states that all the defined systems DEK$_N$, DEK$^*_N$, DES4$_N$, and DES4$^*_N$ solve the logical omniscience problem. It says that none of the rules NEC, MON, and CGR is valid. Moreover, an agent's explicit knowledge at a time, i.e., the totality of all what this agent knows at that time, needs not be closed under any nontrivial logical rule.


\begin{theorem}[Non-Omniscience] \par\begin{enumerate} \par\item The following i... ...a \to K_i\lnot K_i\alpha$\par\end{enumerate}\par\end{enumerate}\par\end{theorem}


\begin{proof} \par We can construct easily interpretations such that (i) all axi... ...ference rules listed above are invalidated. We omit the details. \par\end{proof}

An agent described by the given logics is not logically omniscient. On the other hand, we cannot say that he is not rational: the agent is rational, because he can (at least in principle) perform actions to close his knowledge under logical laws, as the following theorems show. Instead of the necessitation rule and monotony rule in modal epistemic logic we have now a theorem stating that the agents can know all classical theorems and can draw all consequences of what they know, provided that they perform the right reasoning.


\begin{theorem} \par Let $\alpha$, $\beta$\ be objective formulae and let $\Lamb... ...\alpha \to \langle F_i \rangle K_i\beta$. \par\end{description}\par\end{theorem}


\begin{proof} \par First, note that $[F_i]\alpha\land \langle F_i \rangle \beta\... ...ta \to \langle F_i \rangle K_i\beta$\ we get the desired result. \par\end{proof}


\begin{corollary} \par Assume that $\alpha$, $\beta$\ are objective formulae. Th... ...\langle F_i \rangle K_i(\alpha\lor \beta)$\par\end{enumerate}\par\end{corollary}

Probably, the above rules and theorems are derivable for a larger class of formulae, not only for objective ones. The following list comprises some more provable formulae of DEK$_N$ and its extensions. They say that if all premises of a valid inference rule are known, then after some steps of reasoning the agent will know the conclusion. This still holds if one of the premises is not known yet but will be known after some reasoning. The theorem is proved in appendix B.


\begin{theorem} Assume that $\alpha$\ and $\beta$\ are objective. The following ... ...angle F_i \rangle (K_i\alpha\land K_i\beta)$\par\end{enumerate}\par\end{theorem}

next up previous contents
Next: Systems with the directedness Up: Dynamic epistemic logic Previous: Systems of dynamic-epistemic logic   Contents
2001-04-05