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