An Alternative Axiomatization of DEL and Its Applications

1 Introduction

Dynamic Epistemic Logic (DEL) and Epistemic Temporal Logic (ETL) are two major semantics-driven logical approaches for modelling knowledge and interactions in multiagent settings (cf. e.g., [Baltag et al., 1998; van Ditmarsch et al., 2007] for DEL and [Fagin et al., 1995; Parikh and Ramanujam, 1985] for ETL). In a nutshell, the DEL approach updates the epistemic structures by executing events, while the ETL approach computes the epistemic structure on the given temporal structure of the system.

It is not hard to see that iterated updates in DEL construct the temporal structure based on an initial epistemic model. Thus it is natural to cast the DEL-generated temporal epistemic structures as a particular class of ETL models, as studied in [van Benthem et al., 2009]. This point of view turned out to be very useful in solving technical questions in the field (cf. e.g., [Aucher and Herzig, 2011; Holliday et al., 2012]). Wang and Cao [2013] tried to make this view more explicit in logic, by giving a non-standard ETL-style axiomatization of Public Announcement Logic proposed in [Plaza, 1989; Gerbrandy and Groeneveld, 1997]. The new axiomatization differs from the standard reduction-axiom-based systems not only in the shape of the axioms but more importantly in the

∗The first author is supported by the NSSF grant 11CZX054 and the key project of National Social Science Foundation of China 11&ZD088. The authors would like to thank the anonymous referees for their insightful comments.

Guillaume Aucher

Department of Computer Science Universit´e de Rennes 1 - INRIA guillaume.aucher@irisa.fr

corresponding proof method for completeness. It was argued that the new axioms naturally specify the essence of the update, and can be applied to other dynamic epistemic logics where the standard reduction technique is not applicable.

In this work, we follow the proposal made in [Wang and Cao, 2013] and take the analysis to the event-model-based DEL [Baltag et al., 1998]. Importantly, we demonstrate the usefulness of our new axioms and the related proof techniques by transparently unifying many existing/new results about DEL in the same picture.

Our main contributions are summarized as follows:

• We provide a new axiomatization DEN of DEL based on a revision of the proof strategy proposed in [Wang and Cao, 2013] using no reduction axioms.
• The new axioms characterize the update product (Theorem 11), which is the DEL version of the characterization result of PAL relativization in [van Benthem, 2011, Ch 3.8].
• The corresponding properties to the new axioms characterize the DEL-generatable epistemic temporal structures given an event model U (Theorem 13 and 22). We deviate from the representation theorems in [van Benthem et al., 2009] and [van Benthem and Liu, 2004] by considering a fixed event model and allowing epistemic temporal models that are not in the tree-like shape.
• By weakening the proof system DEN, we provide a complete axiomatization of DEL on epistemic models with state-dependent protocols (Theorem 21). Our logic turns out to be equivalent to the TDEL on tree-like generatable epistemic temporal structures discussed in [Hoshi and Yap, 2009], which is a well-known example of a dynamic epistemic-style logic which cannot be reduced to epistemic logic.

The readers are suggested to go through Section 2 even when they are familiar with DEL, since some crucial assumptions and observations are explained there about our exposition of DEL. In Section 3 and 4 we give the new axiomatization and related main results respectively.

2 Preliminaries

Given a non-empty set P of basic proposition letters, and a non-empty set Σ of basic events, the dynamic epistemic language LDEL is defined as follows:

where p ∈ P and e ∈ Σ. We call the [e]-free part of LDEL the epistemic language (LEL). As usual, we define ⊥, φ∨ψ, φ → ψ, ✸φ, and 〈e〉φ as the abbreviations of ¬⊤, ¬(¬φ ∧ ¬ψ), ¬φ ∨ ψ, ¬✷¬φ, and ¬[e]¬φ respectively.

For simplicity, we only consider the single agent case in this paper, although all of our results and techniques apply to the multi-agent case as well.

The language LDEL is usually interpreted on epistemic models 1 which are triples in the form of (S,→, V ) where

• S is a non-empty set of possible worlds,
• → ⊆ S × S is a binary relation over S,
• V : P→ 2S is a valuation function assigning each basic proposition letter a set of worlds where it is true.

In the sequel, given a model M, we use SM,→M and VM to denote the corresponding components of M. We use M to denote the class of all the epistemic models.

To interpret the [e] operators, the event models are introduced as below:

Definition 1 (Event Model). Given Σ, an event model U is a tuple (Σ,↣, Pre) where:

