1. Tkaczyk and Jarmużek (2019) have recently stressed Łoś’s contribution to the emergence of temporal logic. Their paper was followed by a response by Øhrstrøm and Hasle (2019), clarifying Łoś’s influence on Prior.

2. Especially in the early computer science literature, sometimes the notation \(\small{\bigcirc}\) instead of \(X\) is used for the Next Time operator.

3. In the philosophical logic literature, often a prefix notation for \(U\) and \(S\) is used and the two arguments are swapped, i.e., \(U\psi \varphi\) is used for \(\varphi U\psi\).

4. In fact, the reflexive versions of \(S\) and \(U\) can be defined in terms of the strict ones, e.g. \(\varphi S_{\mathit{ref}}\psi :=\psi \vee (\varphi \land \varphi S\psi)\), but generally not vice versa. Still, on discrete linear frames, the strict operators are definable in terms of their reflexive counterparts by making use of \(X\) and its past analogue, respectively: e.g. \(\varphi U\psi := X(\varphi U_{\mathit{ref}}\psi)\).

5. As outlined in Øhrstrøm and Gonzalez (2022), Prior toyed with the idea of branching time –– or the big Y –– already before he received Kripke’s letter, inspired by the science fiction novel The Seeds of Time (1956) by John Wyndham.

6. We have adopted this example from the original entry on Temporal Logic by Anthony Galton (Galton 2008).

7. Note that the assumption that the global domain is the union of all local domains intuitively excludes the possibility of fictitious individuals, who do not really exist at any time instant. The problem can be resolved by allowing for temporally isolated instants or possible worlds, where such fictitious objects can reside. Alternatively, one can drop the above requirement and allow objects in the global domain which do not belong to any local domain.

8. Here we adopt the terminology from McArthur (1976).