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)** 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**) are defined in the usual
way. The provability relation wrt **DEK** is denoted
as usual. Moreover, we say that a formula
is PC-provable, in symbol
, just
in case can be proved using only instances of the schemata
**(PC1) - (PC3)** (in the sublanguage ) 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 , or . However, this is not necessary at all, because they can be proved, as we shall see later.

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

**(TL3)**-
**(DE6)**-
**(DE7)**-
**(DE8)**-
, provided
that

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** and **DES4** can be viewed as
logics of explicit, true knowledge. They correspond to the modal
system **S4**, as they require knowledge to be true, and the
agents to have positive introspection. It is easy to see that both
**DEK** and **DES4** contain **DEK** and
are contained in **DES4**, but neither is a subsystem of
the other.