That is, given a temporal model \(\mathcal{M}\), a formula of the form \(P\varphi\) is true at an instant \(t\) iff \(\varphi\) is true at some earlier instant \(t',\) and \(F\varphi\) is true at \(t\) iff \(\varphi\) is true at some later instant \(t'.\) Consequently, for the duals \(H\) and \(G\), it holds that \(H\varphi\) is true at \(t\) iff \(\varphi\) is true at all earlier instants \(t',\) and \(G\varphi\) is true at \(t\) iff \(\varphi\) is true at all later instants \(t'.\)