• Σ is a non-empty (countable) set of events.
• ↣ ⊆ Σ × Σ is a binary relation on Σ.
• Pre : Σ → LEL is a function assigning each event a precondition (an LEL formula).

A pointed event model U, e is an event model with a designated point e in Σ. We call U an image-finite event model if {f | e ↣f} is finite for each e. ✁

Important: In this paper, we assume that there is a single fixed event model U which is image-finite but can be infinite. 2 The readers who are familiar with DEL may find this assumption and our exposition of DEL slightly different from the usual ones. We will come back to this in Remark 1.

Given an epistemic model M = (S, →, V ), the truth value of DEL formulas at a state s inM is defined as follows:

where the updated model is defined as follows:

Definition 2 (Update Product ⊗). Given an epistemic model M = (S,→, V ) and an event model U = (Σ,↣, Pre), the product model is an epistemic model (M⊗ U) = (S′ ,→′ , V ′ ) where:

1 In this paper, we do not restrict ourselves to S5 models unless specified. We call the models epistemic due to the origin of DEL and its usual applications.

2 Aucher and Herzig [2011] also fix an event model in their discussion, but explores the use of converse modality in the language.

Important: A semantics-driven logic can be represented as a triple 〈language, class of models, satisfaction relation〉, thus the standard DEL can be viewed as 〈LDEL,M, ⊨〉 while EL is 〈LEL,M, ⊨〉. This view is important since in the later part of the paper we will introduce many other semantics of the language LDEL on other classes of structures. We write M ⊨ φ if φ is valid in all the models in M.

Remark 1. It is the time to explain our deviations from the standard exposition of DEL:

[e] vs. [U, e]. Although [U, e] is taken as an innocent operator in most of the DEL literature, a technically satisfactory treatment has to be quite complicated as demonstrated by [Baltag and Moss, 2004], due to the mixture of syntax and semantics introduced by [U, e] operators. 3 Here we make a simple separation of the syntax from the semantics by using atomic events w.r.t. a fixed event model. Note that we allow the event model to be infinite (but image-finite for the later axiomatization) thus this single event model can also be seen as a disjoint union of many finite event models in the standard setting. This simpler language is easier to handle when many alternative semantics are introduced later on.

LEL vs. LDEL in preconditions: Instead of arbitrary LDEL formulas, we only allow LEL formulas as preconditions. It is not an essential restriction, for DEL is equally expressive as epistemic logic (due to Theorem 1 below). On the other hand, this change can simplify the proofs considerably, though our results also hold in the standard setting.

The following axiomatization is based on the expositions in [Baltag and Moss, 2004; van Ditmarsch et al., 2007]: 4

where φ, ψ, χ denote arbitrary formulas, p ∈ P, and e, f ∈ Σ. RE is the rule of replacement of equivalents. We call UATOM, UNEG UCON, UK the reduction axioms. We use EL to denote the system DE without the reduction axioms.

The following result is well-known:

3 The readers may not agree with this claim at the first glance, but they may face troubles when spelling out all the details, e.g., arguing the proof system is recursively enumerable.

4 In DE, we use RE instead of the composition axiom schema in [van Ditmarsch et al., 2007]. Note that the latter schema requires that a certain composition of two event models is again a well-formed event model, while it may not be possible in LDEL where the event model is fixed. In this light, we think DE is more robust than the axiomatization using composition axiom schema since DE works even when the space of event models is not composition closed.

Theorem 1 ([Plaza, 1989]). DEL is equally expressive as EL and there is a translation t which can turn a LDEL formula into an equivalent LEL formula w.r.t. ⊨.

The standard reduction technique to show the completeness of DE can be summarized as follows:

The second step is due to the completeness of EL and the last step requires ⊢DE φ ↔ t(φ). There are different ways to make the proof system meet the requirement. In our setting the last step relies on RE and works in an inside-out fashion (cf. [Wang and Cao, 2013] for a detailed discussion). Based on this proof strategy we can prove the completeness of DE (cf. e.g. [van Ditmarsch et al., 2007]):

Theorem 2. DE is sound and complete for 〈LDEL,M, ⊨〉.

3 Axiomatization DEN

We propose the following alternative axiomatization DEN:

Intuitively, DISTU and NECU are analogues of DISTK and NECK. INV expresses the stability of the valuation. PRE specifies the precondition of an event. NM and PR are variations of the axiom schemata of no learning and perfect recall in ETL (cf. e.g., [Halpern et al., 2004] for discussion).

