Dynamic Epistemic Logic

Origin. Plaza introduced public announcement logic (1989). Baltag, Moss, and Solecki generalized to action models (1998). Van Benthem unified dynamic and epistemic traditions. Combines epistemic logic with dynamic updates. Models how knowledge changes through communication and observation.

Models. Knowledge change through action. Epistemic logic: what agents know. Dynamic epistemic logic: how knowledge changes when events occur. Public announcements eliminate worlds where announcement is false. Private communication, lies, and observation all modeled as epistemic actions.

Formalism.

Public Announcement Logic (PAL): [!φ]ψ — "after truthfully announcing φ, ψ holds"

Semantics: M, w ⊨ [!φ]ψ iff M, w ⊨ φ implies M|φ, w ⊨ ψ where M|φ restricts to φ-worlds.

Reduction axioms:

[!φ]p ↔ (φ → p)
[!φ]¬ψ ↔ (φ → ¬[!φ]ψ)
[!φ](ψ ∧ χ) ↔ ([!φ]ψ ∧ [!φ]χ)
[!φ]Kₐψ ↔ (φ → Kₐ[!φ]ψ)

Action models: A = (E, ~ₐ, pre) where:

E: set of events
~ₐ: indistinguishability for agent a
pre: E → L (preconditions)

Product update M ⊗ A combines model and action.

Examples:

Muddy children: public announcements lead to knowledge
Card games: private communication
Cryptographic protocols: who learns what

Common knowledge update: C_G φ (common knowledge in group G) can be achieved or broken by announcements.

Symbols.

Symbol	Unicode	Name	Meaning
[!φ]	—	Announcement	After announcing φ
Kₐ	—	Knows	Agent a knows
Bₐ	—	Believes	Agent a believes
C_G	—	Common knowledge	Group G commonly knows
⊗	U+2297	Product	Model update
~ₐ	—	Indistinguishable	Agent can't distinguish
E	—	Events	Action events
pre	—	Precondition	Formula an event requires to occur
M\|φ	—	Restriction	Model cut down to the φ-worlds
⊨	U+22A8	Satisfaction	Truth at a world in a model
↔	U+2194	Biconditional	Form of the reduction axioms
→	U+2192	Material conditional	Truthfulness clause in the reductions
∧	U+2227	Conjunction	Distribution of announcement over conjuncts

Metatheory. Plaza's reduction axioms push [!φ] inward until it disappears, so PAL and multi-agent S5 are expressively equivalent; Lutz (2006) showed the translation causes an unavoidable exponential blow-up in formula size and that PAL satisfiability is nonetheless PSPACE-complete, the same as S5ₙ. The same reduction covers action models without common knowledge, so that fragment is again equivalent to S5ₙ. With common knowledge the reduction fails and the dynamic language is strictly more expressive; van Benthem, van Eijck and Kooi (2006) restore a reduction by adding relativized common knowledge, and their language also admits postconditions for factual change. Model checking separates the two systems: polynomial time for public announcement, PSPACE-complete for action-model DEL (Aucher and Schwarzentruber, 2013). Uniform substitution fails — [!p]Kp is valid but [!φ]Kφ is not — and product update is invariant under bisimulation, so updates are well defined on bisimulation classes rather than on representations.

Applies to. Security protocol verification. Game theory (information revelation). Social epistemology. Puzzle analysis (muddy children, wise men). Multi-agent systems. Lying and deception modeling. Gossip protocols.

Limitations. Perfect recall and logical omniscience are built into the semantics: product update never merges worlds an agent had already distinguished, and the S5 base closes knowledge under implication. In PAL announcements are veridical by stipulation, and success still fails — [!φ]Kφ is invalid, because announcing a Moore sentence p ∧ ¬Kp falsifies it — so the set of validities is not closed under uniform substitution. Every event needs a precondition already expressible in the object language, and action models are finite, so unbounded or continuous protocols fall outside the framework. The original BMS system has no postconditions, so events change what is known but never what is the case. Quantifying over announcements makes satisfiability undecidable (French and van Ditmarsch, 2008), and multi-agent epistemic planning with action models is undecidable (Bolander and Andersen, 2011).