text:
Logics of temporal-epistemic actions
- 1.8k Downloads
- Citations
We present Dynamic Epistemic Temporal Logic, a framework for reasoning about operations on multi-agent Kripke models that contain a designated temporal relation. These operations are natural extensions of the well-known "action models" from Dynamic Epistemic Logic (DEL). Our "temporal action models" may be used to define a number of informational actions that can modify the "objective" temporal structure of a model along with the agents' basic and higher-order knowledge and beliefs about this structure, including their beliefs about the time. In essence, this approach provides one way to extend the domain of action model-style operations from atemporal Kripke models to temporal Kripke models in a manner that allows actions to control the flow of time. We present a number of examples to illustrate the subtleties involved in interpreting the effects of our extended action models on temporal Kripke models. We also study preservation of important epistemic-temporal properties of temporal Kripke models under temporal action model-induced operations, provide complete axiomatizations for two theories of temporal action models, and connect our approach with previous work on time in DEL.
KeywordsDynamic epistemic logic Epistemic temporal logic Epistemic logic Asynchronicity
1 Introduction
Anyone who has been late to an appointment or missed a deadline is aware that it is often difficult to keep track of time. This basic difficulty is the motivation for this paper, which presents a framework called Dynamic Epistemic Temporal Logic that allows us to reason about epistemic agents' changing beliefs about time, from one point in time to the next. We will develop this framework by combining techniques from the traditions of Epistemic Temporal Logic (ETL) (Parikh and Ramanujam 2003) and Dynamic Epistemic Logic (DEL) (Baltag and Moss 2004; Baltag et al. 1998, 2008; van Benthem et al. 2006; van Ditmarsch et al. 2007).
Our main contribution in this paper is to extend the modal "action model" operators from DEL by incorporating explicit temporal information as to the relative time at which various model-changing events occur. This change to the standard DEL setup allows for a nuanced study of the relationship between dynamic actions, agent belief, and time. A number of authors have already looked at these issues (van Benthem et al. 2009; Dégremont et al. 2011; Hoshi 2009; Hoshi and Yap 2009; Hoshi 2010). Like these (and other) authors, we are interested in the doxastic/epistemic states of reasoning agents and the representation of these states by possibly asynchronous systems. These states can be considered from two perspectives: the "static" perspective of the underlying model (i.e., from the point of view of a "snapshot in time," which includes a snapshot of agents' knowledge/beliefs about time in that moment) and the "dynamic" perspective of action model-induced changes to the underlying model (i.e., from the point of view of a "progression of snapshots," which can be used to understand agents' evolving beliefs about time from one temporal-epistemic snapshot to the next). The difference between this and previous work is that our action models incorporate a binary relation representing the relative time at which the events of the action model occur. Standard action models were designed to include only doxastic/epistemic information explicitly, but our "temporal action models" explicitly include both doxastic/epistemic and temporal information. Our aim, like that of standard DEL, is to represent all key information "dynamically" using flexible relations defined in the action models themselves. By including a relation for time, our framework extends the domain of applicability of the "action model approach" to a wider class of models in which time plays an explicit role in the action model specification language.
As we will see, our framework is sufficiently flexible to accommodate asynchronicity. However, we do not yet have a precise characterization of the exact class of possibly asynchronous systems our approach can capture. The determination of independent criteria that capture the models of a certain framework (e.g., Epistemic Temporal Logic) that are representable within our setting remains an open problem. Some such criteria are known for DEL itself (van Benthem et al. 2009) and we speculate that many features of this work might be put to use for the analysis of our own framework. However, this is a complex task that we must leave for future work.
With respect to the outline of this paper, Sect. 2 introduces the syntax and semantics of Dynamic Epistemic Temporal Logic (DETL). Section 3 then highlights several features of this system by presenting a number of examples that illustrate different ways of measuring the time at a world in a model. The proof system and completeness results for DETL appear in Sect. 4. In Sect. 5, we study the preservation under updates of several model-theoretic properties that one might wish to enforce so as to ensure models have sensible temporal structure. Finally, we conclude in Sect. 6 by connecting DETL to other work concerned with adding time to DEL.
2 Dynamic epistemic temporal logic
We begin with a nonempty finite set \(\fancyscript{A}\) of agents and a disjoint nonempty set \(\fancyscript{P}\) of (propositional) letters. Our semantics is based on Kripke models (with yesterday). These are structures Open image in new window consisting of a nonempty set \(W^M\) of (possible) worlds, a binary epistemic accessibility relation \(\rightarrow ^M_a\) for each \(a\in \fancyscript{A}\) indicating the worlds \(w'\leftarrow ^M_a w\) agent \(a\in \fancyscript{A}\) considers possible at w, a binary temporal accessibility relation Open image in new window indicating the worlds \(w' \leadsto ^M w\) to be thought of as a "yesterday" of (i.e., fall one clock-tick before) world w,1 and a (propositional) valuation \(V^M:\fancyscript{P}\rightarrow \wp (W^M)\) indicating the set \(V^M(p)\) of worlds at which propositional letter \(p\in \fancyscript{P}\) is true. For now, we do not place any restrictions on the behavior of these relations, but later (in Definition 7) we will introduce several desirable properties that they will typically have in concrete examples. For a binary relation R, a pair \((w,v)\in R\) is often called an "R arrow." A pointed Kripke model (with yesterday), sometimes called a situation, is a pair (M, w) consisting of a Kripke model and a world \(w\in W^M\) called the point. To say that a Kripke model (pointed or not) is atemporal means that it contains no Open image in new window arrows.
Pointed Kripke models (M, w) describe fixed (i.e., "static") epistemic-temporal situations in which agents have certain beliefs about time, propositional truth, and the beliefs of other agents. We now define (epistemic-temporal) action models, which transform a situation (M, w) into a new situation (M[U], (w, s)) according to a certain "product operation" \(M\mapsto M[U]\) defined in a moment (in Definition 5).
Definition 1
\(W^U\) is a nonempty finite set of informational events the agents may experience.
For each \(a\in \fancyscript{A}\), the object \(\rightarrow ^U_a\) is a binary (epistemic) accessibility relation. The relation \(\rightarrow _a^U\) designates the events \(s'\leftarrow ^U_a s\) that agent a thinks are consistent with her experience of event s.
Open image in new window is a binary temporal relation indicating the events \(s' \leadsto ^U s\) that occur as a "yesterday" of (i.e., fall one time-step before) event s.
\(\mathsf {pre}^U:W^U\rightarrow F\) is a precondition function assigning a precondition (formula) \(\mathsf {pre}^U(s)\in F\) to each event s. The precondition \(\mathsf {pre}^U(s)\) of event s is the condition that must hold in order for event s to occur.
\(\mathfrak {A}(F)\) is the set of action models over F,
\(\mathfrak {A}^a(F)\) is the set of atemporal action models over F,
\(\mathfrak {A}_*(F)\) is the set of pointed action models over F, and
\(\mathfrak {A}^a_*(F)\) is the set of pointed atemporal action models over F.
Atemporal action models were developed by Baltag and Moss (2004), Baltag et al. (1998) and have been adapted or extended in various ways in the Dynamic Epistemic Logic literature in order to reason about knowledge and belief change; see the textbook (van Ditmarsch et al. 2007) for details and references. Our contribution here is the inclusion of temporal arrows Open image in new window within action models. To say more about this, we first introduce some additional terminology.
Definition 2
(Progressions, Histories, Depth \({{\mathrm{d}}}(w)\)) We shall use the word state to refer either to a world of a Kripke model or an event of an action model. A progression is a finite nonempty sequence \(\langle {w_i}\rangle _{i=0}^n\) of states having \(w_i\leadsto w_{i+1}\) for each \(i<n\). We say that a progression \(\langle {w_i}\rangle _{i=0}^n\) begins at \(w_0\) and ends at \(w_n\). The length of a progression \(\langle {w_i}\rangle _{i=0}^n\) is the number n, which is equal to the number of \(\leadsto \) arrows it takes to link up the states making up the progression (i.e., one less than the number of states in the progression). A past-extension of a progression \(\sigma \) is another progression obtained from \(\sigma \) by adding zero or more extra states at the beginning of the sequence (i.e., in the "past-looking direction" from x to y in the arrow Open image in new window ). A past-extension is proper if more than zero states were added. A history is a progression that has no proper past-extension. For each state w, we define \({{\mathrm{d}}}(w)\) as follows: if there is a maximum \(n\in \mathbb {N}\) such that there is a history of length n that ends at w, then \({{\mathrm{d}}}(w)\) is this maximum n; otherwise, if no such maximum \(n\in \mathbb {N}\) exists, then \({{\mathrm{d}}}(w) = \infty \). We call \({{\mathrm{d}}}(w)\) the depth of w. A state w satisfying \({{\mathrm{d}}}(w)=0\) is said to be initial.
We will present a number of examples shortly showing that the inclusion of temporal Open image in new window arrows in both Kripke models and action models allow us to reason about time in a Dynamic Epistemic Logic-style framework. The basic idea is this: if the depth \({{\mathrm{d}}}(w)\) of a world w is finite, then the depth \({{\mathrm{d}}}(w)\) of w indicates the time at w; likewise, if the depth \({{\mathrm{d}}}(s)\) of an event s is finite, then the depth \({{\mathrm{d}}}(s)\) of s indicates the relative time at which event s takes place. Notice that this notion of "time" can be a little strange: if \(t_1\leadsto s\) and \(t_2\leadsto s\) with \(t_1\ne t_2\), then \({{\mathrm{d}}}(s)\ge \max \{{{\mathrm{d}}}(t_1),{{\mathrm{d}}}(t_2)\}\) but we might think it odd to say that "the time is \({{\mathrm{d}}}(s)\)" given that there is "branching" in the past direction. Therefore, in order to make our notion of time coherent and useful, there are a number of things we do. First, we introduce our multi-modal language \({L_{\mathsf {DETL}}}\) having doxastic modalities \(\Box _a\varphi \) ("agent a believes \(\varphi \)") for each \(a\in \fancyscript{A}\), the temporal modality \([Y]\varphi \) ("\(\varphi \) was true 'yesterday' (i.e., one time-step ago)"), and action model modalities \([U,s]\varphi \) ("after action (U, s) occurs, \(\varphi \) is true").
Definition 3
Definition 4
(Past State) Let U be an action model. A past state is an event s in U that has no yesterday: there is no \(s'\leadsto ^U s\).
Every history \(s_0\leadsto s_1\leadsto s_2\leadsto \cdots \leadsto s_n\) begins with a past state (see Definition 2). The past state \(s_0\) plays a special role in the semantics by copying part or all of the input Kripke model. The next definition shows how this is done. The sequential execution of successive events \(s_1,\ldots ,s_n\) then transforms this copy.
Definition 5
\(M,w\models \Box _a\varphi \) means \(M,v\models \varphi \) for each \(v\leftarrow ^M_aw\).
\(M,w\models [Y]\varphi \) means \(M,v\models \varphi \) for each \(v\leadsto ^M w\).
- \(M,w\models [U,s]\varphi \) means \(M,w\models \mathsf {pre}^U(s)\) implies \(M[U],(w,s)\models \varphi \), where
\(W^{M[U]} \mathop {=}\limits ^{ \text{ def }}\{ (v,t) \in W^M \times W^U \mid M,v\models \mathsf {pre}^U(t)\}\).
We have \((v,t)\rightarrow ^{M[U]}_a(v',t')\) if and only if both \(v\rightarrow ^M_av'\) and \(t\rightarrow ^U_a t'\).
- We have \((v',t') \leadsto ^{M[U]} (v,t)\) if and only if we have one of the following:
\(v' \leadsto ^M v, t'=t\), and t is a past state; or
\(v'=v\) and \(t' \leadsto ^U t\).
\(V^{M[U]}(p) \mathop {=}\limits ^{ \text{ def }}\{(v,t)\in W^{M[U]} \mid v \in V^M(p)\}\).
After taking the update product \(M\mapsto M[U]\), the epistemic relation \(\rightarrow _a\) behaves as it does in DEL (van Ditmarsch et al. 2007); that is, one pair is epistemically related to another iff they are related componentwise. This is analogous to the notion of synchronous composition in process algebra (van Glabbeek 2001). However, our relations \(\rightarrow _a\) are epistemic, whereas the relations in process algebra are temporal.
The behavior of our temporal relation \(\leadsto \) after the update product \(M\mapsto M[U]\) is analogous to the notion of asynchronous composition from process algebra (Aceto et al. 2001): one component of the pair makes the transition while the other component remains fixed. However, in our case, if \((v',t') \leadsto ^{M[U]} (v,t)\), then the component that makes the transition depends on whether t is a past state. If t is indeed a past state, then the first component makes the transition (\(v'\leadsto v\)) and the second component remains fixed (\(t'=t\)). Otherwise, if t is not a past state, then it is instead the first component that remains fixed (\(v'=v\)) and the second component that makes the transition (\(t'\leadsto t\)).
If M and U are atemporal, then our operation \(M\mapsto M[U]\) is equivalent to the standard "product update" from DEL and M[U] is atemporal.
Definition 6
(Epistemic Past State) Let U be an action model. An epistemic past state is a past state s in U whose precondition is a validity (i.e., \(\models \mathsf {pre}^U(s)\)) and whose only epistemic arrows are the reflexive arrows \(s\rightarrow ^U_a s\) for each agent \(a\in \fancyscript{A}\).
Like a past state (Definition 4), an epistemic past state \(s_0\) in a history \(s_0\leadsto \cdots \leadsto s_n\) plays the special role of copying the initial state of affairs before the remaining events in the history take place. However, there is a key difference: a past state may copy only part of the initial state of affairs, whereas an epistemic past state will always make a complete copy. A later result (Theorem 4) will explain this further. Therefore, a history \(s_0\leadsto \cdots \leadsto s_n\) beginning with an epistemic past state \(s_0\) may be thought of as describing the following construction: the epistemic past state \(s_0\) makes a complete copy of the initial state of affairs (thereby remembering the "past" just as it was) and then the remaining events \(s_1,\dots ,s_n\) transform this copy (appending "future" states of affairs one by one). A series of examples in Sect. 3 will explain this in further detail.
Definition 7
Persistence of Facts (for Kripke models only): \(w\leadsto w' \Rightarrow (w\in V(p)\Leftrightarrow w'\in V(p))\) for all w and \(w'\).
This says that propositional letters retain their values across temporal \(\leadsto \) arrows.
Depth-Definedness: \({{\mathrm{d}}}(w)\ne \infty \) for all w.
This says that every world/event has a finite depth.
Knowledge of the Past: \((w'\leadsto w\rightarrow _a v)\Rightarrow \exists v'(v'\leadsto v)\) for all \(a\in \fancyscript{A}, w', w\), and v.
This says that agents know if there is a past (i.e., a state reachable via a backward step along a \(\leadsto \) arrow).
Knowledge of the Initial Time: \(w\rightarrow _av\wedge \lnot \exists w'(w'\leadsto w)\Rightarrow \lnot \exists v'(v'\leadsto v)\) for all \(a\in \fancyscript{A}, w\), and v.
This says that agents know if there is no past.
Uniqueness of the Past: \((w'\leadsto w\wedge w''\leadsto w)\Rightarrow (w'=w'')\) for all \(w', w\), and \(w''\).
This says that there is only one possible past.
Perfect Recall: \((w\leadsto v\rightarrow _a v')\Rightarrow \exists w'(w\rightarrow _aw'\leadsto v')\) for all \(a\in \fancyscript{A}, w, v\), and \(v'\).
This says that agents do not forget what they knew in the past.2
Synchronicity: The structure is depth-defined and \(w\rightarrow _a w'\) implies \({{\mathrm{d}}}(w)={{\mathrm{d}}}(w')\) for all \(a\in \fancyscript{A}, w\), and \(w'\).
This says that there is no uncertainty, disagreement, or mistakenness among the agents with regard to the depth of a world/event.
History Preservation (for action models U only): \(s'\leadsto ^U s\) implies \(\models \mathsf {pre}^U(s)\rightarrow \mathsf {pre}^U(s')\) for all \(s'\) and s; further, every past state in U is an epistemic past state.
This says that a non-initial event s can take place only if its predecessor \(s'\) can as well, and initial events can always take place (Definition 6). Whenever an event s in a history preserving action model U is executable at a world w of a Kripke model M (i.e., \(M,w\models \mathsf {pre}^U(s)\)), the temporal structure of any partial or full history \(s_n\leadsto \cdots \leadsto s_0=s\) in U is preserved as the partial or full history \((w,s_n)\leadsto \cdots \leadsto (w,s_0)=(w,s)\) in the updated model M[U]. In this way, history preserving action models preserve the executable parts of their own histories.
- Past Preservation (for pointed action models (U, s) Epistemic Past Stateonly): The action model U is history preserving; further, every progression \(s_n\leadsto ^U\cdots \leadsto ^Us_0=s\) that ends at s can be past-extended to a historythat begins at an epistemic past state \(s_{n+m}\). To say an event \(t\in W^U\) is past preserving means the action (U, t) with point t is past preserving. This says that there is a "link to the past" (i.e., an epistemic past state) via a sequence of Open image in new window arrows. Since past preserving action models are history preserving, it follows that past preserving action models preserve executable parts of their own histories and maintain a "link to the past." (This is explained in detail in and around the forthcoming Theorem 4.)$$\begin{aligned} s_{n+m}\leadsto ^U \cdots \leadsto ^U s_{n+1} \leadsto ^U s_n\leadsto ^U\cdots \leadsto ^Us_0=s \end{aligned}$$
Time-advancing (for pointed action models (U, s) only): The action (U, s) is past preserving and the point s is not a past state.
This says that the "past" is at least one time-step away.
For the moment, we do not require that our Kripke models or action models satisfy any of the above properties. This will change in Sect. 5, where we study the preservation of Kripke model properties under action models satisfying appropriate properties, and in Sect. 6, where we impose a number of these properties in order to study connections between our framework and other approaches to the study of time in Dynamic Epistemic Logic.
A note on the depth of worlds (Definition 2) in the updated model M[U]: if world w and event t both have finite depth, then the maximum depth of the resulting world \((w,t)\in W^{M[U]}\) is \({{\mathrm{d}}}(w)+{{\mathrm{d}}}(t)\). The reason: we can take at most \({{\mathrm{d}}}(t)\) backward steps in the second coordinate (fix the first coordinate and proceed backward in the second until a past state is reached), and we can take at most \({{\mathrm{d}}}(w)\) backward steps in the first coordinate (fix the second coordinate and proceed backward in the first until an initial world is reached). The actual depth of (w, t) does not need to obtain its maximum: when stepping backward in either coordinate (with the other fixed), we may reach a pair \((w',s')\) whose world \(w'\) violates the precondition of the event \(s'\) (i.e., \(M,w'\not \models \mathsf {pre}^U(s')\)) and therefore the pair \((w',s')\) will not be a member of \(W^{M[U]}\). However, if the action model U is history preserving, then this problem is avoided and hence \({{\mathrm{d}}}(w,t)={{\mathrm{d}}}(w)+{{\mathrm{d}}}(t)\).
Finally, we note that we can express finite depth explicitly in our language.
Theorem 1
In the next section, we will discuss how the depth of a world w can be used as an explicit measure of the time at world w. If one adopts this measure of time, then it follows from Theorem 1 that we can express the time of a world within our language \({L_{\mathsf {DETL}}}\): we say that "the time at world w is n" to mean that w satisfies \(D_n\).
3 Examples
In this section, we will illustrate several features of our system. This will demonstrate the way in which our system can represent interesting epistemic situations as well as shed some light on the ways in which time is treated in dynamic systems. First, we will define explicit and implicit measures of time. An explicit measure of time is one in which the time of a world w in model M can be determined solely by inspection of M. As we have seen, the depth of a world in a Kripke model (see Definition 2) can provide an explicit measure of the time at that world, and this can be expressed explicitly in our language (Theorem 1). In contrast, an implicit measure of time is one in which the time of a world w in model M cannot be determined solely be inspection of M. For example, if we measure the time at a world in M by the number of updates that have led up to M, this can provide an implicit measure of the time at that world. These are not the only possible implicit and explicit measures, but they are certainly natural ones within our \(\mathsf {DETL}\) framework.
Now we will consider ways in which explicit and implicit representations of time might differ. More specifically, we will consider cases in which there is only a single update (implicitly increasing the time by 1) but at which the explicit time at the actual world changes by a number other than 1. Second, we will add in the epistemic aspect, by demonstrating the ways in which agents can hold differing beliefs about temporal and epistemic features of their situation.
3.1 Explicit and implicit representations of time
Example 1
The action \((U_2,s)\) (Fig. 2) represents the public announcement of p. Applied to our initial situation (M, w) (Fig. 1), the result is \((M[U_2],(w,s))\).
The language of ordinary DEL is the atemporal fragment of \({L_{\mathsf {DETL}}}\) without the [Y] modality. In this language, the only way to refer to the agents' knowledge before the announcement is with reference to the original situation (M, w). This is because ordinary DEL lacks \(\leadsto \) arrows, both in action models and in the underlying Kripke models.
Example 1 showed "standard" temporal behavior: a single update increases the time of the actual world by 1. Two obvious ways in which updates could be "non-standard" are by not increasing the time when an update takes place or by increasing the time by a number greater than 1.
Example 2
Here we consider the effect of the action \((U_3,t)\) (Fig. 3) on our initial situation (M, w) (Fig. 1). This action has a structure that is nearly identical to that of action \((U_2,s)\) in Example 1 (Fig. 2); in fact, these actions are based on the same underlying action model (i.e., \(U_2=U_3\)). However, the actual events of \((U_2,s)\) and \((U_3,t)\) are different. The result of the update with the latter action is the pointed model \((M[U_3],(w,t))\). Note that the resultant actual world (w, t) is among the worlds (u, t), (w, t), and (v, t) that make up the "copy" of the initial model M.
We have designed our system so that the initial world w and its copy (w, t) satisfy the same formulas. In this way, we may identify each initial world with its copy, so that the collection of copied worlds (and the arrows interconnecting them) may be identified with the initial model itself. This allows us to reason about what was the case in the initial model by evaluating formulas only within the resultant model. In effect, we can "forget" the initial model because all of its information is copied over to the resultant model.
To make this work, both w and its copy (w, t) must satisfy the same formulas. We guarantee this by designing our system so that it ignores all "future" worlds, by which we mean the worlds accessible from the point only via a link \(x\leadsto y\) from a "past" world x to a "future" world y.3 So from the point of view of our theory, the time-1 worlds (u, s) and (w, s) in Fig. 3 are ignored in the resultant time-0 situation \((M[U_3],(w,t))\) because the time-1 worlds can only be reached via a forward \(\leadsto \) arrow. This leaves only the "copy" of the initial model M consisting of the worlds (u, t), (w, t), and (v, t). The resultant situation \((M[U_3],(w,t))\) is therefore equivalent to the initial situation (M, w) from the point of view of our theory. In other words, the action \((U_3,t)\) does not change the state of affairs at all.4
Remark 1
The previous two examples illustrate some motivation behind our choice not to include a [T] operator, as defined in (1). If our language had included such an operator, two worlds that are intended to represent the exact same state of affairs could disagree about the truth of formulas. In Example 2, a non-time-advancing update transforms (M, w) into \((M[U_3],(w,t))\), but the worlds w and (w, t) are meant to represent the same situation and so should satisfy the same formulas. However, (M, w) and \((M[U_3],(w,t))\) disagree on the truth of the formula \(\langle T\rangle p\). But as we have defined \({L_{\mathsf {DETL}}}\) without the [T]-operator, we can easily show that for any \({L_{\mathsf {DETL}}}\)-formula \(\varphi \), we have \(M, w \models \varphi \) iff \(M[U], (w,t) \models \varphi \) because t is an epistemic past state (see Theorem 4). This avoids the problem illustrated here where two worlds that are supposed to represent the same situation disagree on the truth of formulas.
Example 1 also illustrates the semantic difference between an action model operator [U, s] and the operator [T]. The truth of \([U,s]\varphi \) is determined by evaluating \(\varphi \) in a new model, while the truth of \([T]\varphi \) is determined by evaluating \(\varphi \) within the model as it currently stands. In considering our initial model (M, w) (Fig. 1), note that \(M, w \not \models \langle {T}\rangle p\). However, as we can see, \(M, w \models \langle {U_2,s}\rangle p\). So while we informally read the formula \(\langle {T}\rangle \varphi \) as claiming that \(\varphi \) will hold "tomorrow" (and that there is at least one possible "tomorrow" world), this is only from the perspective of a static model—it does not consider all possible ways in which that model might evolve given different updates.
The [U, s] and [T] operators are not the only options for "tomorrow" operators. Section 2 mentions the way in which the update operators [U, s] serve as dynamic parameterized operators. And it is also possible to define dynamic unparameterized operators that work by quantifying over the parameterized ones, and these also are different from [T] operators. Call our unparameterized operator [N], and we can define: \(M,w\models [N]\varphi \) if and only if \(M,w\models [U,s]\varphi \) for all action models (U, s) with only epistemic preconditions (this constraint is imposed on the action models, so as to ensure the well-foundedness of the semantics) (Balbiani et al. 2008). Since all public announcement action models fall into this category, we have that \(M,w\models \langle N\rangle p\) (since \(M,w\models \langle U_2,s\rangle p\)) and yet \(M,w\not \models \langle T\rangle p\).
We believe that these interpretive issues involving [T] reflect its complex relationship with the update modalities. Indeed, [T] may not even have a clear interpretation in the context of our framework, which is part of the rationale for leaving it out of our language. But such a situation is not unusual in the epistemic logic tradition. For instance, a common system for modeling agents' beliefs is \(\mathsf {KD45}\), whose epistemic accessibility relation does not have to be symmetric. In such systems, it is not clear that the converse of the accessibility relation has a clear semantic interpretation, but this is not viewed as problematic. So for us, the relation Open image in new window is one example of many from modal logic of a relation that has a corresponding modality but whose converse does not. (Also, the semantic asymmetry of having a [Y] operator but no corresponding [T] operator is analogous to an asymmetry in ordinary DEL, which has [U, s] modalities but no converse \([U,s]^{-1}\) modalities.) As a result, our system \(\mathsf {DETL}\) is one that has a dynamic parameterized future (accessed via the update modals [U, s]) and a static unparameterized past (accessed via the yesterday modal [Y]).
Example 3
In this example, the time at the actual world increases by 2 even though only a single update \((U_4,r)\) (Fig. 4) takes place. With simple modifications of \((U_4,r)\), we could increase the time by any finite number.
These three examples demonstrate the differences between explicit and implicit measures of time; in particular, the number of updates (the implicit time) need not equal the depth of the actual world (the explicit time). In this paper, we will adopt the convention that the time at the actual world is measured by its depth (explicit time). While this is by no means a necessary choice, it has the advantage of allowing us to determine the time at a world solely by inspection of the model to which it belongs.
3.2 Agents mistaken about time
Given that we are measuring the time at a world by its depth, we can represent situations in which agents are unable to distinguish between worlds that have different times. These situations can be brought about by \(\mathsf {DETL}\) actions, as the following example illustrates.
Example 4
In this example, \((U_5,r)\) (Fig. 5) represents the sequenced public announcement of p followed by the asynchronous semi-private announcement of q to agent b. This increases the time at the actual world by 2, as in Example 3. However, in the present example, agent a is uncertain whether the time has increased by 1 or by 2.
We contrast Example 4 with the following.
Example 5
\((U_6,r)\) (Fig. 6) couples a public announcement of p with the simultaneous semi-private announcement of q to agent b. When we compare this with Example 4 (pictured in Fig. 5), we note that the agents' respective knowledge gain is identical with respect to the propositional facts: a learns that p is true but not whether q is true, while b learns both p and q. However, in the current example (pictured in Fig. 6), b learns p and q simultaneously instead of successively, and a's knowledge differs accordingly.
4 Proof system and completeness
Definition 8
The theory of Dynamic Epistemic Temporal Logic, \(\mathsf {DETL}\), is defined in Fig. 7. Axioms whose name begins with "U" are called reduction axioms.5
Many axioms of \(\mathsf {DETL}\) are the same as in Dynamic Epistemic Logic.6 In defining \(\mathsf {DETL}\), we have not imposed any of the properties from Definition 7 on action models, nor have we designed the theory to be sound for Kripke models having properties from Definition 7 that one might expect. So \(\mathsf {DETL}\) should be viewed as the minimal theory that brings update mechanisms to a basic Epistemic Temporal Logic. However, we will study the preservation of these properties in Sect. 5, and we study a \(\mathsf {DETL}\)-based theory satisfying a number of these properties in Sect. 6.
Theorem 2
(\({L_{\mathsf {DETL}}}\) Reduction) For every \({L_{\mathsf {DETL}}}\)-formula \(\varphi \), there is an action model-free \({L_{\mathsf {SETL}}}\)-formula \(\varphi ^\circ \) such that \(\mathsf {DETL}\vdash \varphi \leftrightarrow \varphi ^\circ \).
The proof is a straightforward adaptation of the standard argument from Dynamic Epistemic Logic (van Ditmarsch et al. 2007). \(\square \)
Theorem 3
(Soundness and Completeness) \(\mathsf {DETL}\vdash \varphi \) if and only if \(\models \varphi \).
Case: s is a past state.
Assume \(M,w\models [U,s][Y]\varphi \). By the definition of truth, \(M[U],(w',s)\models \varphi \) for each \((w',s)\leadsto ^{M[U]}(w,s)\). Therefore, if \(v\leadsto ^M w\) satisfies \(M,v\models \mathsf {pre}^U(s)\), then \(M[U],(v,s)\models \varphi \). Conclusion: \(M,w\models [Y][U,s]\varphi \). Conversely, assume \(M,w\models [Y][U,s]\varphi \) and \((w',s)\leadsto ^{M[U]}(w,s)\). The second assumption implies both that \(w'\leadsto ^M w\)—and hence \(M,w'\models [U,s]\varphi \) by the first assumption—and that \(M,w'\models \mathsf {pre}^U(s)\). But then \(M[U],(w',s)\models \varphi \). Conclusion: \(M,w\models [U,s][Y]\varphi \).
Case: s is not a past state. Assume \(M,w\models [U,s][Y]\varphi \). By the definition of truth, \(M[U],(w,t)\models \varphi \) for each \((w,t)\leadsto ^{M[U]}(w,s)\). If \(s'\leadsto ^Us\) satisfies \(M,w\models \mathsf {pre}^U(s')\), then \((w,s')\leadsto ^{M[U]}(w,s)\) and hence \(M[U],(w,s')\models \varphi \). Conclusion: \(M,w\models \bigwedge _{s'\leadsto ^U s}[U,s']\varphi \). Conversely, assume \(M,w\models \bigwedge _{s'\leadsto ^U s}[U,s']\varphi \) and \((w,t)\leadsto ^{M[U]}(w,s)\). The second assumption implies both that \(t\leadsto ^U s\)—and hence \(M,w\models [U,t]\varphi \) by the first assumption—and that \(M,w\models \mathsf {pre}^U(t)\). But then \(M[U],(w,t)\models \varphi \). Conclusion: \(M,w\models [U,s][Y]\varphi \).
5 Preservation results
In this section, we study the preservation of properties of Kripke models defined previously in Definition 7. These properties have been of interest in the study of time in Dynamic Epistemic Logic (van Benthem et al. 2009, 2007; Dégremont et al. 2011; Sack 2010, 2008; Yap 2011) and so it will be useful for our purposes to understand the conditions under which they are preserved within our \(\mathsf {DETL}\) setting. Theorem 4 concerns the behavior of past states in action models, and Theorem 5 concerns the preservation of Kripke model properties.
Theorem 4
- (a)
If s is an epistemic past state, then (M[U], (w, s)) and (M, w) satisfy the same \({L_{\mathsf {DETL}}}\)-formulas.
- (b)If (U, s) is past preserving, then there is a historysuch that \((M[U],(w,s_0))\) and (M, w) satisfy the same \({L_{\mathsf {DETL}}}\)-formulas.$$\begin{aligned} (w,s_0) \leadsto ^{M[U]} (w,s_1) \leadsto ^{M[U]} \cdots \leadsto ^{M[U]} (w,s_n) = (w,s) \end{aligned}$$
- (a)
Since the language of \({L_{\mathsf {DETL}}}\) does not include forward-looking tomorrow operators [T], it follows by the standard argument in modal logic (Blackburn et al. 2001) that bisimilar worlds satisfy the same action model-free \({L_{\mathsf {DETL}}}\)-formulas (i.e., the same \({L_{\mathsf {SETL}}}\)-formulas).8 By \({L_{\mathsf {DETL}}}\) Reduction (Theorem 2) and soundness (Theorem 3), bisimilar worlds also satisfy the same \({L_{\mathsf {DETL}}}\)-formulas. Finally, one can show that there is a bisimulation between (w, s) and w. The result follows.
- (b)
Past preservation of (U, s) implies there exists a history \(s_0\leadsto ^U\cdots \leadsto ^Us_n=s\) that begins at an epistemic past state \(s_0\). The result therefore follows by part (a).\(\square \)
We now examine the relationship between our conditions on action models (Definition 7) and the preservation of certain Kripke models properties (also Definition 7) under the update operation \(M\mapsto M[U]\).
Theorem 5
- (a)
If M satisfies persistence of facts, then so does M[U].
- (b)
If M and U are depth-defined, then so is M[U].
- (c)
If M and U satisfy knowledge of the past and U is history preserving, then M[U] satisfies knowledge of the past.
- (d)
If M satisfies knowledge of the initial time and U is history preserving, then M[U] satisfies knowledge of the initial time.
- (e)
If M and U satisfy uniqueness of the past, then so does M[U].
- (f)
If M and U satisfy perfect recall and U is history preserving, then M[U] satisfies perfect recall.
- (g)
If M and U are synchronous and U is history preserving, then M[U] is synchronous.
We prove each item in turn.
(a) If M satisfies persistence of facts, then so does M[U]. Suppose that M satisfies persistence of facts and \((w,s) \leadsto ^{M[U]} (w',s')\). It follows that \(w=w'\) or \(w\leadsto ^M w'\). Now M satisfies persistence of facts, so \(w\in V^M(p)\) iff \(w'\in V^M(p)\). Applying the fact that \((v,t)\in V^{M[U]}(p)\) iff \(v\in V^M(p)\), we have \((w,s)\in V^{M[U]}(p)\) iff \((w',s')\in V^{M[U]}(p)\).
Base case: \({{\mathrm{d}}}(s)=0\).It follows that s is a past state. Therefore \((w',s')\leadsto ^{M[U]}(w,s)\) implies \(w'\leadsto ^M w\) and \(s'=s\). We now prove (4) by a sub-induction on \({{\mathrm{d}}}(w)\). In the sub-induction base case, \({{\mathrm{d}}}(w)=0\) and therefore there is no \(w'\leadsto ^M w\), which implies there is no \((w',s)\leadsto ^{M[U]}(w,s)\). But then \({{\mathrm{d}}}(w,s)=0={{\mathrm{d}}}(w)+{{\mathrm{d}}}(s)\), which completes the sub-induction base case. For the sub-induction step, we assume that (4) holds for all worlds v having \(0\le {{\mathrm{d}}}(v)<{{\mathrm{d}}}(w)\) (the "sub-induction hypothesis") and we prove (4) holds for world w itself. If \({{\mathrm{d}}}(w,s)=0\), then (4) follows immediately because depths are non-negative integers. So let us assume that \({{\mathrm{d}}}(w,s)>0\). Then we may choose an arbitrary \((w',s)\leadsto ^{M[U]}(w,s)\), from which it follows that \(w'\leadsto ^M w\). Since M is depth-defined, \({{\mathrm{d}}}(w')\le {{\mathrm{d}}}(w)-1\) and so we may apply the sub-induction hypothesis:Hence$$\begin{aligned} {{\mathrm{d}}}(w',s) \le {{\mathrm{d}}}(w')+{{\mathrm{d}}}(s) \le {{\mathrm{d}}}(w)-1+{{\mathrm{d}}}(s). \end{aligned}$$$$\begin{aligned} {{\mathrm{d}}}(w,s)= & {} 1+\max \{{{\mathrm{d}}}(w',s)\mid (w',s)\leadsto ^{M[U]}(w,s)\}\\\le & {} 1+\max \{{{\mathrm{d}}}(w)-1+{{\mathrm{d}}}(s) \mid (w',s)\leadsto ^{M[U]}(w,s)\}\\= & {} {{\mathrm{d}}}(w)+{{\mathrm{d}}}(s) \end{aligned}$$
Induction step: we suppose (4) holds for all events t having \(0\le {{\mathrm{d}}}(t)<{{\mathrm{d}}}(s)\) (the "induction hypothesis") and prove that (4) holds for event s itself.s is not a past state because \({{\mathrm{d}}}(s)>0\). Therefore \((w',s')\leadsto ^{M[U]}(w,s)\) implies \(w'=w\) and \(s'\leadsto ^U s\). If \({{\mathrm{d}}}(w,s)=0\), then (4) follows immediately because depths are non-negative integers. So let us assume \({{\mathrm{d}}}(w,s)>0\). Then we may choose an arbitrary \((w,s')\leadsto ^{M[U]}(w,s)\), from which it follows that \(s'\leadsto ^U s\). Since U is depth-defined, we have \({{\mathrm{d}}}(s')\le {{\mathrm{d}}}(s)-1\) and so we may apply the induction hypothesis:Hence$$\begin{aligned} {{\mathrm{d}}}(w,s') \le {{\mathrm{d}}}(w)+{{\mathrm{d}}}(s') \le {{\mathrm{d}}}(w)+{{\mathrm{d}}}(s)-1. \end{aligned}$$$$\begin{aligned} {{\mathrm{d}}}(w,s)= & {} 1+\max \{{{\mathrm{d}}}(w,s')\mid (w,s')\leadsto ^{M[U]}(w,s)\}\\\le & {} 1+\max \{{{\mathrm{d}}}(w)+{{\mathrm{d}}}(s)-1 \mid (w,s')\leadsto ^{M[U]}(w,s)\}\\= & {} {{\mathrm{d}}}(w)+{{\mathrm{d}}}(s) \end{aligned}$$
Case: \(w' \leadsto ^M w\) and \(s'=s\) is a past state.
Since \(w'\leadsto ^M w \rightarrow ^M_a v\) and M satisfies knowledge of the past, there exists \(v' \leadsto ^M v\). Since U is history preserving and s is a past state, s is an epistemic past state. From this we obtain two things. First, \((v',s)\in W^{M[U]}\) because epistemic past states have valid preconditions. Second, applying the fact that \(s \rightarrow ^U_a t\), it follows that \(s=t\) because \(\rightarrow _a\) arrows leaving epistemic past states are all reflexive. Since \(v' \leadsto ^M v\) and s is a past state, we conclude that \((v',s)\leadsto ^{M[U]} (v,s)=(v,t)\).
Case: \(w'=w\) and \(s'\leadsto ^U s\).
Since \(s'\leadsto ^U s \rightarrow ^U_a t\) and U satisfies knowledge of the past, there exists \(t' \leadsto ^U t\). Applying this to the assumption that U is history preserving and the fact that \((v,t)\in W^{M[U]}\), it follows that \((v,t') \in W^{M[U]}\). But then \((v,t') \leadsto ^{M[U]} (v,t)\).
Case: s is not a past state.
Since s is not a past state, there exists \(s' \leadsto ^U s\). Since U is history preserving and \((w,s)\in W^{M[U]}\), it follows that \((w,s')\in W^{M[U]}\). But then \((w,s') \leadsto ^{M[U]} (w,s)\), which contradicts our assumption that \({{\mathrm{d}}}(w,s)=0\).
Case: s is a past state.
Since U is history preserving and s is a past state, s is in fact an epistemic past state. Applying the fact that \(s \rightarrow ^U_a t\), it follows that \(s=t\) because \(\rightarrow _a\) arrows leaving epistemic past states are all reflexive. Since \((v',t')\leadsto ^{M[U]} (v,t)\) and \(t=s\) is a past state, it follows that \(t'=t=s\) and \(v\leadsto ^M v'\). Also, it follows from the fact that s is a past state and \({{\mathrm{d}}}(w,s)=0\) that we have \({{\mathrm{d}}}(w)=0\). Since M satisfies knowledge of the initial time, it follows from \({{\mathrm{d}}}(w)=0\) and \(w\rightarrow ^M_a v\) that \({{\mathrm{d}}}(v)=0\), but this contradicts \(v\leadsto ^M v'\).
Case: s is a past state.
Since s is a past state, if follows from \((v_1,t_1)\leadsto ^{M[U]}(w,s)\) and \((v_2,t_2)\leadsto ^{M[U]}(w,s)\) that we have \(s=t_1=t_2, v_1\leadsto ^M w\), and \(v_2\leadsto ^M w\). Since M satisfies uniqueness of the past, it follows that \(v_1=v_2\). Hence \((v_1,t_1)=(v_2,t_2)\).
Case: s is not a past state.
Since s is not a past state, if follows from \((v_1,t_1)\leadsto ^{M[U]}(w,s)\) and \((v_2,t_2)\leadsto ^{M[U]}(w,s)\) that we have \(w=v_1=v_2, t_1\leadsto ^U s\), and \(t_2\leadsto ^U s\). Since U satisfies uniqueness of the past, it follows that \(t_1=t_2\). Hence \((v_1,t_1)=(v_2,t_2)\).
Case: \(w'=w\) and \(s'\leadsto ^U s\).
Since \(s' \leadsto ^U s \rightarrow ^U_a t\) and U satisfies perfect recall, there exists \(t'\) satisfying \(s' \rightarrow ^U_a t' \leadsto ^U t\). Since U is history preserving and \((v,t)\in W^{M[U]}\), it follows that \((v,t')\in W^{M[U]}\). But then \((v,t')\leadsto ^{M[U]}(v,t)\). Since \(w\rightarrow ^M_av\) and \(s'\rightarrow ^U_at'\), we have \((w',s')=(w,s')\rightarrow ^{M[U]}_a(v,t')\).
Case: \(w'\leadsto ^M w\) and \(s'=s\) is a past state.
Since \(w' \leadsto ^M w \rightarrow ^M_a v\) and M satisfies perfect recall, there exists \(v'\) satisfying \(w' \rightarrow ^M_a v' \leadsto ^M v\). Further, since s is a past state and U is history preserving, s is an epistemic past state. From this two things follow. First, \((v',s)\in W^{M[U]}\) because epistemic past states have valid preconditions. Second, applying the fact that \(s\rightarrow ^U_a t\), it follows that \(s=t\) because \(\rightarrow _a\) arrows leaving epistemic past states are all reflexive. Since \(v'\leadsto ^M v\) and s is a past state, we have \((v',s)\leadsto ^{M[U]}(v,s)=(v,t)\). Further, since \(w'\rightarrow ^M_av'\) and \(s\rightarrow ^U_at=s\), we have \((w',s')=(w',s)\rightarrow ^{M[U]}_a(v',s)\).
Base case: \({{\mathrm{d}}}(t)=0\).
It follows that t is a past state. Since U is history preserving, t is an epistemic past state. Therefore, \(u\in W^M\) implies \((u,t)\in W^{M[U]}\) because epistemic past states have valid preconditions, and hence \(u\leadsto ^M u'\) implies \((u,t)\leadsto ^{M[U]}(u',t)\). It follows by an easy sub-induction on \({{\mathrm{d}}}(v)\) that \({{\mathrm{d}}}(v,t)={{\mathrm{d}}}(v)\). Since \({{\mathrm{d}}}(t)=0\), this proves (5).
Induction step: assume the result holds for events s with \({{\mathrm{d}}}(s)<{{\mathrm{d}}}(t)\) (the "induction hypothesis") and prove the result holds for event t with \({{\mathrm{d}}}(t)>0\).
Theorem 5 describes conditions under which properties of epistemic temporal models are preserved under updates. We will use this theorem later to show that a well-studied atemporal Dynamic Epistemic Logic approach to reasoning about time is limited to the class of Kripke models that necessarily satisfy all of the properties we have defined. This highlights one of the key advantages of our \(\mathsf {DETL}\) framework: it may be used to reason about situations that do or do not satisfy these (or other) properties. The choice is left to the user.
6 Connections with previous work
6.1 \(\mathsf {RDETL}\)
Theorem 5 studied the preservation of Kripke model properties under certain actions. We chose these properties because they have been of interest in many studies of time in Dynamic Epistemic Logic (van Benthem et al. 2009, 2007; Dégremont et al. 2011; Sack 2010, 2008; Yap 2011). We now focus our attention on the class of Kripke models that satisfy these properties. This provides a paradigmatic example demonstrating how our \(\mathsf {DETL}\) framework can be used to reason about a well-studied account of time in Dynamic Epistemic Logic.
Definition 9
(Restricted (forest-like) models) A Kripke model M is restricted (or forest-like) if it satisfies persistence of facts, depth-definedness, knowledge of the past, knowledge of the initial time, uniqueness of the past, and perfect recall (Definition 7). Let \(\mathfrak {R}\) be the class of all the restricted Kripke models and \(\mathfrak {R}_{*}\) the class of all pointed restricted Kripke models.
The restricted models satisfy all the constraints on Kripke models given in Definition 7. Although synchronicity was not explicitly named as one of the properties of a restricted model, it is not hard to show that synchronicity does follow from the other properties (argue by induction on the depth of worlds, making use of perfect recall, knowledge of the past, and knowledge of the initial time).
We now define a fragment of \({L_{\mathsf {DETL}}}\) whose update modals preserve these restricted models.
Definition 10
(Language \(L_{\mathsf {RDETL}}\)) The language \(L_{\mathsf {RDETL}}\) of restricted \(\mathsf {DETL}\) is the sublanguage of \({L_{\mathsf {DETL}}}\) obtained by removing all actions [U, s] that are based on an action model U that fails to satisfy one or more of persistence of facts, depth-definedness, knowledge of the past, history preservation, knowledge of the initial time, uniqueness of the past, or perfect recall. This removal applies recursively to preconditions as well.
The restrictions on the action models in \(L_{\mathsf {RDETL}}\) are those that appear in the Preservation Theorem (Theorem 5). Hence updating a restricted model by an action model in \(\mathfrak {A}(L_{\mathsf {RDETL}})\) yields another restricted model.
Definition 11
( \(\mathsf {RDETL}\) Semantics) We write \(M,w\models _{\mathsf {RDETL}}\varphi \) to mean that \((M,w)\in \mathfrak {R}_*\) and \(M,w\models \varphi \). We write \(\models _{\mathsf {RDETL}}\varphi \) to mean that \(M,w\models \varphi \) for every \((M,w)\in \mathfrak {R}_*\).
6.1.1 Proof system for \(\mathsf {RDETL}\)
Definition 12
( \(\mathsf {RDETL}\) Theory) The theory of Restricted Dynamic Epistemic Temporal Logic, \(\mathsf {RDETL}\), is defined in Fig. 8. We write \(\vdash _{\mathsf {RDETL}}\varphi \) to mean that \(\varphi \) is a theorem of \(\mathsf {RDETL}\).
Theorem 6
(Soundness and Completeness for \(\mathsf {RDETL}\)) \(\vdash _{\mathsf {RDETL}}\varphi \) iff \(\models _{\mathsf {RDETL}}\varphi \) for each \(\varphi \in L_{\mathsf {RDETL}}\).
Theorem 3 already establishes the soundness of the \(\mathsf {DETL}\) schemes and rules. Soundness for the remaining schemes is straightforward to prove.
The completeness proof can be divided into two stages. First, prove the Reduction Theorem: every \(L_\mathsf {RDETL}\)-formula is \(\mathsf {RDETL}\)-provably equivalent to an action model-free formula in \({L_{\mathsf {SETL}}}\). This follows by the proof of Theorem 2. Second, prove completeness of action model-free formulas with respect to the class of restricted Kripke models: \(\nvdash _\mathsf {RDETL}\psi \) for a given \(\psi \in {L_{\mathsf {SETL}}}\) implies there is a restricted situation (M, w) for which \(M,w\not \models \psi \). We outline a proof of the second stage.
\(W^{\varOmega \times \mathbb {Z}}\mathop {=}\limits ^{ \text{ def }}W^\varOmega \times \mathbb {Z}\).
For each \(a\in \fancyscript{A}\): \((w,k)\rightarrow ^{\varOmega \times \mathbb {Z}}_a (w',k')\) if and only if \(w\rightarrow _a^\varOmega w'\) and \(k=k'\).
Open image in new window if and only if Open image in new window and \(k'=k-1\).
\(V^{\varOmega \times \mathbb {Z}}(p) \mathop {=}\limits ^{ \text{ def }}V^\varOmega (p) \times \mathbb {Z}\).
Open image in new window , where \(R^*\) denotes the reflexive-transitive closure of a binary relation R.
For each \(a\in \fancyscript{A}\): \({\rightarrow _a^M}\mathop {=}\limits ^{ \text{ def }}{\rightarrow _a^{\varOmega \times \mathbb {Z}}}\cap (W^M\times W^M)\).
\(V^M(p)\mathop {=}\limits ^{ \text{ def }}V^{\varOmega \times \mathbb {Z}}(p)\cap W^M\).
\(W^{M'}\mathop {=}\limits ^{ \text{ def }}\{(w,k)\in W^M\mid 0\le k\le m\}\).
For each \(a\in \fancyscript{A}\): \({\rightarrow _a^{M'}}\mathop {=}\limits ^{ \text{ def }}{\rightarrow _a^M}\cap (W^{M'}\times W^{M'})\).
\(V^{M'}(p)\mathop {=}\limits ^{ \text{ def }}V^M(p)\cap W^{M'}\).
\(W^F\mathop {=}\limits ^{ \text{ def }}\{[w,k]\mid (w,k)\in W^{M'}\}\).
For each \(a\in \fancyscript{A}\): \(A\rightarrow ^F_a B\) iff \(\exists (w,k)\in A\) and \(\exists (v,j)\in B\) with \((w,k)\rightarrow ^{M'}_a(v,j)\).
Open image in new window iff \(\exists (w,k)\in A\) and \(\exists (v,j)\in B\) with Open image in new window .
\(V^F(p)\mathop {=}\limits ^{ \text{ def }}\{A\in W^F\mid p\in \mathsf {Cl}_m(\lnot \psi ) \text { and } \forall (w,k)\in A:M',(w,k)\models p\}\).
Truth preservation: By what we have shown above, it follows that for each \((w,k)\in W^\varOmega \times \{0,\dots ,m\}\) and each \(\varphi \in \mathsf {Cl}_k(\lnot \psi )\), we have \(\varOmega ,w\models \varphi \) if and only if \(F,[w,k]\models \varphi \). In particular, we have \(F,[\varGamma _{\lnot \psi },m]\not \models \psi \). So to complete the proof, it suffices for us to show that \(F\in \mathfrak {R}\) (i.e., F is a restricted model).
- F satisfies uniqueness of the past:Suppose not. From \([w',k']\leadsto ^F[w,k]\) and \([w'',k'']\leadsto ^F[w,k]\), we have \(k'=k''=k-1\). From \([w',k-1]\ne [w'',k-1]\), it follows that there exists \(\varphi \in \mathsf {Cl}_{k-1}(\lnot \psi )\) such that, without loss of generality, \(F,[w',k-1]\models \varphi \) and \(F,[w'',k-1]\not \models \varphi \). Defining$$\begin{aligned} ([w',k']\leadsto ^F[w,k] \wedge [w'',k'']\leadsto ^F[w,k])\Rightarrow ([w',k']=[w'',k'']). \end{aligned}$$we have \(\chi \in \mathsf {Cl}_k(\lnot \psi )\) and \(F,[w,k]\not \models \chi \) and hence that \(\varOmega ,w\not \models \chi \) by Truth preservation. But then it follows by the Truth Lemma that the maximal consistent set w fails to contain an instance \(\chi \) of the Uniqueness of the Past axiom, a contradiction.$$\begin{aligned} \chi \mathop {=}\limits ^{ \text{ def }}\lnot [Y]\varphi \rightarrow [Y]\lnot \varphi , \end{aligned}$$
- F satisfies persistence of facts:Suppose not. Then we have$$\begin{aligned}{}[w,k]\leadsto ^F[v,j] \Rightarrow ([w,k]\in V^F(p)\Leftrightarrow [v,j]\in V^F(p)). \end{aligned}$$Let \(\chi \mathop {=}\limits ^{ \text{ def }}[Y]p\leftrightarrow (\lnot [Y]\bot \rightarrow p)\). Since F satisfies uniqueness of the past, it follows from (6) that \(F,[v,j]\not \models \chi \). Since \([w,k]\leadsto ^F[v,j]\), we have \(j\ge 1\). Further, it follows by (6) that \([w,k]\in V^F(p)\) or \([v,j]\in V^F(p)\). Applying the definition of \(V^F(p)\), we have that \(p\in \mathsf {Cl}_m(\lnot \psi )\) and therefore that \(p\in \mathsf {Cl}_0(\lnot \psi )\). So since \(j\ge 1\), we have \(\chi \in \mathsf {Cl}_j(\lnot \psi )\). But then it follows from \(F,[v,j]\not \models \chi \) by Truth preservation that \(\varOmega ,v\not \models \chi \). Applying the Truth Lemma, the maximal consistent set v fails to contain an instance \(\chi \) of the Persistence of Facts axiom, a contradiction.$$\begin{aligned} \lnot ([w,k]\in V^F(p)\Leftrightarrow [v,j]\in V^F(p)). \end{aligned}$$(6)
F is depth-defined: \({{\mathrm{d}}}([w,k])\ne \infty \).
For each \([v,j]\in W^F\), we have \(0\le j\le m\). Further, Open image in new window implies \(j'=k'-1\). It follows that \({{\mathrm{d}}}([w,k])\ne \infty \).
- F satisfies knowledge of the past:Suppose not. Letting \(\chi \mathop {=}\limits ^{ \text{ def }}\lnot [Y]\bot \rightarrow \Box _a\lnot [Y]\bot \), it follows that \(F,[w,k]\not \models \chi \). Further, from \([w',k']\leadsto ^F[w,k]\), we have \(k\ge 1\) and therefore that \(\chi \in \mathsf {Cl}_k(\lnot \psi )\). But then it follows by Truth preservation that \(\varOmega ,w\not \models \chi \). Applying the Truth Lemma, the maximal consistent set w fails to contain an instance \(\chi \) of the Uniqueness of the Past axiom, a contradiction.$$\begin{aligned} ([w',k']\leadsto ^F[w,k]\rightarrow ^F_a[v,j])\Rightarrow \exists [v',j']([v',j']\leadsto ^F[v,j]). \end{aligned}$$
- F satisfies knowledge of the initial time:Suppose \([w,k]\rightarrow ^F_a[v,j]\) and \(\lnot \exists [w',k']([w',k']\leadsto ^F[w,k])\). If \(k=0\), then it follows by \([w,k]\rightarrow ^F_a[v,j]\) that \(j=0\) and therefore that \(\lnot \exists [v',j']([v',j']\leadsto ^F[v,j])\) by Trimming. So let us assume that \(k>0\). Further, toward a contradiction, we assume that \(\exists [v',j']([v',j']\leadsto ^F[v,j])\). Letting \(\chi \mathop {=}\limits ^{ \text{ def }}[Y]\bot \rightarrow \Box _a[Y]\bot \), it follows that \(F,[w,k]\not \models \chi \). But since \(k>0\), we have \(\chi \in \mathsf {Cl}_k(\lnot \psi )\) and hence it follows by Truth preservation that \(\varOmega ,w\not \models \chi \). Applying the Truth Lemma, the maximal consistent set w fails to contain an instance \(\chi \) of the Knowledge of the Initial Time axiom, a contradiction.$$\begin{aligned}&[w,k]\rightarrow ^F_a[v,j]\wedge \lnot \exists [w',k']([w',k']\leadsto ^F[w,k])\\&\quad \Rightarrow \lnot \exists [v',j']([v',j']\leadsto ^F[v,j]). \end{aligned}$$
- F satisfies perfect recall:Suppose \([w,k]\leadsto ^F[v,j]\rightarrow ^F_a[v',j']\). Then \(k+1=j=j'\). Now \([v,k+1]=[v,j]\rightarrow ^F_a[v',j']=[v',k+1]\) implies \(\exists (v_*,k+1)\in [v,k+1]\) and \(\exists (v'_*,k+1)\in [v',k+1]\) with \((v_*,k+1)\rightarrow ^{M'}_a(v'_*,k+1)\). Hence \(v_*\rightarrow ^\varOmega _av'_*\). Now from \([w,k]\leadsto ^F[v,j]=[v,k+1]\), we have that \(F,[v,k+1]\models \lnot [Y]\bot \). Since \(k+1\ge 1\), it follows that \(\lnot [Y]\bot \in \mathsf {Cl}_{k+1}(\lnot \psi )\) and therefore we have by Truth preservation that \(\varOmega ,v_*\models \lnot [Y]\bot \). By the definition of truth, it follows that there is a \(w_*\in W^\varOmega \) with \(w_*\leadsto ^\varOmega v_*\). But then \([w_*,k]\leadsto ^F[v,j]=[v,k+1]\), from which it follows by uniqueness of the past for F that \([w_*,k]=[w,k]\) and therefore that \((w_*,k)\in [w,k]\). Now \(\varOmega \) satisfies perfect recall (for if it did not, we could find a violation of an instance of the Perfect Recall axiom at a maximal consistent set, a contradiction). Therefore, since we have \(w_*\leadsto ^\varOmega v_*\rightarrow ^\varOmega _a v'_*\), it follows by perfect recall for \(\varOmega \) that there is a \(w'_*\in W^\varOmega \) satisfying \(w_*\rightarrow ^\varOmega _a w'_*\leadsto ^\varOmega v'_*\). But then \([w,k]=[w_*,k]\rightarrow ^\varOmega _a[w'_*,k]\leadsto ^\varOmega [v'_*,k+1]=[v',k+1]=[v',j]\). \(\square \)$$\begin{aligned} ([w,k]\leadsto ^F[v,j]\rightarrow ^F_a[v',j'])\Rightarrow \exists [w',k']([w,k]\rightarrow ^F_a[w',k']\leadsto ^F[v',j']). \end{aligned}$$
6.2 \(\mathsf {YDEL}\)
In this section, we relate \(\mathsf {DETL}\) to a more conservative approach to adding time to \(\mathsf {DEL}\), which, as is generally studied in the literature (Baltag and Moss 2004; Baltag et al. 1998, 2008; van Benthem et al. 2006; van Ditmarsch et al. 2007), does not use \(\leadsto \) arrows in its action models. Further, the semantics of \(\mathsf {DEL}\) does not use Kripke models with designated time-keeping arrows \(\leadsto \). In order to draw this comparison, we will define an extension of \(\mathsf {DEL}\) called "Yesterday Dynamic Epistemic Logic," or \(\mathsf {YDEL}\) (see Sack 2008, 2010; Yap 2011), that records a history of the updates made. We will then show that \(\mathsf {YDEL}\) reasoning can be done within the \(\mathsf {DETL}\) setting, since (modulo translation) \(\mathsf {YDEL}\) is sound and complete with respect to a particular class of \(\mathsf {DETL}\) models.
Definition 13
\({L_{\mathsf {YDEL}}}\) is the atemporal fragment of \({L_{\mathsf {DETL}}}\). For reasons explained in a moment, we assume that the special symbol \(\flat \) is used neither as a world nor as an event in \({L_{\mathsf {YDEL}}}\).
We will evaluate \(\mathsf {YDEL}\) formulas on restricted Kripke models (Definition 9).
Definition 14
The forthcoming Corollary 1 shows that \(M\oplus U\in \mathfrak {R}\) whenever \(M\in \mathfrak {R}\) and U is atemporal. The function of the symbol \(\flat \) is to serve as an epistemic past state, preserving a copy of M in \(M \oplus U\) (Lemma 1). Since \(\mathsf {YDEL}\) uses atemporal action models, which contain no \(\leadsto \) arrows, the mechanism for preserving the previous model M is "hardcoded" in the semantics. However, by defining a translation from \({L_{\mathsf {YDEL}}}\) to \({L_{\mathsf {DETL}}}\) (Definition 15), we will be able to show that "atemporal" \(\mathsf {YDEL}\) reasoning can be captured in \(\mathsf {DETL}\).
Lemma 1
Let (M, w) be a situation and (U, s) be an atemporal action satisfying \(M,w\models \mathsf {pre}^U(s)\). The function \(f:W^M\rightarrow W^{M\oplus U}\) defined by \(f(w)\mathop {=}\limits ^{ \text{ def }}(w,\flat )\) is a bisimulation.
w and \((w,\flat )\) have the same valuation. If \(f(w)=(w,\flat ) \rightarrow ^{M \oplus U}_a (v,t)\), then \(t=\flat \) and \(w \rightarrow ^M_a v\). If \(w \rightarrow ^M_a v\), then \((w, \flat ) \rightarrow ^{M \oplus U}_a (v,\flat )\).\(\square \)
Before defining the translation from \(\mathsf {YDEL}\) to \(\mathsf {DETL}\), we will first show how \(\mathsf {YDEL}\) works by illustrating the way in which \(M \oplus U\) is constructed.
Example 6
Figure 9 pictures an initial situation and a \(\mathsf {YDEL}\) action. In the initial situation, neither agent knows whether p is true. The action informs a that p is true but tells b only that a was either informed of p or provided with trivial information. After applying the action to the situation, we obtain the resultant situation in Fig. 10.
We now show how \(\mathsf {YDEL}\) reasoning is captured in \(\mathsf {DETL}\).
6.2.1 Translation of \(L_\mathsf {YDEL}\) into \(L_\mathsf {DETL}\)
We define a translation from \(\mathsf {YDEL}\) formulas and action models to \(\mathsf {DETL}\) formulas and action models. This translation acts on action models by adding a new epistemic past state \(\flat \) along with an arrow \(\flat \leadsto s\) to each action s. See Fig. 11 for an example.
Definition 15
The function \(\sharp \) transforms the atemporal action models used by \(\mathsf {YDEL}\) into \(\mathsf {DETL}\) action models having epistemic past states. As it turns out, such action models are in fact \(\mathsf {RDETL}\) action models (Definition 10).
Lemma 2
If U is an atemporal action model, then \(U^\sharp \in \mathfrak {A}(L_{\mathsf {RDETL}})\).
The proof of this lemma is straightforward. It follows that the image of \(\sharp \) is contained in \(L_{\mathsf {RDETL}}\cup \mathfrak {A}(L_{\mathsf {RDETL}})\). This containment is strict: every history in \(U^\sharp \) has length 1, while the length of histories in \(\mathsf {RDETL}\) action models is unbounded.
Theorem 7
- (a)
\(M\oplus U=M[U^\sharp ]\), and
- (b)
\(M,w\models _\mathsf {YDEL}\varphi \) iff \(M,w\models _\mathsf {RDETL}\varphi ^\sharp \).
- 1.
For each \(M\in \mathfrak {R}\) and each \(U\in \mathfrak {A}^a(L_i)\): \(M\oplus U=M[U^\sharp ]\).
- 2.For each \((M,w)\in \mathfrak {R}_*\) and each \(\varphi \in L_i\):$$\begin{aligned} M,w\models _\mathsf {YDEL}\varphi \ \textit{iff}\ M,w\models _\mathsf {RDETL}\varphi ^\sharp . \end{aligned}$$
\(t,t'\ne \flat \) and \(t\rightarrow ^U_at'\); or
\(t=t'=\flat \).
\(t=\flat , t'\ne \flat \), and \(v=v'\); or
\(t=t'=\flat \) and \(v\leadsto ^M v'\).
\(v\leadsto ^Mv', t=t'\), and t is a past state; or
\(v=v'\) and \(t\leadsto ^{U^\sharp } t'\).
Finally, we have \((v,t)\in V^{M\oplus U}(p)\) if and only if \(v\in V^M(p)\) if and only if \((v,t)\in V^{M[U^\sharp ]}(p)\). Here we made tacit use of the fact that \(W^{M\oplus U}=W^{M[U^\sharp ]}\). Conclusion: \(V^{M\oplus U}=V^{M[U^\sharp ]}\).
This completes the proof of Statement 1. The proof of Statement 2 then proceeds by a sub-induction on the construction of \(L_{i+1}\)-formulas. Most cases are obvious, so we only address the case for \(L_{i+1}\)-formulas \([U,s]\varphi \). Proceeding, we have \(M,w\models _\mathsf {YDEL}[U,s]\varphi \) if and only if \(M,w\not \models _\mathsf {YDEL}\mathsf {pre}^U(s)\) or \(M\oplus U,(w,s)\models _\mathsf {YDEL}\varphi \). By Statement 2 of the induction hypothesis, the latter is equivalent to "\(M,w\not \models _\mathsf {RDETL}\mathsf {pre}^U(s)^\sharp \) or \(M\oplus U,(w,s)\models _\mathsf {RDETL}\varphi ^\sharp \)," which is itself equivalent to "\(M,w\not \models _\mathsf {RDETL}\mathsf {pre}^{U^\sharp }(s)\) or \(M[U^\sharp ],(w,s)\models _\mathsf {RDETL}\varphi ^\sharp \)" (by the definition of \(U^\sharp \) for the left disjunct and Statement 1 of the induction hypothesis for the right). But this is equivalent to \(M,w\models _\mathsf {RDETL}[U^\sharp ,s]\varphi ^\sharp \) by the \(\mathsf {RDETL}\) semantics. Since \([U^\sharp ,s]\varphi ^\sharp =([U,s]\varphi )^\sharp \), the result follows. \(\square \)
A corollary of Theorem 7 is that restricted models are closed under the \(\mathsf {YDEL}\) update operation \(M\mapsto M\oplus U\).
Corollary 1
If \(M\in \mathfrak {R}, U\in \mathfrak {A}({L_{\mathsf {YDEL}}})\), and \(W^{M\oplus U}\ne \emptyset \), then \(M\oplus U\in \mathfrak {R}\).
Fix \(M\in \mathfrak {R}\) and \(U\in \mathfrak {A}({L_{\mathsf {YDEL}}})\) with \(W^{M\oplus U}\ne \emptyset \). Since \(U\in \mathfrak {A}({L_{\mathsf {YDEL}}})\) if and only if U is atemporal (Definition 13), it follows by Lemma 2 that \(U^\sharp \in \mathfrak {A}(L_{\mathsf {RDETL}})\). Applying Preservation (Theorem 5) and the definition of \(L_{\mathsf {RDETL}}\) (Definition 10), we have \(M[U^\sharp ]\in \mathfrak {R}\). By Theorem 7, \(M\oplus U=M[U^\sharp ]\in \mathfrak {R}\). \(\square \)
6.2.2 Connecting the theories of \(\mathsf {YDEL}\) and \(\mathsf {RDETL}\)
Definition 16
The theory \(\mathsf {YDEL}\) is defined in Fig. 12. Note that all axioms and rules refer to formulas in \({L_{\mathsf {YDEL}}}\) and hence to action models in \(\mathfrak {A}({L_{\mathsf {YDEL}}})\).
Theorem 8
The theory of \(\mathsf {YDEL}\) is sound and complete with respect to \(\mathfrak {R}_{*}\).
Soundness for \([U,s][Y]\varphi \leftrightarrow (\mathsf {pre}^U(s)\rightarrow \varphi )\).
We first prove the left-to-right direction of the equivalence. Suppose \(M,w \models [U,s][Y] \varphi \) and \(M,w \models \mathsf {pre}^U(s)\). This implies that for every \((v,t) \leadsto ^{M \oplus U} (w,s)\), we have \(M \oplus U, (v,t) \models \varphi \). By definition of \(M\oplus U\), we have \((w, \flat ) \leadsto ^{M \oplus U} (w,s)\), and so \(M \oplus U (w,\flat ) \models \varphi \). By Lemma 1, \(M,w \models \varphi \). Now we prove the right-to-left direction. Suppose \(M,w \models \mathsf {pre}^U(s)\) and \(M,w \models \varphi \) (the case where \(M,w\not \models \mathsf {pre}^U(s)\) is immediate). By definition of \(M\oplus U\) and uniqueness of the past, \((w,t) \leadsto ^{M \oplus U} (w,s)\) implies \(t=\flat \). By the fact that \(M,w \models \varphi \) and Lemma 1, we have \(M \oplus U, (w,\flat ) \models \varphi \). Hence \(M,w \models [U,s][Y] \varphi \).
Soundness for (UN) follows from the fact that restricted models are closed under the operation \(M\mapsto M\oplus U\) (Corollary 1).
Corollary 2
7 Conclusion
We have presented Dynamic Epistemic Temporal Logic (\(\mathsf {DETL}\)), a general framework for reasoning about transformations on Kripke models with a designated timekeeping relation Open image in new window . Our "temporal" action models are a generalization of the atemporal action models familiar from Dynamic Epistemic Logic. We showed by way of a number of examples how temporal action models can be used to reason about and control the flow of time. We also highlighted some key design choices that allow this framework to avoid conceptual complications relating to time and that enable us to define actions that preserve a complete copy of the past state of affairs. This leads to one natural choice for understanding time: the time of a world is the depth of that world (i.e., the maximum number of "backward" temporal steps one can take from that world, whenever this maximum exists).
Kripke models with a designated timekeeping relation are essentially the models of Epistemic Temporal Logic. Therefore, one way of understanding our work is as follows: we extend the domain of action model operations from those on (atemporal) Kripke models to (what are essentially) the models of Epistemic Temporal Logic. We showed that a number of properties that may arise in the latter models—such as Persistence of Facts, Perfect Recall, and Synchronicity—are preserved under the application of temporal action models that themselves satisfy certain related properties. This makes it possible to use our \(\mathsf {DETL}\) framework to develop Dynamic Epistemic Logic-style theories of temporal Kripke models. Such logics can be used to reason about objective changes in time along with the agents' basic and higher-order knowledge and beliefs about changes in this structure. As an example, we showed how the \(\mathsf {DETL}\) approach can be used to define the logic \(\mathsf {RDETL}\) of "restricted" Dynamic Epistemic Temporal Logic, which is essentially the Dynamic Epistemic Logic of synchronous actions with the "yesterday" temporal operator [Y]. We proved that \(\mathsf {RDETL}\) reasoning captures the reasoning of \(\mathsf {YDEL}\), the first Dynamic Epistemic Logic of synchronous time with the yesterday modal.
The \(\mathsf {DETL}\) approach is not, however, limited to synchronous systems. We presented one example where a synchronous model is transformed into an asynchronous one, leaving one agent sure that two clock ticks occurred, and the other uncertain as to whether it was one or two. We contrasted this with a synchronous variant in which the agents' knowledge about atemporal information is the same, but the knowledge change is compressed into a single clock tick that is common knowledge. Here we see that the difference is easily discernible by a simple examination of the temporal action models involved. In essence, our theory extends the types of knowledge change describable by atemporal action models to the temporal setting, which gives us a great deal of control as to the relationship between how much time passes and what the agents perceive of this passage. And we of course also inherit many features (and drawbacks) of the atemporal action model approach.
One direction for future work is to extend our temporal language to include more than just the one-step "yesterday" operator Y. For example, it would also be interesting (and challenging) to consider backward-looking "since" operator and other operators familiar from temporal logic (Goldblatt 2006).10
In closing, we mention a recent study of time in Dynamic Epistemic Logic that looks at asynchronous systems (Dégremont et al. 2011). The basic idea is that an atemporal action model operates on a temporal Kripke model in such a way that an agent experiences a single clock tick if her knowledge of atemporal information changes, but will otherwise be uncertain as to whether the clock ticked. So, for example, if agent a does not know p, a public announcement of p will transform her knowledge in a synchronous manner: the clock will tick once, she will learn p, and she will know that the clock ticked once. But if the public announcement of p then occurs again, the clock will tick but, since she already knows p and hence her atemporal knowledge will not change, she will be uncertain as to whether the clock ticked once or not at all. The result is an asynchronous situation.
Though we have shown (by way of an example) that \(\mathsf {DETL}\) can reason about some asynchronous updates, we have not proved that it can reason about every such update. Nor have we shown that it can reason about a certain class of asynchronous updates that can be independently identified according to some desirable properties it satisfies. In particular, it is not clear if there is a \(\mathsf {DETL}\) action model for all the updates that can be produced by the framework of Dégremont et al. (2011). Moreover, the latter approach is based on "protocols" constraining the sequences of actions that can occur, something we have left out of the present study for simplicity. Another complication is that the asynchronous updates of Dégremont et al. (2011) essentially insert agent arrows \(\rightarrow _a\) based on whether a certain knowledge condition is satisfied, whereas our temporal action models do not allow us to conditionally insert arrows. This suggests that there may be connections with "arrow update logics" (Kooi and Renne 2011a, b) that allow such conditions on arrows. In particular, it has been shown that generalized arrow updates are equivalent to atemporal action models in terms of update expressivity (Kooi and Renne 2011b). Therefore, an arrow update version of \(\mathsf {DETL}\) might suggest a natural way to represent asynchronous updates like those of Dégremont et al. (2011), and this may turn out to be equivalent in update expressivity to our present approach, just as in the atemporal case. If this is so, then it may be the case that "conditional" arrow changes are already within the scope of our current approach, albeit indirectly.
In conclusion, we believe that \(\mathsf {DETL}\) presents a viable option for developing Dynamic Epistemic Logic-style theories of Epistemic Temporal Logic. While this paper [and its early predecessor (Renne et al. 2009)] present the first steps of this study, there is clearly still much more work to be done.
- 1.
For all structures X, let \(\leadsto ^X\) denote the converse of Open image in new window and let \(\leftarrow ^X_a\) denote the converse of \(\rightarrow ^X_a\). Our discussion of temporal issues will typically use \(\leadsto \) rather than Open image in new window because the former follows the natural direction of time's flow. Here and elsewhere, we will omit superscripts on relations when doing so ought not cause confusion.
- 2.
We note that because synchronicity requires the structure to be depth-defined and perfect recall does not, perfect recall does not imply synchronicity. However, the conjunction of perfect recall, depth-definedness, and uniqueness of the past are together equivalent to the conjunction of synchronicity and uniqueness of the past. See Goranko and Pacuit (2014) for a discussion of a weaker version of perfect recall that does not stand in a similar relationship to synchronicity. In the interest of simplicity, we do not consider this more complicated weaker version here.
- 3.
Formally, a \({L_{\mathsf {DETL}}}\)-formula \(\varphi \) is true at a world x if and only if \(\varphi \) is true at x even after we delete all worlds y satisfying the property that every path from x to y contains at least one \(\leadsto \) arrow (followed in the "forward" direction \(z\leadsto z'\) from "past" z to "future" \(z'\)). This is so because \({L_{\mathsf {DETL}}}\) has no [T] operator, as defined in (1).
- 4.
This is similar to the way in which the "do nothing" Propositional Dynamic Logic (PDL) program \( skip \) does not change the state of the system. However, there is a difference: the PDL program does not change the structure of the model, though the action \((U_3,t)\) does. Nevertheless, from the point of view of language equivalence, this change is inconsequential: the "before" situation and the "after" situation satisfy the same \({L_{\mathsf {DETL}}}\)-formulas, and so our intention is that these situations are to be identified.
- 5.
While these may not have the typical "look" of reduction axioms as they are commonly found in Dynamic Epistemic Logics, they can nevertheless be considered reduction axioms in the sense that they allow us to prove the reduction to \({L_{\mathsf {SETL}}}\) as per Theorem 2.
- 6.
The primary difference is with those concerning the Y-modality. There are two cases: s is a past state, and s is not a past state. In both cases, U[Y] is a simplification of U\(\Box _a\), reflecting the involvement of asynchronous composition rather than synchronous (see the discussion after Definition 5). In U\(\Box _a\), the conjunction reflects the transitions made in the action model, while the modality \(\Box _a\) that follows reflects the transitions made in original model. Note that if s is a past state, then there is no \(s'\leadsto ^U s\), so we can remove the conjunction. If s not a past state, then it is the first coordinate rather than the second coordinate that must be fixed in a \(\leadsto \) transition in the updated model. Hence we remove the modality [Y] that would otherwise follow the conjunction.
- 7.
The axiomatization of the validities of the action model-free sublanguage \({L_{\mathsf {SETL}}}\) are obtained from the axiomatization of \(\mathsf {DETL}\) by deleting each of the reduction axioms, deleting the rule UN, and restricting the language to that of \({L_{\mathsf {SETL}}}\). What results is just multi-modal \(\mathsf {K}\), with one \(\mathsf {K}\) modality for each agent modal \(\Box _a\) and one \(\mathsf {K}\) modality for the yesterday modal [Y]. Completeness thereby follows by the standard construction (e.g., in (Blackburn et al. 2001, Chap. 4) using the "modal similarity type" of \({L_{\mathsf {SETL}}}\)).
- 8.
In detail: a bisimulation is a nonempty binary relation B between the worlds of Kripke models (with yesterday) Open image in new window and Open image in new window such that \(wBw'\) implies w and \(w'\) satisfy the same propositional letters; and, for each binary relation symbol Open image in new window specified by the structures, \(wBw'\) and \(wR^Mv\) implies there is a \(v'\in W^{M'}\) such that \(w'R^{M'}v'\) and \(vBv'\), and \(wBw'\) and \(w'R^{M'}v'\) implies there is a \(v\in W^M\) such that \(wR^Mv\) and \(vBv'\). Note that the definition of bisimulation only considers temporally reachable worlds "in the past" (i.e., in the direction from x to y in the arrow Open image in new window ).
- 9.
- 10.
Thanks to an anonymous reviewer for this suggestion.
The authors thank the reviewers for their feedback and suggestions. Bryan Renne was funded by Veni grant 275-20-030 from the Netherlands Organisation for Scientific Research (NWO). Joshua Sack was funded by Vidi grant 639-072-904 from the NWO.
- Aceto, L., Fokkink, W., & Verhoef, C. (2001). Structural operational semantics. In J. A. Bergstra, A. Ponse, & S. A. Smolka (Eds.), Handbook of process algebra. Amsterdam: Elsevier.Google Scholar
- Balbiani, P., Baltag, A., van D., H., Herzig, A., Hoshi, T., & de Lima, Tiago. (2008). Knowable' as 'known after an announcement. The Review of Symbolic Logic, 1(3), 305–334.CrossRefGoogle Scholar
- Baltag, A., & Moss, L. S. (2004). Logics for epistemic programs. Synthese, 139(2), 165–224.CrossRefGoogle Scholar
- Baltag, A., Moss, L. S., & Solecki, S. (1998). The logic of public announcements, common knowledge, and private suspicions. In I. Gilboa (Eds..), Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge (TARK VII) (pp. 43–56), Evanston, Illinois, USA.Google Scholar
- Baltag, A., van Ditmarsch, H. P., & Moss, L. S. (2008). Epistemic logic and information update. In P. Adriaans & J. van Benthem (Eds.), Handbook on the philosophy of information (pp. 369–463). Amsterdam: Elsevier.Google Scholar
- Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal logic. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
- Dégremont, C., Löwe, B., & Witzel, A. (2011). The synchronicity of dynamic epistemic logic. In K. R. Apt (Eds.), Proceedings of the 13th Conference on Theoretical Aspects of Rationality and Knowledge (TARK XIII), (pp. 145–152).Google Scholar
- Goldblatt, R. (2006). Logics of time and computation, volume 7 of CSLI Lecture Notes. Center for the study of language and information. Berlin: Springer.Google Scholar
- Goranko, V., & Pacuit, E. (2014). Temporal aspects of the dynamics of knowledge. In A. Baltag & S. Smets (Eds.), Johan van Benthem on logic and information dynamics, outstanding contributions to logic. Berlin: Springer.Google Scholar
- Hoshi, T. (2009). Epistemic dynamics and protocol information. PhD thesis, Stanford University.Google Scholar
- Hoshi, T. (2010). Merging DEL and ETL. Journal of Logic, Language, and Information, 19(4), 413–430.CrossRefGoogle Scholar
- Hoshi, T., & Yap, A. (2009). Dynamic epistemic logic with branching temporal structures. Synthese, 169(2), 259–281.CrossRefGoogle Scholar
- Kooi, B., & Renne, B. (2011). Arrow update logic. Review of Symbolic Logic, 4(4), 536–559.CrossRefGoogle Scholar
- Kooi, B., & Renne, B. (2011). Generalized arrow update logic. In K. R. Apt (Ed.), Proceedings of the 13th Conference of Theoretical Aspects of Rationality and Knowledge (TARK XIII) (pp. 205–211), Groningen, The Netherlands.Google Scholar
- Parikh, R., & Ramanujam, R. (2003). A knowledge based semantics of messages. Journal of Logic, Language, and Information, 12, 453–467.CrossRefGoogle Scholar
- Renne, B., Sack, J., & Yap, A. (2009). Dynamic epistemic temporal logic. In X. He, J. Horty, & E. Pacuit (Eds.), Logic, rationality, and interaction, second international workshop, LORI 2009, Chongqing, China, 8–11 October 2009. Proceedings, volume 5834/2009 of Lecture Notes in Computer Science (pp. 263–277). Berlin/Heidelberg: Springer.Google Scholar
- Sack, J. (2008). Temporal languages for epistemic programs. Journal of Logic, Language, and Information, 17(2), 183–216.CrossRefGoogle Scholar
- Sack, J. (2010). Logic for update products and steps into the past. Annals of Pure and Applied Logic, 161(12), 1431–1461.CrossRefGoogle Scholar
- van Benthem, J., Gerbrandy, J., Hoshi, T., & Pacuit, E. (2009). Merging frameworks for interaction. Journal of Philosophical Logic, 38(5), 491–526.CrossRefGoogle Scholar
- van Benthem, J., Gerbrandy, J., & Pacuit, E. (2007). Merging frameworks for interaction: DEL and ETL. In Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge (TARK XI) (pp. 72–81).Google Scholar
- van Benthem, J., van Eijck, J., & Kooi, B. (2006). Logics of communication and change. Information and Computation, 204(11), 1620–1662.CrossRefGoogle Scholar
- van Ditmarsch, H., van der Hoek, W., & Kooi, B. (2007). Dynamic epistemic logic (synthese library). Dordrecht: Springer.CrossRefGoogle Scholar
- van Glabbeek, R. J. (2001). The linear time-branching time spectrum I—The semantics of concrete, sequential processes. In J. A. Bergstra, A. Ponse, & S. A. Smolka (Eds.), Handbook of process algebra (pp. 3–99). Amsterdam: Elsevier.CrossRefGoogle Scholar
- Yap, A. (2011). Dynamic epistemic logic and temporal modality. In P. Girard, O. Roy, & M. Marion (Eds.), Dynamic formal epistemology, volume 351 of synthese library (pp. 33–50). New York: Springer.CrossRefGoogle Scholar
Copyright information
Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.


text:
If you're following the schedule, you should read these chapters today: Deuteronomy 6, Psalm 89, Isaiah 34, Revelation 4. Click on any of those references to see all the passages in one long page on BibleGateway. If you can't do all the readings today, read Deuteronomy 6.
It is impossible for people to know how many federal laws there are that are currently in existence. Way back in 1982, the Department of Justice spent 2 years attempting to count the number of federal criminal laws; they came up with an estimate of 3,000. But that was a long time ago and many more criminal laws have been passed. There are also many, many civil laws and other regulations that have the force of law.
In other words, as one pundit put it, you're probably breaking some kind of law right now. Although Israel's law may seem oppressive and, in many cases, strange, it was a fairly simple law code. At least the laws can be counted and exist all in one place. Yet it is common for unbelievers and, sometimes, believers, to complain that the Old Testament law is oppressive. According to our passage today, however, God's law is not oppressive but a gateway to freedom. Verse 2b tells us that God gave Israel the law so that, "…you, your children and their children after them may fear the Lord your God as long as you live by keeping all his decrees and commands that I give you, and so that you may enjoy long life." Obey God's law, and long life will be yours. Simple.
Likewise, verse 25 says, "And if we are careful to obey all this law before the Lord our God, as he has commanded us, that will be our righteousness." Want to be righteous before God? Keep his laws and all will be well—spiritually and otherwise—in your life.
If it is true that God's law to Israel was designed for their good and that it is relatively simple compared to our system of laws, then why didn't Israel just obey it and reap the benefits God provided? The answer, of course, is sin. While keeping God's law perfectly could make one righteous in theory, in reality it could never make anyone righteous before God. One, nobody can keep God's law perfectly because we will slip up and sin; two, even if we kept God's law perfectly, we would still have original sin that was imputed to us when Adam and Eve fell. So, although God's law offered his people a pathway to a long, economically prosperous and morally righteous life, in reality, it was an impossible pathway to follow successfully. This uncovers the real reason for God's law: "Therefore no one will be declared righteous in God's sight by the works of the law; rather, through the law we become conscious of our sin" (Rom 3:20). God's law showed us what God demands of us morally but our attempts to follow it show us how completely we are morally damaged. When anyone realizes how impossible it is to keep God's law—even though doing so offers many promised blessings—that person is ready to be saved because he or she will realize how much and how often we fall short of God's law. Knowing that, then, prepares us to plead with God to save us from the penalties we deserve for breaking God's law; Christ came to pay those penalties (his "passive obedience") so that his perfect obedience to law (his "active obedience") could be credited to us by faith. Here is something to encourage us; when we were utterly powerless to obey God's law, Christ saved us from the law and its penalties through his active and passive obedience. Receive that salvation by faith never fear the law again.
Now for your thoughts: What stood out in your Bible reading for today? What questions do you have about what you read? What are your thoughts about what I wrote above? Post them in the comments below or on our Facebook page http://www.facebook.com/calvarybiblechurch/. And, feel free to answer and interact with the questions and comments of others. Have a great day; we'll talk scripture again tomorrow.

subset: commoncrawl


text:
REVELLERS at the ScotFest eighties and nineties music festival will now be able to buy a corporate box – complete with its own Tamagotchi.
The £1500 box, which will host ten festival goers at Ingliston Royal Highland Centre, Edinburgh, offers waiter service, special access to cocktail and spirit bars, higher end food and separate toilets.
VIPs who watch The Jacksons, Boyzone, B*witched, S Club, Liberty X, East 17, 5ive and Five Star on July 6 and 7 also get to choose how their own private garden will look for the two day fest.
Those who manage to keep their Tamagotchi alive the longest will also be invited to an exclusive after show party to mingle with performers.
VIDEO: Free welly-washing and other camping information announced for Edinburgh music festival ScotFest
Festival organiser Mark Bennett said: "We have had some enquiries about providing an extra special experience at Scotfest for some businesses.
"Our corporate boxes will allow people to watch the festival in style with every convenience at their disposal."
Scotfest, a real family festival complete with childminders, inflatables and family friendly overnight camping, has a capacity of 35,000 revellers a day and tickets are now available at https://scotfestuk.ticketline.co.uk/


text:
The tri-engine Falcon 50 long-range jet dependably crosses deserts and oceans nonstop. It can take off and land safely on even short runways and offers you every imaginable comfort, to satisfy your most exclusive personal wishes.
3057 NM (View Range Map)
Number of passengers
Cruising speed
431 knots
Cabin height
Cabin volume
700 ft3
Baggage capacity
115 ft3
Over 45 aircraft covering every category from Helicopter to Turbo-Prop to Ultra Long Range Jets
190+ employees, 100+ pilots, 6 offices, 500+ flights/month
IS-BAO III, Argus Gold+, Transport Audited
Over 30 years of experience in chartering, managing, and maintaining aircraft
Dedicated Client Account Manager, 24/7 In-Office & Online Account Access


text:
Do you find your mood drops as soon as the clocks go back? Do you find yourself snapping unreasonably at family members or friends, feel lethargic, low or even depressed? Do you get out of control cravings for carbs, especially chocolate, cake, bread and pasta to raise low serotonin levels?
Trust me, You are not alone. Now we know why some animals hibernate in winter to get away from it all!
Seasonal Affective Disorder (SAD) is associated with the symptoms above and may be due to a variety of causes, such as:
- hormone imbalances (particularly serotonin and melatonin)
- high stress as a result of a trauma you've experienced
- a change in diet
- medication
- physical illness.
It can be useful to explore all of these areas to find out how you can help yourself recover from SAD and prevent or manage it in future.
Let's look at some of the causes above:
1. Hormone Imbalance: serotonin and melatonin and effects of light
The relationship between serotonin and melatonin and light is still unclear. Melatonin is a hormone made from tryptophan via serotonin and is important for sleep-wake cycles. The amount released from the pineal gland is related to the amount of darkness in a 24- hour period. The longer the night, the more melatonin is released as we are naturally encouraged by this circadian rhythm to sleep when the sun goes down. Light falling on the retina of the eye reduces the amount of serotonin that is converted to melatonin which is why so many SAD sufferers benefit from using light boxes to create artificial daylight which drops the melatonin to normal.
It's the light hitting the eye that controls the messages affecting sleep, as well as appetite, sex drive, temperature, mood and activity. Therefore low light means these activities slow down. Therefore, it's clear how less light in winter disrupts our body clock.
With depression, we have lower levels of serotonin, which is why we are tempted to eat carbohydrates to cheer us up, and so the cycle continues.
However, some people need more light than others and even with correction may still experience SAD or feelings of depression. For more information about SAD, including causes and how you can access treatment and support, have a look at the MIND website here: http://www.mind.org.uk/information-support/types-of-mental-health-problems/seasonal-affective-disorder-sad/causes-of-sad/#.WCRHEeZ74q4
2. Effects of Stress
Stressful events and how we react to stress is another factor. And lack of sleep compounds the issue. The stress hormone cortisol can disrupt sleep by waking you up which makes you feel lethargic the following day, when you really need the cortisol to do its work. Keep a journal to see how stress affects you and carry out an adrenal stress test to assess levels of hormones in order to guide supplementation.
3. Diet lacking in mood boosting foods, vitamins and minerals
There are many ways that diet can cause problems with both sleep cycles and stress. The food stressors such as sugar, caffeine and alcohol in excess can disrupt hormones. Nutritional deficiencies, such as key vitamins and minerals, omega 3 fats, and protein may be the route cause of mood disorder.
4. Medications
Often if you check the side effects of any medications, you may see that mood can be affected, if that's the case speak to your doctor to see if there is a better alternative.
5. Physical illness
Many health conditions have lethargy and disrupted sleep as side effects. For example, if you have a health condition that causes chronic fatigue, accept that this takes a toll on your sleep patterns and energy levels. Take time to recover and make sure that you have self care strategies in place rather than pushing yourself through hectic events in your life.
What can we do to manage SAD?
As a starting point SAD can be managed with nutrition, exercise, counselling and mindfulness methods
Here's an Action Plan to help:
1. Firstly make some key changes to your diet:
- Eating tryptophan-containing foods is one way of potentially boosting brain serotonin levels. Choose from turkey, chicken, tuna, salmon, eggs, pumpkin seeds, sunflower seeds, kidney beans, rolled oats, lentils, chickpeas, tahini, walnuts, avocado and almond butter. However, the absorption of tryptophan is enhanced by eating carbohydrate-rich foods. Now, you don't want that carbohydrate source to be fast-releasing high GL sugars found in biscuits, cakes, pasta and bread. Rather you want it to be from wholefood sources like oats, quinoa, brown rice, vegetables and fruits, lentils, sweet potato and beans. Combine these foods at meal/snack times. You can also try supplements such as 5htp which directly converts to tryptophan or valerian which also aids sleep, however seek the advice of a qualified nutritionist to ensure safety with supplementation.
- Eat regular meals and snacks containing protein, not only for tryptophan, but also to keep blood sugar in balance. If you are skipping meals, your blood sugar will get very low and you may experience low mood, anxiety and possibly headaches. Reduce or avoid sugar where you can and replace with healthier snacks/desserts. Avoid or reduce alcohol intake, and if this is a problem for you, seek help for this.
- Drink regular water to keep hydrated and prevent lethargy.
- Ensure a daily intake of a handful of nuts and seeds, plus 3 portions of oily fish per week. People who don't like or are allergic to fish, vegetarians and vegans will need to supplement a suitable source of EPA/DHA which is required for the brain.
- Ensure a varied diet and take a multivitamin and mineral if you suspect deficiencies. Speak to a nutritionist for further help to choose the right one for you. Have an adrenal stress test and check your levels of vitamin D as this is actually a hormone, the deficiency of which is now being linked to SAD.
- Check out www.foodandmood.org website for further information.
2. Find Ways to Manage Your Stress
It's useful to work out your triggers for stress and find ways to cope, whether it's committing to a form of exercise, (walking in nature is my favourite!), dancing or yoga, taking up a mindfulness class or talking to a counsellor or therapist. Set aside 10 minutes a day for meditation. Reiki and Bach flowers are my stress relievers and I would be happy to help you, if you are interested.
Local mindfulness courses are run at Heart in Twickenham by Cheryl Edwards (firstname.lastname@example.com) and you will be able to find a wide range of talking therapies at Asana Health in Kingston (www.asanahealth.co.uk).
I hope that you are now prepared for the winter and festive season ahead and let me know if you have any questions about nutrition for SAD or the tests I carry out in my clinic. I am happy to help put you in the right direction with my free 20-minute no-obligation coaching call (contact me on email@example.com or call 07880 353964).
Healthy wishes!


text:
Birds of a feather read together.
We love our local book clubs.
We offer a 10% discount on all the books on your club's reading list. Just let us know your purchase is a book club read to receive the discount.
Come and browse our selection of local club picks and bring us your club's list to add even more variety.
Selections to knock their socks off.
Each spring we host our annual "Book Club" Staff Picks Nights, with presentations from all the Owls of our favourite discoveries of the past year, with an eye for books that promote discussion.
Attendees go home with a handout of over 50 recommendations.
Our in-House Book Clubs
We host six in-house book clubs at the Owl's Nest. Clubs run September to June and are open to new members at any time.
Junior Owlets for readers in Grades 3 to 6
Second Saturdays at 9:00AM
Junior Owlets (Homeschoolers)
Second Mondays at 10:30AM
Senior Owlets for readers in Grades 6 & Up
Second Saturdays at 2:00PM
O.W.L.S. (Our Wonderful Literary Society), a literary fiction club for adults.
First Thursdays at 7:00PM
Hootdunnit, a mystery book club for adults.
Third Wednesdays at 7:00PM
Book Club for Adults Who Love Y.A. Fiction
First Mondays at 7:00PM
Reading lists and meeting dates available in-store, or by email request. They are also listed on our webstore's events page


text:
Have you ever thought about paying a long visit to Dubai? if you haven't done so yet, it is time to think about doing it. While you are at it, it will not take too much of your time if you plan about means of transportation to use as well. Is it not too early you might ask? Well, it depends on how to perceive things for your trip. Some people have it all in the mind before landing in the city while others like to take decisions on how things keep unfolding. It all comes down to what suits you better. With all this said, one thing will surely happen – when you end up with a rent a Mercedes Dubai to fulfill your transportation needs in the city, you will likely have a great time there. What if someone told you that hiring services of rent a car will prove to be cheaper when compared to cabs and public transportation?
Amazing experience
Try calculating it and you will know that the fare you end up paying for rent a car is actually slightly cheaper than that of a cab. Wait – why would you be calculating money at all when you landed in this city to have as much fun as possible? That's how some tourists think but just because they do, doesn't mean they are right? The fact is that one should always think about saving some money and not spending it all on the trip. You will have a hard time saving money when in Dubai as this city will bring something amazing to you that you will not be able to resist. For instance, if you are a fan of boating and yachting, will you be able to resist renting one when visiting the Marina area? No, you will most probably not be able to do that regardless of how hard you try.
Have fun but try rationality
If it was not for the prices, you might have bought almost everything you had seen in Dubai so far. Even if you could lay your hands on that lovely luxury rent a car of yours, you would do it. But, touring Dubai is not just all about spending money, rather it is more about collecting memories to cherish them for life. You have Dubai car rental Lamborghini at your disposal throughout the tour or for as long as you like but the sweet memories are going to last forever and perhaps one day, you will head back to your favorite tourist destination.