  In temporal logic (also known as tense logic), there are two basic operators, \(G\) for the future, and \(H\) for the past. \(G\) is read ‘it always will be that’ and the defined operator \(F\) (read ‘it will be the case that’) can be introduced by \(FA = {\sim}G{\sim}A\). Similarly \(H\) is read: ‘it always was that’ and \(P\) (for ‘it was the case that’) is defined by \(PA={\sim}H{\sim}A\). A basic system of temporal logic called \(\mathbf{Kt}\) results from adopting the principles of \(\bK\) for both \(G\) and \(H\), along with two axioms to govern the interaction between the past and future operators: