Last modified on 13 July 2009, at 14:10

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 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.