Systems of dynamic-epistemic logic

Now we go on to define axiomatic systems for reasoning about the dynamics of knowledge. We have three groups of axioms: the usual axioms of the propositional calculus, axioms for temporal logic, and axioms governing the interaction between knowledge and reasoning activities.

The axioms (PC1) - (PC3) together with the rule (MP) axiomatize completely the propositional calculus. Together with (TL1), (TL2) and (NEC$_t$) they form a complete axiomatization of the minimal temporal logic of transitive time. The remaining axioms and inference rules describe the dynamics of knowledge. Axiom (DE1) says that the agents are capable of using modus ponens. Axiom (DE2) is the persistence axiom discussed previously, which says that agents do not forget what they know when they are reasoning. Axioms (DE3) - (DE5) state that the agents are able to use the axioms (PC1) - (PC3) of classical logic in their reasoning.

The notions of a proof, a theorem, and a consistent set of formulae (with respect to the logic DEK$_N$) are defined in the usual way. The provability relation wrt DEK$_N$ is denoted $\vdash_{\rm DEK_N}$ as usual. Moreover, we say that a formula $\alpha\in L_K$ is PC-provable, in symbol $\vdash_{PC} \alpha$, just in case $\alpha$ can be proved using only instances of the schemata (PC1) - (PC3) (in the sublanguage $L_K$) and modus ponens.

Of course, we can postulate that the agents can use further simple tautologies and inference rule in their reasoning. For example, we can include axioms such as $K_i\alpha \land K_i\beta\to \langle F_i \rangle K_i(\alpha\land \beta)$, or $\langle F_i \rangle K_i(\alpha\lor \lnot \alpha)$. However, this is not necessary at all, because they can be proved, as we shall see later.

Extensions of DEK$_N$ can be obtained by adding more axioms and inference rules to the basic system. We consider logics obtained from DEK$_N$ by adding axioms from the following list:

(TL3)

$\langle F_i \rangle[F_i]\alpha \to [F_i]\langle F_i \rangle\alpha$

(DE6)

$K_i\alpha \to \alpha$

(DE7)

$\langle F_i \rangle K_i(K_i\alpha \to \alpha)$

(DE8)

$K_i\alpha\to \langle F_i \rangle K_iK_i\alpha$, provided that $\alpha\in \mathcal{L}_N^{K+}$

Axiom (TL3) corresponds to the directedness property discussed previously. It says that courses of thought are directed towards more epistemic completeness. Axiom (DE6) is the well-known schema T saying that knowledge entails truth. Axiom (DE7) says that agents potentially trust their knowledge: when thinking about themselves, they think that what they know must be true. Finally, (DE8) says that the agents are capable of positive introspection.

The systems DES4$_N$ and DES4$^*_N$ can be viewed as logics of explicit, true knowledge. They correspond to the modal system S4$_N$, as they require knowledge to be true, and the agents to have positive introspection. It is easy to see that both DEK$^*_N$ and DES4$_N$ contain DEK$_N$ and are contained in DES4$^*_N$, but neither is a subsystem of the other.