Axiomatizing the monodic fragment of first-order temporal logic (Q1849866)

It is shown that the fragment of the first-order temporal logic over the natural numbers that has no functional symbols, no equality and contains only monodic formulas, i.e., all those where each temporal subformula has at most one free variable, can be given a Hilbert-style axiomatization. Moreover, adding equality yields a theory which is not recursively enumerable. Finally the paper shows that the monodic fluted fragment and the monodic loosely guarded fragment are decidable.