 The language \(\eqref{PAL}\) of Public Announcement Logic extends the basic modal language \eqref{ML} by adding formulas \([F!]G\) to express that “after the public announcement of F, formula G is true”: 