In their system PAN for PAL, Wang and Cao [2013] used an axiom schema PFUNC (partial functionality), which can be translated into the following axiom schema in our setting: 〈e〉φ ↔ (Pre(e) ∧ [e]φ). It is easy to see that this axiom schema is essentially a reformulation of the reduction axiom for negation (UNEG). To make a neat system, instead of PFUNC or UNEG, we have a much weaker axiom schema PRE which is also present in [Aucher and Herzig, 2011]. To derive UNEG based on PRE, we need the functionality axiom schema 〈e〉φ → [e]φ whose instances are indeed derivable in DEN but in a highly non-trivial way. 6

5 We can rewrite NM into ✸〈f〉φ → ∧e:e↣f [e]✸φ if for each f, {e | e ↣ f} is finite.

6 By a simultaneous induction on the structure of φ we can prove the following two claims at the same time: (1) ⊢DEN 〈e〉φ → [e]φ and (2) [e]φ is DEN-provably equivalent to an LEL formula. The case of φ = ¬ψ for (2) needs the induction hypothesis of (1), and

The soundness of DEN is straightforward. Note that although all the other reduction axioms are derivable in DEN without much effort, 7 it is quite involved to derive UNEG in DEN as we mentioned in footnote 6. Thus we cannot conclude the completeness of DEN immediately based on the completeness of DE. In this paper, we follow the general ideas in [Wang and Cao, 2013] to prove the completeness of DEN directly, without referring to DE nor EL. We revise the proof strategy of [Wang and Cao, 2013] as follows to make it closer to the standard reduction approach:

1. Define an auxiliary semantics ⊩ of LDEL on epistemic temporal models with e-transitions. 8
2. Find a class C of epistemic temporal models such that for any LDEL formula φ : M ⊨ φ =⇒ C ⊩ φ.
3. Show that DEN completely axiomatizes the valid LDEL formulas on C w.r.t. ⊩.

In sum, we proceed as follows (from left to right):

Compared to the standard reduction technique, here we keep the formulas intact but change the semantics, and reduce the original completeness to the completeness w.r.t. the new semantics on a class of temporal epistemic models. The new completeness question is much easier to solve using standard techniques in modal logic.

Let us start with the new semantics.

Definition 3 (Extended model). Given an event model U, an U-extended model N is a tuple:

where:

• (S,→, V ) is an epistemic model,
• For each e ∈ Σ, e→ is a (possibly empty) binary relation over S.

Important notation: We call (S,→, { e→| e ∈ Σ}) the extended frame of N, and (S,→, V ) the epistemic core of N (notation N -). As usual, we say that N is image-finite if for each s in N, s has finitely many → successors and finitely many e-successors for each e ∈ Σ. For a sequence of events h = e0 . . . ek we write t h→ t′ for t e0→ . . . ek→ t′ . ✁

Since we fix a U, we will just call the above models extended models. Note that extended models can be viewed as temporal epistemic models with the extra information of U. The components of U will be used later when defining the special class C.

We now define an auxiliary semantics ⊩ for the language LDEL on extended models (we omit the clauses which are the same as for ⊨):

the case of φ = [e]ψ for (1) requires the IH of (2) and RE which is an admissible rule in DEN (cf. [Wang and Cao, 2013] for discussion of RE in PAL). We omit the details due to space limitation.

7 UCON is derivable from NECU and DISTU, UATOM is derivable from PRE, INV, and UK is drivable from PRE, PR, and NM.

8 Note that, as in [Aucher and Herzig, 2011], the epistemic temporal models here are not necessarily tree-like structures as in [van Benthem et al., 2009].

By definition, the two semantics coincide on LEL formulas:

Proposition 3. For any LEL formula φ and any pointed extended model M, s: M, s ⊩ φ ⇐⇒ M-, s ⊨ φ.

However, ⊨ and ⊩ differ on extended models for formulas involving [e], unless restricted to special classes of models. 9

Definition 4 (Normal extended model). An extended model

is normal if the following properties hold for any s, t in N: 10 . Pre s has e-successors iff N, s ⊩ Pre(e).

Inv if s e→ t then for all p ∈ P : t ∈ V (p) ⇐⇒ s ∈ V (p).

Nm (no miracles) if s → s′ and s′ f→ t′ then for all e and t such that s e→ t and e ↣f, we have t → t′ .

Pr (perfect recall) if s e→ t and t → t′ then there exists an s′ such that s → s′ and s′ f→ t′ for some f such that e ↣f in U.

