# Logic for Computer Scientists/Modal Logic/Temporal Logics

## Temporal Logics

The two modalities ${\displaystyle \square }$ and ${\displaystyle \diamond }$ cannot be used to distinguish between past and future. For this we need a multi-modal logic with the following ${\displaystyle \square }$-operators

• ${\displaystyle [F]A}$: ${\displaystyle A}$ holds always in the future
• ${\displaystyle [P]A}$: ${\displaystyle A}$ holds always in the past
• ${\displaystyle [A]A}$: ${\displaystyle A}$ holds always

and the corresponding ${\displaystyle \diamond }$-operators:

• ${\displaystyle \langle F\rangle A}$: ${\displaystyle A}$ holds somewhere in the future
• ${\displaystyle \langle P\rangle A}$: ${\displaystyle A}$ holds somewhere in the past
• ${\displaystyle \langle A\rangle A}$: ${\displaystyle A}$ holds somewhere

The semantics is then given as before, by giving constraints for the three reachability relations or by giving appropriate axioms, e.g.

• ${\displaystyle [F]A\to [F][F]A}$: Transitivity; an analog axiom holds for the two other ${\displaystyle \square }$-operators.
• ${\displaystyle A\to [F]\langle P\rangle A}$: if we go from a time point ${\displaystyle t}$ in the future ${\displaystyle t'}$, we can go back in the past to the time point where ${\displaystyle A}$ was true.
• ${\displaystyle [A]A\leftrightarrow [F]A\land [P]A}$: connection of past with future.

In addition there are many other aspects of temporal logics. E.g. one can distinguish between left- and rightlinear structures or between dense and discrete time structures.