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:
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.