Note that Pre, Nm and Pr all refer to components of U. The last two properties are best illustrated by the following diagrams of commutativity:

Before going further we need notions of bisimulation over epistemic models and extended models.

Definition 5 (Bisimulation). A binary relation Z is called a bisimulation between two pointed epistemic models M, s and N, t, if sZt and whenever wZv the following hold:

Invariance for all p ∈ P, w ∈ VM(p) iff v ∈ VN(p),

Zig if w → w′ for some w′ in M then there is a v′ ∈ SN with v → v′ and w′Zv′ ,

Zag if v → v′ for some v′ in N then there is a w′ ∈ SM with w →w′ and w′Zv′ .

A binary relation Z is called a Σ-bisimulation between two pointed extended models M, s and N , t, if sZt and whenever wZv the following hold besides Invariance, Zig and Zag:

• Σ-Zig if w e→w′ for some w′ inMthen there is a v′ ∈ SN with v e→ v′ and w′Zv′ ,
• Σ-Zag if v e→ v′ for some v′ in N then there is a w′ ∈ SM with w e→w′ and w′Zv′ .

9 More precisely, we say ⊩ and ⊨ coincide on an extended model N if for any φ ∈ LDEL, any s in N, N, s ⊩ φ ⇐⇒ N -, s ⊨ φ.

10 In [Aucher and Herzig, 2011], properties involving 'backward looking' were discussed on EDL models which are similar to our extended models.

We say M, s and N, t are bisimilar (resp. Σ-bisimilar) if there is a bisimulation (resp. Σ-bisimulation) between them. We use ↔ (resp. ↔Σ) for the bisimilarity relation (resp. Σbisimilarity). ✁

It is well-known that the LDEL formulas are preserved under bisimulation over epistemic models w.r.t. ⊨ (cf. e.g., [van Ditmarsch et al., 2007]), and LDEL formulas are preserved under Σ-bisimulation over extended models w.r.t. ⊩ (cf. e.g., [Blackburn et al., 2002]).

Here comes the crucial lemma saying that in a normal extended model, product updating with (U, e) has the same effect as moving along the e-transitions.

Lemma 4. If w e→ v in a normal extended modelM, then

Proof. Let Z be the binary relation between M- ⊗U and M- such that (s, f)Zt iff s f→ t inMfor some f in U.

Clearly, Z is non-empty since w e→ v inM. Now suppose sZt (thus s f→ t in M for some f), we need to check the three conditions of bisimulation.

The invariance condition is immediate due to the definition of ⊗ and Inv. For Zig, suppose (s, f) → (s′ , f ′ ) in M- ⊗U, then it is clear that s → s′ in M-, f ↣ f ′ in U, and M-, s′ ⊨ Pre(f ′ ). According to Proposition 3 and the fact that the preconditions are LEL formulas, M, s′ ⊩ Pre(f ′ ). Thus from Pre, there is a t′ such that s′ f ′→ t′ namely (s′ , f ′ )Zt′ . Now s f→ t, s → s′ , s′ f ′→ t′ and f ↣f ′ , thus from Nm we have t → t′ in M and thus in M-. Finally for Zag, suppose t → t′ for some t′ inM-. FromPr, there is an s′ inMsuch that s → s′ and s′ f ′→ t′ for some f ′ such that f ↣ f ′ . By Pre, M, s′ ⊩ Pre(f ′ ). According to Proposition 3 again, M-, s′ ⊨ Pre(f ′ ) thus (s, f) → (s′ , f ′ ) exists inM- ⊗U and (s′ , f ′ )Zt′ .

Now we are ready to prove that the two semantics do coincide on normal extended models. Almost all of our main results rely on this crucial theorem and its variations.

Theorem 5. For any LDEL formula φ and any pointed normal extended model M, s:

Proof. We prove it by induction on the structure of the formulas. The cases for Boolean combinations and ✷φ are trivial due to Proposition 3 and the induction hypothesis. For the case of [e]φ, we distinguish two cases depending on the truth value of Pre(e). Suppose M, s ⊮ Pre(e) then by the induction hypothesis (IH) M-, s ⊭ Pre(e) thus M-, s ⊨ [e]φ. Since M is normal and M, s ⊮ Pre(e), by Pre there is no outgoing e-transition from s in M, therefore M, s ⊩ [e]φ. Now we consider the case when M, s ⊩ Pre(e). By Pre, there must be at least one e-successor of s in M. Now take an arbitrary e-successor of s, call it t. From IH and Lemma 4, M- ⊗U, (s, e) ↔ M-, t. Since LDEL formulas are invariant under bisimulation w.r.t. ⊨, for any LDEL formula φ: M- ⊗ U, (s, e) ⊨ φ ⇐⇒ M-, t ⊨ φ. From IH, M- ⊗ U, (s, e) ⊨ φ ⇐⇒ M, t ⊩ φ. According to the fact that the selection of t is arbitrary, it is clear that: M, s ⊩ [e]φ ⇐⇒ M-, s ⊨ [e]φ.

