 In light of these equivalences, the set of formulae of TL can be recursively defined as follows, over a given set of atomic propositions \(PROP\):   \[ \varphi := p \in {PROP} \mid \bot \mid \lnot \varphi \mid (\varphi \land \varphi) \mid P\varphi \mid F\varphi. \]    The truth-functional connectives \(\vee,\to,\) and \(\leftrightarrow\) are definable in terms of \(\lnot\) and \(\land\) as usual. Besides, we can define \(A\varphi =H\varphi \wedge \varphi \wedge G\varphi\) and, dually, \(E\varphi =P\varphi \vee \varphi \vee F\varphi,\) which on linear flows of time mean “always” and “sometime”, respectively.