The abstract action of reasoning

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 $F_i$ 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 $F_i$ could be interpreted as a course of thought of the agent $i$. From the viewpoint of dynamic logic: if the set of all atomic actions associated with the agent $i$ and his basis logic is a finite set $\{r_i^1, \ldots ,r_i^n \}$, then $F_i$ can be viewed as $(r_i^1~\cup~r_i^2~\cup~\ldots~\cup~r_i^n)^+$, where the symbols $\cup$ and $^+$ denote choice and non-zero iteration, respectively.^4.2 The choice of the symbols $F_i$ 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 $\langle F \rangle$ satisfies all the axioms for the minimal temporal logic K$_t$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 $\mathcal{L}_N^{DE}$ and will be defined in the following section.