Let Cn be the class of normal extended models. The following corollary is immediate based on Theorem 5.

Now we only need to show that DEN completely axiomatize the valid LDEL formulas on Cn w.r.t. ⊩.

Theorem 6. For any φ ∈ LDEL: Cn ⊩ φ ⇐⇒ ⊢DEN φ. Namely, DEN is sound and complete for 〈LDEL, Cn, ⊩〉.

Proof. We only sketch the proof since it is rather routine. The soundness is straightforward. For the completeness, first note that the proof system induces a normal modal logic 11 , due to DISTK, DISTU, NECK, and NECU. The proof starts by building the canonical extended model with both → and e→ transitions in the usual way for normal modal logics with ✷ and [e] modalities. The truth lemma is immediate, and we just need to show the canonical extended model is indeed in Cn. Note that PR and NM are Sahlqvist formulas if we replace the proposition variable φ by p, and Pr and Nm are exactly the frame properties that PR and NM defined. Then by the Sahlqvist completeness theorem, the canonical extended model has Pr and Nm (cf. e.g., [Blackburn et al., 2002]). On the other hand it is also easy to show that INV and PRE make sure the canonical model has Inv and Pre respectively.

From Corollary 1 and Theorem 6 it follows:

Theorem 7. DEN is complete for 〈LDEL,M, ⊨〉.

Similarly we can show:

Theorem 8. DEN+T, DEN+T+4 and DEN+T+4+5 are sound and complete w.r.t. the standard semantics of LDEL on the class of all T, S4, S5 frames.

4 Applications

Recall that M is the class of all the epistemic models.

Definition 6. Given an event model U, a model transformer ⊛ w.r.t. U is a function: M → M such that S⊛(M) ⊆ SM × Σ. Following the convention, we write M⊛ U for ⊛(M) and writeM⊛U i forM⊛U . . . ⊛U ︸ ︷︷ ︸ i , with M⊛ U 0 = M.

A model transformer ⊛ is a (partial) tensor product if for all (s, e), (t, f ) ∈ SM⊛U :

• (s, e) →M⊛U (t, f) iff s → t inMand e ↣f in U.

As before, we fix U thus when we mention a model transformer we mean a model transformer w.r.t. U.

Following [van Benthem et al., 2009], we define LDELprotocols:

Definition 7. Let Σ∗ be the set of finite (possibly empty) sequences of the events in Σ. A (state-dependent) protocol w.r.t. M is a function ρ : SM → 2Σ∗ such that for any s ∈ SM : ρ(s) ⊆ Σ∗ is closed under prefixes. Thus the empty string ϵ is in ρ(s) for any protocol ρ. We use ρu to denote the universal protocol, i.e., for all s ∈ SM : ρu(s) = Σ∗ .

11 Except that DEN is not closed under uniform substitution (US): the application of US to INV does not preserve validity.

Now we generalize the DEL-forest defined in [van Benthem et al., 2009] to arbitrary model transformer ⊛:

Definition 8 (⊛-forest). Given an epistemic model M and a protocol ρ, let

be the extended model generated by executing ρ where:

• S = {(s, e1, . . . , ek) | 0 ≤ k and (s, e1, . . . , ek) exists inM⊛U k and e1 . . . ek ∈ ρ(s)}.
• (s, e1, . . . , ek) → (t, e′1 , . . . , e′j ) iff k = j, and (s, e1, . . . , ek) → (t, e′1 , . . . , e′k ) inM⊛U k .
• (s, e1, . . . , ek) e→ (t, e′1 , . . . , e′j ) iff s = t and e′1 . . . e′j = e1 . . . eke
• V ((s, e1, . . . , ek)) = VM⊛U k(s, e1, . . . , ek)

Important notation: We often omit the universal protocol and write F ⊛(M) for F ⊛(M, ρu). ✁

Intuitively, F ⊛(M, ρ) is a (synchronous) update universe consisting of the updated models in the form of M⊛ U k linked by update transitions e→under the constraint of ρ.

