 There is a close correspondence between the A-series of time and tense logic, on the one hand, and between the B-series and first-order logic, on the other, as was already noted by Prior (1967, Chapter 1) himself. Consider, for example, the sentence “It is dark, it was light, and it will be light again.” This sentence can be formalized in TL as   \[\mathsf{dark} \wedge P(\mathsf{light}) \wedge F(\mathsf{light})\]   while its first-order formulation reads   \[\mathsf{dark}(t_1) \wedge \exists t_0 (t_0 \prec t_1 \wedge \mathsf{light}(t_0)) \wedge \exists t_2 (t_1 \prec t_2 \wedge \mathsf{light}(t_2)).\]    The TL formula consists of tensed propositions (propositions not containing temporal operators are present tensed), and it invokes the local perspective of the present. In the first-order formula, in contrast, propositions are untensed or tenseless. Here we are provided with predicates of time instants rather than with tenses, and the perspective involved is a global perspective from outside of time. Prior felt that not everything that can be expressed in a tensed language can likewise be expressed in a tenseless one, his classic example being: “Thank goodness, that’s over!” (Prior 1959).