On the interpretability of arithmetic in temporal logic (Q915718)

In this paper techniques of extending first-order temporal theories by definitions of new function symbols are developed after the manner of classical first-order logic. These techniques have enabled the author to interpret classical first-order theories, including arithmetic in particular, in a temporal one. The results of \textit{A. Szalas} [Theor. Comput. Sci. 47, 329-334 (1986; Zbl 0622.03012)] are strengthened as follows: There is no sound and complete finitistic axiomatization of first-order temporal logic with equality (with \(\bigcirc\) and \(\square)\) in each of the following two cases: (a) The language allows quantification only over global variables and contains at least two binary function symbols. (b) The language allows quantification over global and local variables and has an arbitrary (particularly empty) signature.