 where \(R(\tau_1,\dots,\tau_n)\) and \(\tau_1 = \tau_2\) are atomic formulae. The truth functional connectives \(\vee, \rightarrow\), and \(\leftrightarrow\), as well as the temporal operators \(H\) and \(G\), can be defined as usual. Moreover, the dual \(\exists\) of \(\forall\) is defined by \(\exists x \varphi := \neg \forall x \neg \varphi\).