  Prior’s expanded calculus contained two additional axioms concerning futurity, \(Gp \rightarrow Fp\) and \(Fp \rightarrow FFp.\) There was also a simplification: instead of following his previous practice and defining \(G\) as \(\neg F\neg\), Prior took \(G\) as undefined and defined \(F\) as \(\neg G\neg\); this enabled him to replace the somewhat unwieldy axiom (1) by the more elegant \(G(p \rightarrow q) \rightarrow(Gp \rightarrow Gq)\). Moreover, he transformed this calculus of ‘pure futurity’ into a calculus of ‘pure pastness’ by replacing \(F\) throughout the axioms, rules, and definition, by the past tense operator \(P\) (‘It has been the case that’), and replacing \(G\) by the past perpetual operator \(H\) (‘It has always been the case that’).