In the sequel, we write M, s ≡LDEL N , t if M, s and N , t satisfy the same set of LDEL formulas. 12

Clearly, the update product ⊗ is a model transformer. It is not hard to show the following by the definition of ⊗:

Proposition 9. For any pointed epistemic model M, s, F ⊗(M) is normal and M, s ≡LDEL F ⊗(M), s.

Proof. The normality is straightforward based on the definition of F ⊗(M). Since M, s is actually the "ground floor" of (F ⊗(M))-, which is isolated from the other part of (F ⊗(M))-, we have M, s ≡LDEL (F ⊗(M))-, s. Since F ⊗(M) is normal, due to Theorem 5 we have (F ⊗(M))- ≡LDEL F ⊗(M), s. Thus M, s ≡LDEL F ⊗(M), s.

From the above proposition, for each pointed epistemic model M, s we have an LDEL-equivalent normal extended model F ⊗(M). Corollary 1 can then be strengthened:

Proposition 10. For any φ ∈ LDEL: M ⊨ φ ⇐⇒ Cn ⊩ φ.

4.1 Characterization theorems under universal protocol

Let M⊛ be the class of all the F ⊛(M) based on some M ∈ M under the universal protocol. We say M⊛ frame-validates an axiom schema φ if all the frames underlying the models in M⊛ validates all the instances of φ w.r.t. ⊩. We say M⊛ model-validates an axiom φ if all the models in M⊛ validate all the instances of φ w.r.t. ⊩.

Theorem 11. (1) M⊛ frame-validates NM and PR iff ⊛ is a tensor product. (2) M⊛ frame-validates NM and PR, and model-validates INV and PRE iff ⊛ is the update product.

12 Note that M, s and N, t may be of different types, e.g. one extended model and one epistemic model. In such cases we evaluate LDEL formulas according to ⊩ and ⊨ respectively.

Proof. (Sketch) We only prove (1): It is a standard exercise in modal logic to verify that any extended frame validating NM (resp. PR) w.r.t. ⊩ iff it has the Nm (resp. Pr) property. Now, to complete the proof, we break the requirement of a tensor product into two parts:

I: (s, e) →M⊛U (t, f) implies s → t inMand e ↣ f in U. II: If (s, e) and (t, f) exist inM⊛U, s → t inM, and e ↣ f in U, then (s, e) →M⊛U (t, f).

We just need to show Pr corresponds to (I) and Nm corresponds to (II) which is quite straightforward.

In the following, we prove the characterization results of extended models which are generatable by DEL updates.

Definition 9 (Generatable model modulo Σ-bisimulation). Given a model transformer ⊛, a pointed extended model N , t is ⊛-generatable if there is a pointed epistemic model M, s such that N, t ↔Σ F ⊛(M), s. A pointed extended model N, t is ⊛-prot-generatable if there is an epistemic model M, s and a protocol ρ such that N , t ↔Σ F ⊛(M, ρ), s.

Given a pointed extended model N, t, its Σ-bisimulation contraction (notation N tC ) is the |t|-generated submodel of the Σ-bisimulation contraction of N, where |t| is the equivalence class of t w.r.t. ↔Σ. We can show:

Proposition 12. For any pointed extended model N, t: N, t is Σ-bisimilar to a pointed normal model iff N tC is normal.

Proof. ⇐ is trivial, we only show =⇒ : Suppose N, t ↔Σ N ′ , t′ andN ′ is normal. ClearlyN tC , |t| ↔Σ N ′ , t′ . Inv and Pre can be verified easily. ForPr: suppose |w| e→ |u| → |v|, then since N tC , |t| ↔Σ N ′ , t′ and the fact that all the non-|t| nodes are connected with |t|, there are w′ , u′ and v′ in N ′ such that w′ e→ u′ → v′ and N tC , |w| ↔Σ,w′ , N tC , |u| ↔Σ , u′ and N tC , |v| ↔Σ, v′ . Since N ′ is normal there is a r′ in N ′ such that w′ → r′ f→ v′ for some f with e ↣ f in U. Since N tC , |w| ↔Σ,w′ then there is a |r| in N tC such that |w| → |r| and N tC , |r| ↔Σ N ′ , r′ . Since r′ f→ v′ , there is an |o| in N tC such that |r′ | f→ |o| and N tC , |o| ↔Σ N ′ , v′ . Since N tC , |v| ↔Σ, v′ , we have N tC , |v| ↔Σ N tC , |o|. Now since N tC is Σ-bisimulation contracted |o| = |v|. Therefore there is a |r| in N tC such that |w| → |r| f→ |v|. Nm can be proved similarly using the properties of the contraction.

