 Thus, validity of a formula of TL in a temporal model is a first-order property. Validity in a temporal frame, on the other hand, turns out to be a second-order property as it involves quantification over valuations. If we treat the unary predicates from \(\mathcal{P}\) as predicate variables of a second-order language \(L_{2},\) every temporal frame \(\mathcal{T} = \langle T,\prec\rangle\) can be regarded as an \(L_{2}\)-model, where the predicate variables represent the valuation of the respective atomic propositions. Let \(\forall \overline{P}\varphi \) denote the universal closure of an \(L_{2}\)-formula \(\varphi\) over all predicate variables occurring in it. Then: