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}$.
 A: 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).
Notice that usually in these systems uniform substitution is not mentioned in the rules (though I have not look at the Van Ditmarsch et. al. book so I'm not sure regarding the proof of completeness there). However it has been shown that substitution is necessary for completeness. The paper I mention has also more details on the reduction axioms (and thus pertain to your question), if you are interested.