Theorem 13. For any image-finite pointed extended model N, t: N, t is ⊗-generatable iff N tC is normal.

Proof. Suppose N, t is ⊗-generatable, then N, t ↔ F ⊗(M), s for some model M, s. From Proposition 9, F ⊗(M) is normal. Now from Proposition 12, N tC is normal.

For the other direction, suppose the N tC is normal. We first show the following:

The first equivalence is due to the bisimilarity between N, t and N tC and the fact that LDEL is preserved under Σbisimulation w.r.t. ⊩ (cf. e.g., [Blackburn et al., 2002]). The second equivalence is due to the normality of N tC and Theorem 5. The third equivalence is due to Proposition 9.

Now let N ′ = (N tC )-. Since N, t and U are image-finite, it is not hard to show by induction on the length of the sequence h that for each (h, e) in F ⊗(N ′ ) there are only finitely many (h′ , e′ ) such that (h, e) → (h′ , f). Moreover, each s in F ⊗(N ′ ) has at most one f-successor for each f ∈ Σ. Therefore F ⊗(N ′ ) is also image-finite. Now by the well-known Hennessy-Milner theorem (cf. e.g., [Blackburn et al., 2002]), N, t ↔Σ F ⊗(N ′ ), |t|.

Compared to the representation results in [van Benthem et al., 2009] and [van Benthem and Liu, 2004], there are two major differences in our setting: 1. Our notion of generatable extended models is modulo Σ-bisimulation, thus allowing models which are not in the tree-like shape; 2. More importantly, we fix an event model U and consider the generatable models w.r.t. U. 13 In particular, Nm and Pr also refer to the structure of U. Due to such differences, our result is not a special case of Theorem 2 in [van Benthem et al., 2009].

4.2 DEL with protocols

In [Hoshi and Yap, 2009], the authors discussed the axiomatization of LDEL on generatable history-based epistemic temporal models, i.e., 〈LDEL,M⊗prot ,⊩〉 where M⊗prot is the class of all the F ⊗(M, ρ). This looks more like an epistemic temporal logic rather than a dynamic epistemic logic. In this paper, inspired by [van Ditmarsch et al., 2011], we give a new 'dynamic' semantics of LDEL directly on epistemic models with protocols (M, ρ), by using the transformer ⊙ defined below (the clauses that coincide with the standard semantics ⊨ are omitted):

where M, ρ ⊙ U = (S′ , →′ , V ′ , ρ′ ) with:

Note that the protocol ρ constrains the domain of the updated model. Moreover, after executing an event e, the current protocol has to be updated (the reader can verify that ρ′ is indeed a well-defined protocol). Let PM be the class of all the epistemic models with protocols then the above logic can be denoted as 〈LDEL, PM, ⊪〉.

A moment of reflection should confirm the following observation where (M, ρ) at the right-hand-side below is taken as a single model: 14

We also need a revised notion of bisimulation between epistemic models with protocols:

Definition 10 (Prot-bisimulation). A binary relation Z is called a prot-bisimulation between two pointed epistemic models with protocols M, ρ, s and N , γ, t, if sZt and whenever wZv the following holds besides Invariance, Zig, Zag: Prot-invariance ρ(w) = γ(v).

13 [van Benthem and Liu, 2004] shows a result in the shape of: an epistemic temporal model is generatable by some event model iff it satisfies certain properties. Here we replace some by a fixed U.

14 Here we also need to relax the definition of model transformer to allow epistemic models with protocols.

We use ↔prot to denote the prot-bisimilarity.

✁

It is rather routine to show that prot-bisimulation preserves truth of LDEL formulas under ⊪:

Proposition 15. IfM, ρ, s ↔prot N, γ, t then for all LDEL formula φ : M, ρ, s ≡LDEL N , γ, t.

Important notation: Given an extended model N and a state t in it, let path(t) be {h | t h→ t′ for some t′}. The characteristic protocol of N (notation ρN) is a protocol for N - such that ρN (s) = path(s) for each s ∈ SN = SN -.

Definition 11. An extended model is semi-normal if it satisfies Inv, Nm, Pr and the following two for all the e, s:

PPre s has e-successors implies M, s ⊩ Pre(e);

Det if s has two e-successors t, t′ then path(t) = path(t′ ).

