 The standard translation of TL into first-order logic enables a systematic treatment of various aspects of temporal logic with the tools and techniques of classical logic (see e.g. Blackburn et al. 2006). As we will see in  Section 3.6,  however, not all first-order properties of temporal frames are definable by temporal formulae; and vice versa, not all properties of temporal frames that can be expressed by formulae of TL are first-order definable. A non-trivial correspondence between temporal logic and first-order logic as alternative languages for describing properties of time emerges.