 The reduction axioms characterize truth of an announcement formula \([F!]G\) in terms of the truth of other announcement formulas \([F!]H\) whose post-announcement formula H is less complex than the original post-announcement formula G. In the case where G is just a propositional letter p, Reduction Axiom 1 says that the truth of \([F!]p\) can be reduced to a formula not containing any announcements of F. So we see that the reduction axioms “reduce” statements of truth of complicated announcements to statements of truth of simpler and simpler announcements until the mention of announcements is not necessary. For example, writing the reduction axiom used in a parenthetical subscript, we have the following sequence of provable equivalences: 