Supplement to Dynamic Epistemic Logic
Appendix N: Temporal aspects of Dynamic Epistemic Logic
Sack (2007, 2008, 2010) and Yap (2006, 2011) have suggested an extension of action model languages obtained by adding new temporal formulas \([Y]F\) assigned the reading “F was true yesterday (i.e., one time-step ago)”. The suggestion is to use the so-called “yesterday” modal operator \([Y]\) to describe the passage of time explicitly in the language. For instance, if we wish to formalize our suggestion that time flows forward whenever actions occur, then we might wish to endorse a principle such as \[ p\to[A,e][Y]p, \] which says, “if p is true, then, after the action occurs, we have that p was true yesterday”. Intuitively, this makes sense: if p is true before the occurrence of the event, then it must be the case that p is true just after the event occurs. Formally endorsing this principle (i.e., developing a formal semantics and an axiomatics that respects the appropriate reduction axioms and in which the above formula is valid for each letter p) is tantamount to enforcing the requirement that every action has one time-step (or “clock-tick”) in duration. That is, the passage of time and the occurrence of actions are directly linked: to ask what time it is amounts to asking how many actions have occurred since some fixed starting point. But there are other possible linkages one might wish to consider as well. Letting \([Y]^nF\) denote the formula F proceeded by n occurrences of the yesterday modal \([Y]\) (i.e., \([Y]^0F\coloneqq F\) and \([Y]^{n+1}F=[Y]^n[Y]F\)), what follows are a few examples.
- Direct linkage: with the occurrence of each action, the clock ticks some fixed nonzero number of times n. We can think of n as the “duration” of the action. (Above we discussed the case \(n=1\).) Therefore, to ask what time it is under direct linkage amounts to asking for the value of n times the number of actions that have occurred since some fixed moment. In symbols, accepting direct linkage amounts to formally endorsing the principle \[ M,w\models p\to[A,e][Y]^np. \]
- Proportional linkage: with the occurrence of each action, the clock ticks a number of times equal to a function f of the size \(s(A,e)\) of the action. So the duration of an action depends in some way on its size. Therefore, to ask what time it is under proportional linkage amounts to asking for the sum of the durations of all actions that have occurred since some fixed moment. In symbols, accepting proportional linkage amounts to formally endorsing the principle \[ M,w\models p\to[A,e][Y]^{f(s(A,e))}p. \]
- Situational linkage: with the occurrence of each action, the clock ticks a number of times equal to a function g that depends on the action A as considered within the context of the current situation \((M,w)\) in which action A occurs. So the duration of an action (and even the issue of whether an action has some nonzero duration) depends on the action and the situational context in which the action occurs. Therefore, to ask what time it is under situational linkage amounts to asking how many times “affirmative clock-tick conditions” have been met (as governed by the output of the clock tick-specifying function g). In symbols, accepting situational linkage amounts to formally endorsing the principle \[ M,w\models p\to[A,e][Y]^{g(M,w,A,e)}p. \]
Proportional linkage is a generalization of direct linkage (take f constant), and situational linkage is a generalization of proportional linkage (take \(g(M,w,A,e)\) to be the value of f on the size \(s(A,e)\)).
Let us assume we have fixed one particular relationship between the flow of time and the occurrence of model-changing events. For example, following Sack (2008, 2010) and Yap (2006, 2011), let us suppose we pick direct linkage with \(n=1\): time flows one clock-tick per action. This fixes an “objective” relationship between time and the occurrence of actions. That is, according to the assumption of direct linkage with \(n=1\), the objective fact is that the time is given in terms of the number of actions that have occurred since some particular fixed starting point. A different linkage would lead to a logical framework with a different objective factual accounting of time. But note that the agents’ “subjective experience” of the linkage between time and the occurrence of actions need not match the objective truth. For example, perhaps the subjective experience is synchronous, wherein the agents have no disagreement, mistakeness, or uncertainty with regard to the objective measure of time. Or perhaps it satisfies the property of perfect recall, which in one variation says that no agent forgets her past knowledge after the occurrence of an action. Other properties might be satisfied as well. This leads us to the following question: which combinations of objective linkage and subjective experience are logically compatible with a particular axiomatic theory of DEL?
Some work has been done on this question. Yap (2006, 2011), van Benthem, Gerbrandy, and Pacuit (2007), Sack (2008, 2010), Hoshi (2009), Hoshi and Yap (2009), van Benthem et al. (2009a), and Wang and Cao (2013), and looked at \(n=1\) direct linkage satisfying synchronicity, perfect recall, and other interesting subjective properties. See Hoshi (2010) for a survey of the traditional approach in DEL; see Wang and Cao (2013) for an alternative axiomatic approach more in the spirit of temporal logic. These lines of work generally follow the suggestion we outlined above: time flows one clock-tick per model-changing event, and the agents have common knowledge of this fact (though individual knowledge with respect to other atemporal issues may vary). So this is a synchronous, perfect recall-satisfying \(n=1\) direct linkage with a matching subjective experience of \(n=1\) direct linkage. Dégremont, Löwe, and Witzel (2011) introduce an \(n=1\) direct linkage in an asynchronous setting. In this approach, time flows just as before, one clock-tick per model-changing event. The difference is in the subjective experience: an agent knows a model-changing event has occurred if her knowledge or belief of something unrelated to time (or “atemporal”) changes. For example, suppose p is true but agent a does not know whether this is so. After the public announcement of p, agent a’s knowledge changes because she comes to learn p, a statement that not that does not contain a temporal modal \([Y]\) and that is therefore unrelated to time (i.e., atemporal). Therefore, the agent will know that the public announcement of p has occurred, and hence she will know that the clock ticked once as per this announcement. But then if the public announcement of p occurs again, agent a’s atemporal knowledge will not change: she already knows p (since it was just announced) and therefore her knowledge about things unrelated to time does not change as per this second announcement of p. Therefore, while the clock will tick a second time as per the occurrence of the second announcement (and the assumption of \(n=1\) direct linkage), she will not know that it has indeed ticked because her atemporal knowledge and belief remains the same. This leads to an asynchronous state wherein she is confused as to the actual time, which is objectively two clock-ticks later but subjectively either one or two clock-ticks later. This gives the general idea of the approach due to Dégremont, Löwe, and Witzel (2011), an asynchronous \(n=1\) direct linkage with a subjective experience of situational linkage. Finally, we mention the approach of Renne, Sack, and Yap (2009, 2015), which introduces a generalized framework for reasoning about a variety of direct linkages and subjective experiences all within the same logic.
The Dynamic Epistemic Logic approach to reasoning about model change has natural connections with the interpreted systems approach of Fagin et al. (1995) and the Epistemic Temporal Logic approach of Parikh and Ramanujam (2003), though there are some important differences. In particular, in these non-DEL approaches, as in temporal logic in general, all temporal information is included from the start within the model. Intuitively, the model contains all information about the past, present, and future. Contrast this with DEL, where models represent the present and, in some cases, the past as well. But in either case, DEL theories developed to date leave the future “open” in the sense that future states of affairs are realized not by looking within a given model but instead by applying a model-changing action modality. It is such model-changing actions that produce “future” states of affairs. So in the “open future” approach of DEL, different future states of affairs are realized by way of different sequences of action model modalities. In “closed future” approaches (e.g., interpreted systems, Epistemic Temporal Logic, and temporal logic), future states of affairs are all together described in advance within a single model. See Hoshi (2010) and Dégremont, Löwe, and WWitzel (2011) for more details.
Another interesting area of work in DEL is to extend “closed future” theories with DEL-style model-changing operators, which introduces many technical and philosophical challenges (e.g., what do we mean by “future” if there are both formulas \([T]F\) that look at what is true at a static “tomorrow”-world found within the current model and formulas \([A,e]F\) that look at what is true after the occurrence of a dynamic, model-changing operation?). The work of Renne et al. (2009, 2015) presents an approach for updating Epistemic Temporal Logic-style models; however, this approach avoids complications by restricting future operators to the dynamic action model modalities \([A,e]\), effectively ignoring “static” futures that would otherwise only be accessible via a “tomorrow” modal operator \([T]\).