 A basic language of first-order temporal logic (FOTL) is essentially an extension of a given first-order language by the operators \(P\) and \(F\). Whereas in propositional temporal logics atomic propositions are unstructured entities, in first-order temporal logics atomic formulae are built up from terms denoting individuals and predicate symbols denoting relations, and the language is equipped with quantifiers ranging over individuals. (A brief overview of first-order logic is provided in the supplementary document   First-order Relational Structures and Languages.)  In what follows, we consider FOTL over a relational first-order language (no function symbols) with equality. The set of formulae is defined as follows: