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{array}{ccc}& & \diamond A\text{ and}\\ & & ◻A\end{array}$

are formulae.

The symbols $\diamond$ and $◻$ 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 $◻A$ for $A$ is always true.