## SyntaxEdit

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

are formulae.

The symbols and stand traditionally for *possibility* and
*necessity*; in the context of temporal logic they stand for *always* and
*eventually*, so that stands for * is eventually true* and
for * is always true*.