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.

Last modified on 13 July 2009, at 14:10

Logic for Computer Scientists/Modal Logic/Syntax

Syntax

Wikibooks ™