The following theorem states some results for specific systems which
will clarify the role played by the directedness axiom
(TL3). Observe that the formula
is not provable in DEK
, i.e., it
may be the case that both
and
are true but
is not true. Generally, if a valid inference rule has at
least 2 premises, and if each of these premises will be known after
some course of thought, then it is not necessarily the case that the
conclusion will be known. Such situations are precluded in the
presence of the directedness axiom.
Utilizing the previous result we can establish an embedding relation
between K and DEK
. Similar relations
obtain between other normal modal systems and their dynamic-epistemic
counterparts which contain schema (TL3).