# Public announcement logic - inclusion of the necessitation rule

In the book Dynamic Epistemic Logic by Ditmarsch et. al. a system for simple public announcement logic in the context of epistemic logic is proposed as:

Axioms:

all instances of propositional tautologies

$K_a(\phi\to\psi)\to(K_a\phi\to K_a\psi)$

$K_a\phi\to\phi$

$K_a\phi\to K_aK_a\phi$

$\neg K_a\phi\to K_a\neg K_a\phi$

$[\phi]p\leftrightarrow(\phi\to p)$

$[\phi]\neg\psi\leftrightarrow (\phi\to\neg[\phi]\psi)$

$[\phi](\psi\land\chi)\leftrightarrow([\phi]\psi\land[\phi]\chi)$

$[\phi]K_a\psi\leftrightarrow(\phi\to K_a[\phi]\psi)$

$[\phi][\psi]\chi\leftrightarrow[\phi\land[\phi]\psi]\chi$

Rules:

$From\;\phi\;and\;\phi\to\psi\;infer\psi$

$From\;\phi\;infer\;K_a\phi$

How does it come that in the context of a new modal operator, namely $[\phi]\psi$, it is not necessary for a sound and complete axiomatic system like the one above(as proved by Ditmarsch et. al.) to include the before mentioned necessitation rule $from\;\phi\;derive\;[\psi]\phi$. In other literature I've read about the inclusion of this rule. What makes it necessary to include it because obviously with the above system to be sound and complete to $S5$ models it doesn't seem necessary.

Edit: $p$ in the 6th axiom corresponds to an atomic proposition from a countably infinite set $\mathcal{P}$.

• What does it mean $[\phi]p$ ? – Mauro ALLEGRANZA Mar 29 '17 at 11:19
• The operator $[\phi]$ corresponds to the public announcement of the formula $\phi$, i.e. $[\phi]\psi$ corresponds to after the announcement of $\phi$, it holds that $\psi$. $p$ in this case is a atomic propositional variable. – blub Mar 29 '17 at 11:28
• The semantics of $[\phi]\psi$ is : if $\phi$ holds in $M$, then $\psi$ hilds in the "$\phi$-restriction" of $M$, assuming that we know what it means a "-restriction"... – Mauro ALLEGRANZA Mar 29 '17 at 11:30
• Thus, your purported rule sounds like: if $\phi$ olds in $M$, then it holds in every $\psi$-restriction of $M$, whatever $\psi$ is ? – Mauro ALLEGRANZA Mar 29 '17 at 11:31
• @MauroALLEGRANZA I'm aware of this. My confusion arises from the fact that some axiomatic systems in the literature use this mentioned necessitation axiom and others like the one mentioned above from my main reference material doesn't. – blub Mar 29 '17 at 11:33

The axioms concerning the modality of the public announcement are usually called interaction or reduction axioms and they imply that this modality is superfluous in the language in terms of expressibility. Indeed, notice that all the axioms involving the interaction between the modality $[\varphi]$ and the rest of the connectives "push" the modality $[\varphi]$ to less complex formulas, and it disappears when it is in front of an atomic proposition. Hence you can devise a translation from the language expanded with the announcement modality to the language without the announcement modality that guarantees equivalence. The standard completeness proof relies on this reduction of PAL to just S5 and thus that it follows that the rule in question is derivable from the axioms and the existing rules (since it is sound).