# Logic for Computer Scientists/Modal Logic/Syntax

## SyntaxEdit

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

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

are formulae.

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