# 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

## 1 Answer

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.

• Thank you. I was suspecting this reasons I was just not completely safe around this matter. – blub Mar 29 '17 at 18:27