In order to define systems of dynamic-epistemic logic formally we can fix a basis logic and then associate with each axiom schema and each inference rule an atomic action. The formal language is then defined over this set of atomic actions. The logic comprises all theorems of dynamic logic and the specific epistemic axioms discussed above.
However, there are some problems with this approach. First, there might be many different, but equivalent axiomatizations of the basis logic, so the choice of the basic actions must be arbitrary. Moreover, as the resulting dynamic-epistemic system contains dynamic logic entirely, it becomes very complex and therefore difficult to be dealt with. Even more importantly, in most cases we do not need to care about what course of actions the agents just carried out; we are only interested in the result of the actions, so to speak. We only need to know that a certain agent has carried out some reasoning steps, and after that he gains certain new information.
This last point leads us to another approach. We introduce an
auxiliary action with the following intended reading: do any one
of the atomic actions (we don't know what action;) repeat the
non-deterministic choice finitely many times (at least once, but we
don't know how many times!) The action
could be interpreted as a
course of thought of the agent
. From the viewpoint of dynamic
logic: if the set of all atomic actions associated with the agent
and his basis logic is a finite set
, then
can be viewed as
,
where the symbols
and
denote choice and non-zero
iteration, respectively.4.2 The choice of the
symbols
is not accidental at all: in temporal logic it stands
for the operator ``Future''. It turns out that our auxiliary action
behaves in the same manner as the future operator of temporal logic:
the operator
satisfies all the axioms for the
minimal temporal logic K
4. It is no surprise at all: we
know that the minimal temporal logic can be embedded into dynamic
logic, and one way to do this is to take the iteration of an action to
interpret the future operator. The formal language in which our
dynamic-epistemic logics are formulated is called
and will be defined in the following section.