Public Announcement Logic

Origin. Plaza introduced PAL (1989). Simplest dynamic epistemic logic. Models truthful public announcements. Announces φ: eliminate worlds where φ false. Foundation for more complex epistemic updates. Extensively studied fragment of DEL.

Models. Knowledge change from announcements. Before announcement: agents have uncertainty. Announcement of φ: all learn φ is true. After: only φ-worlds remain. Common knowledge created.

Formalism.

Syntax: φ ::= p | ¬φ | φ ∧ ψ | Kₐφ | [!φ]ψ | ⟨!φ⟩ψ

[!φ]ψ: "after announcing φ, ψ holds" ⟨!φ⟩ψ: "φ can be announced and then ψ holds"

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

Restriction: M|φ = (W', R', V') where

W' = {w ∈ W : M, w ⊨ φ}
R'ₐ = Rₐ ∩ (W' × W')
V'(p) = V(p) ∩ W'

Reduction axioms:

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

Group knowledge:

Eᴳφ: everyone in G knows φ
Cᴳφ: common knowledge in G
[!φ]Cᴳψ: common knowledge after announcement

Symbols.

Symbol	Unicode	Name	Meaning
[!φ]	—	Announcement	After public φ
⟨!φ⟩	—	Possible ann	Can announce φ
Kₐ	—	Knows	Agent a knows
Eᴳ	—	Everyone	All in G know
Cᴳ	—	Common	Common knowledge
\|	—	Restriction	Model restriction
⟨	U+27E8	Angle bracket, left	Opening of the diamond ⟨!φ⟩
⟩	U+27E9	Angle bracket, right	Closing of the diamond ⟨!φ⟩
W	—	Domain	Set of worlds; W' after restriction
Rₐ	—	Accessibility	Agent a's epistemic relation
V	—	Valuation	Atoms true at each world
⊨	U+22A8	Satisfaction	Truth at a world in a model
∩	U+2229	Intersection	Relation and valuation cut to W'
×	U+00D7	Cartesian product	W' × W' in the restricted relation
∈	U+2208	Membership	Worlds surviving the announcement
↔	U+2194	Biconditional	Form of the reduction axioms
→	U+2192	Material conditional	Truthfulness clause in the reductions
¬	U+00AC	Negation	Propositional connective
∧	U+2227	Conjunction	Propositional connective

Metatheory. Plaza (1989), and independently Gerbrandy and Groeneveld (1997), gave the reduction axioms, which drive [!φ] inward through atoms, connectives and knowledge operators until it disappears; the composition axiom [!φ][!ψ]χ ↔ [!(φ ∧ [!φ]ψ)]χ collapses any sequence of announcements into a single one. PAL is therefore expressively equivalent to multi-agent S5 and inherits its completeness and decidability, but the translation is exponential: Lutz (2006) proved the succinctness gap unavoidable and showed PAL satisfiability PSPACE-complete, the same class as S5ₙ. Model checking runs in polynomial time. With common knowledge the reduction breaks down — there is no reduction axiom for [!φ]C_Gψ, and PAL with C is strictly more expressive than S5ₙ with C — which van Benthem, van Eijck and Kooi (2006) repair by adding relativized common knowledge C(φ, ψ). Validity is not closed under uniform substitution: [!p]Kₐp is valid while [!φ]Kₐφ is not, so PAL is not a normal modal logic in the standard sense.

Applies to. Puzzle solving (muddy children). Protocol analysis. Information flow. Security (what announcements reveal). Game theory. Social epistemology.

Limitations. Announcements are truthful by construction — [!φ]ψ holds vacuously where φ is false — so lying, error and private communication all fall outside and require action models. Success fails: announcing a Moore sentence p ∧ ¬Kₐp falsifies it, so [!φ]φ is valid only for the successful formulas, a class containing every Boolean φ but with no simple syntactic characterization. This is also why validity is not substitution-closed, so a valid scheme cannot be instantiated freely. Only what the epistemic language already expresses can be announced, and the framework has no way to represent learning a fact for which it has no formula. Every announcement is public and simultaneous, which by Halpern and Moses (1990) is precisely the condition that fails in asynchronous systems and over lossy channels. Quantifying over announcements makes satisfiability undecidable (French and van Ditmarsch, 2008).