But Findlay's remark, like so much that has been written on the subject of time in the present century, was provoked in the first place by McTaggart's ...

ABSTRACT Many temporal and modal logic languages can be regarded as subsets of first order logic, i.e. the semantics of a temporal logic formula is given as a first order condition on points of the underlying models (Kripke structures). Often the set of possible models is restricted to models which are trees. A temporal logic language is (first order) expressively complete, if for every first order condition for a node of a tree there exists an equivalent temporal formula which expresses (...) the same condition. In this paper expressive completeness of the temporal logic language with the set of operators U (until), S (since), and X k (k-next) is proved, and the result is extended to various other tree-like structures. (shrink)

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.