  Prior showed, furthermore, that no assumptions at all are needed for the derivation of the two interactive axioms \(p \rightarrow GPp\) and \(p \rightarrow HFp,\) nor for the axioms \(G(p \rightarrow q) \rightarrow(Gp \rightarrow Gq)\) and \(H(p \rightarrow q) \rightarrow (Hp \rightarrow Hq)\). In the case of these formulae, the ordinary machinery of truth-functional and quantifier logic suffices for their proof. The same is true, he showed, of the four rules of the tense calculus ((3) and (4) above, together with the \(P\) form of (3) and the \(H\) form of (4)). This part, therefore, of Prior’s calculus of tenses is purely logical, whereas others of the axioms—those stating that \(l\) is transitive, that time is dense, and that there is no first or last moment of time—express physical properties of time. In later work, Prior considered further calculi, in which these particular ‘physical’ axioms are replaced by others, for example axioms stating that time has a first moment, or is linear (a ‘straight line’), or is non-linear, with the present always standing at the junction of a number of branches, any of which might become the actual future.