 In this model, \(F(x)q\) is true at \(t_2\) and \(F(x+y)q\) is true at \(t_1\), although none of the propositions are necessary, since \(F(x){\sim}q\) is possible at \(t_2\). The reason why \(F(x)q\) is true at \(t_2\) is just that the evaluation of a proposition according to the true futurist theory should be based on the specified branch through \(t_2\) representing “the future” at \(t_2\) within the model. However, as we shall see in the following, it turns out that the idea of a specified branch at every moment can be integrated into the semantics in several ways. But first of all some comments on the very idea of a specified branch.