A Logic with Progressive Tenses

Abstract

Let (W, <) be a strictly linearly ordered set (a “time-line”). Having a Kripke model over (W, <) we interpret simple past and future operators in the well-known way:

$$ \begin{gathered} x \vDash FA \Leftrightarrow \left( {\exists y > x} \right)y \vDash A \hfill \\ x \vDash PA \Leftrightarrow \left( {\exists y < x} \right)y \vDash A. \hfill \\ \end{gathered} $$