Logic for Computer Scientists/Modal Logic/Syntax

Syntax

We assume the syntax of classical propositional logic as used in the chapters above. Additional we have the following two rules: If $A$ is a formula

${\begin{matrix}&&\diamond A{\mbox{ and}}\\&&\square A\end{matrix}}$

are formulae.

The symbols $\diamond$ and $\Box$ stand traditionally for possibility and necessity; in the context of temporal logic they stand for always and eventually, so that $\diamond A$ stands for $A$ is eventually true and $\Box A$ for $A$ is always true.