Abstract

We present a Hilbert style axiomatisation for the set of formulas in the temporal language with F and P which are valid over non-transitive cyclical flows of time. We also give a simpler axiomatisation using the slightly controversial 'irreflexivity rule' and go on to prove the decidability of any temporal logic over cyclical time provided it uses only connectives with first-order tables