  Prior showed that if various assumptions are made concerning the relation \(l\), the axioms of the tense calculus can be proved in the \(l\)-calculus. (Two years later, he and Meredith used essentially the same strategy in creating the possible worlds semantics for ordinary modal logic.) He discovered that \(FFp \rightarrow Fp\) and its image \(PPp\rightarrow Pp\) follow from the assumption \(lxy \rightarrow (lyz \rightarrow lxz),\) stating that the relation \(l\) is transitive. \(Fp \rightarrow FFp\) and its image \(Pp \rightarrow PPp\) follow given the assumption lxz \(\rightarrow \exists y(lxy \amp lyz),\) stating that ‘between any two dates there is another date’ (a condition sometimes said to express time’s density). \(Gp \rightarrow Fp\) follows given \(\exists xlxz,\) stating that ‘there is a date later than any given date’, i.e., that there is no last moment of time.  \(Hp \rightarrow Pp\) requires \(\exists xlzx,\) stating that there is no first moment of time.