(* File: PAL.thy Author: Asta Halkjær From This work is a formalization of public announcement logic with countably many agents. It includes proofs of soundness and completeness for variants of the axiom system PA + DIST! + NEC!. The completeness proofs build on the Epistemic Logic theory. *) theory PAL imports "Epistemic_Logic.Epistemic_Logic" begin section ‹Syntax›