PPre is clearly weaker than Pre due to the protocol constraints. Det says the protocol is not really branching. To capture these two properties, we propose the following two axiom schemata (where e ∈ Σ and h ∈ Σ∗ ):

Let PDEN be DEN -PRE+PPRE+DET and Csn be the class of all the semi-normal extended models. Note that DET is a special case of 〈e〉φ → [e]φ, and PPRE is clearly weaker than PRE, thus it can be shown that PDEN is strictly weaker than DEN(similarly, semi-normality is weaker than normality). We will show that PDEN completely axiomatizes LDEL on models in PM. Again we follow the completeness proof strategy as before:

It is not hard to show that:

Theorem 16. For any φ ∈ LDEL:Csn ⊩ φ ⇐⇒ ⊢PDEN φ. To complete the proof we only need to show PM ⊪ φ =⇒ Csn ⊩ φ. Following the same strategy, we need the analogue of Lemma 4:

Lemma 17. For any semi-normal extendedmodelM, if w e→ v inM, we have :

Proof. (Sketch) Most of the proof is identical to the proof to Lemma 4. There are two changes: 1. We need to verify the extra Prot-invariance; 2. We cannot use Pre but only PPre. Prot-invariance can be guaranteed by Det and we do not need the full Pre under the presence of the protocol information. We omit the detailed proof due to the space limit.

Based on the above lemma, we can prove analogues of Theorem 5 and Proposition 9 by almost identical proofs:

Theorem18. For any LDEL formula φ and any semi-normal extended model M:

Proposition 19. For any epistemic model M and any protocol ρ: F ⊗(M, ρ) is semi-normal and thus F ⊗(M, ρ), s ≡LDEL M, ρ, s.

We can then prove the following proposition, which is the (strengthened) last piece for the completeness proof.

Proposition 20. For any φ ∈ LDEL: PM ⊪ φ ⇐⇒ Csn ⊩ φ ⇐⇒ M⊗prot ⊩ φ.

Theorem 21. PDEN is sound and complete for 〈LDEL, PM ⊪〉 and 〈LDEL, M⊗prot ⊩〉.

This result also shows that our logic 〈LDEL, PM ⊪〉 is essentially the same as the logic proposed in [Hoshi and Yap, 2009] which can be viewed as 〈LDEL,M⊗prot ⊩〉.

Using Propositions 19 and 18 we can show for any pointed extended model N , t:

N, t ≡LDEL N tC , |t| ≡LDEL N ′ , γ, |t| ≡LDEL F ⊗(N ′ , γ), |t| where γ = ρN tC and N ′ = (N tC )-. Based on this, an analogue of Theorem 13 follows due to an almost identical proof:

Theorem 22. An image-finite pointed extended model N, t is ⊗-prot-generatable iff N tC is semi-normal.

5 Conclusion

Let us sum up the results once again for clarity since we have been talking many different semantics:

• DEN completely axiomatizes 〈LDEL,Cn, ⊩〉 and 〈LDEL,M, ⊨〉 (Theorems 6 and 7 respectively).
• PDEN completely axiomatizes 〈LDEL,Csn, ⊩〉, 〈LDEL, PM, ⊪〉, and 〈LDEL, M⊗prot , ⊩〉 (Theorems 16 and 21).
• PRE, INV, NM, and PR characterize update product while the first two axioms characterize (partial) tensor product (Theorem 11).
• Pre, Inv, Nm and Pr characterize the ⊗-generatable extended models under universal protocols (Theorem 13), while PPre, Det, Inv, Nm and Pr characterizes the ⊗-generatable extended models under arbitrary protocols (Theorem 22).

In our view, the essential proof strategy for the completeness of a DEL-like logic (w.r.t. some proof system), is to reduce the completeness of the original logic to the completeness of epistemic temporal logic on certain class of epistemic temporal models. The latter problem is usually much easier to prove, compared to the original one. Therefore the most crucial step is to make the transition from the validity w.r.t. dynamic epistemic semantics to the validity w.r.t. epistemic temporal semantics on certain class of models (cf. Propositions 10 and 20). To do so, we can 'flatten' the dynamics in certain epistemic temporal structures (cf. Lemmata 4 and 17).

We believe that our method can be applied to other dynamic epistemic logics. In particular, the discussion on DEL with protocols shows the possibility to handle logics which cannot be reduced to epistemic logic. The same discussion also demonstrates that we can dynamify the logic satisfying certain epistemic temporal properties (cf. Theorem 21). For future work, we would like to look at the dynamic epistemic logics with iteration operators (e.g., common knowledge and Kleene star of the updates).