unicode_fol_kit.semantics.dynamic_epistemic

Public announcement logic (PAL) — dynamic epistemic model update.

Static epistemic logic (Knows over a Kripke model) describes what agents know; public announcement logic adds the dynamics: a truthful public announcement of φ removes every world where φ is false, so the agents’ knowledge changes. The announcement operator [φ!]ψ (“after announcing φ, ψ holds”) has the truth condition:

M, w ⊨ [φ!] ψ   iff   M, w ⊨ φ  implies  M|φ, w ⊨ ψ

where M|φ is announce() — M restricted to its φ-worlds (relations and valuation cut down to the survivors). The dual ⟨φ!⟩ψ (“φ is true and after announcing it ψ holds”) is φ ∧ M|φ,w ⊨ ψ. Announcements compose, so iterated updates and the Moore-sentence phenomenon (announcing p ∧ ¬K_a p makes it false) fall straight out.

Built on unicode_fol_kit.semantics.kripke.satisfies_modal(); the announced and post formulas are ordinary (propositional, epistemic, …) modal formulas.

Public API: announce(), box_announce(), diamond_announce().

Functions

announce(model, formula)	Return model updated by a truthful public announcement of formula.
box_announce(model, world, announcement, post)	Return whether model, world ⊨ [announcement!] post (PAL box).
diamond_announce(model, world, announcement, ...)	Return whether model, world ⊨ ⟨announcement!⟩ post (PAL diamond).

unicode_fol_kit.semantics.dynamic_epistemic.announce(model, formula)

Return model updated by a truthful public announcement of formula.

The result keeps exactly the worlds where formula is true (under satisfies_modal()); every relation is restricted to those survivors and the valuation (and per-world object domains, if any) likewise. Inputs are not mutated.

Parameters:

• model (KripkeModel)

• formula (Node)

Return type:

KripkeModel

unicode_fol_kit.semantics.dynamic_epistemic.box_announce(model, world, announcement, post)

Return whether model, world ⊨ [announcement!] post (PAL box).

Vacuously true when the announcement is false at world (an untruthful announcement is not made); otherwise post must hold at world in the updated model announce().

Parameters:

• model (KripkeModel)

• world (Any)

• announcement (Node)

• post (Node)

Return type:

bool

unicode_fol_kit.semantics.dynamic_epistemic.diamond_announce(model, world, announcement, post)

Return whether model, world ⊨ ⟨announcement!⟩ post (PAL diamond).

True iff the announcement is truthful at world and post then holds at world in the updated model — the dual of box_announce().

Parameters:

• model (KripkeModel)

• world (Any)

• announcement (Node)

• post (Node)

Return type:

bool