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.