Incompleteness of first-order temporal logic with until (Q1123184)

The version of first-order temporal logic (with equality) chosen in this paper is essentially that introduced by \textit{Z. Manna} and \textit{A. Pnueli} [Verification of concurrent programs: the temporal framework, in: The correctness problem in computer science (\textit{R. S. Boyer} and \textit{J S. Moore} (eds.)), 215-273 (1981; Zbl 0476.68009)]; it uses the temporal modalities ``always'', ``sometimes'', ``next time'', ``until'' and ``at next''. It is shown that this logic is weakly incomplete (the set of tautologies over an arbitrary signature is not r.e.) and strongly incomplete (the set of tautologies is r.e. for no signature). Although the first claim is a consequence of the second, they are separately presented. The proof of the first theorem is analogous to the proof of incompleteness of second-order prediate logic. It is based on Trakhtenbrot's theorem and the fact that finite structures are characterizable in temporal logic (this result is interesting by its own). For the second theorem, the technique consists in reducing the complement of the halting problem for Turing machines to the problem whether a temporal formula (only with \(``='')\) is a tautology.