 Not every first-order formula has a correspondent in TL. Actually, with a little extra care to re-use individual variables, TL can be translated in the two-variable fragment FO\(^{2}\) of first-order logic, which eventually implies decidability of validity in TL (for validity in FO\(^{2}\) is decidable, as shown by Grädel and Otto 1999). For instance, the example above can be re-written as