Logic for Computer Scientists/Modal Logic/Syntax

< Logic for Computer Scientists‎ | Modal Logic


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.