The other Boolean connectives 1,  ∧, →, and ↔ are used as abbreviations in the standard way. In addition, we abbreviate ¬[α]¬A to &lt;α&gt;A (“some execution of α from the present state leads to a state where A is true”) as in modal logic. We write αn for α;…;α with n occurrences of α. More formally: