The power of temporal proofs (Q1118578)

Let FTL denote first order temporal logic with the temporal operators ``nexttime'' and ``until''. A simple proof is presented of the fact that the set of valid formulas of FTL is \(\Pi^ 1_ 1\)-complete (\textit{D. M. Gabbay} [J. Symb. Logic 37, 579-587 (1972; Zbl 0266.02025)] refers to an unpublished proof of this fact by D. Scott). Hence FTL cannot have an effective standard axiomatization. An axiomatic system \({\mathcal T}_ 0\) is proposed which is complete with respect to nonstandard models of FTL. But \({\mathcal T}_ 0\) is incomplete in another sense. Namely, there exists a simple formula f not deducible in \({\mathcal T}_ 0\) but the translation p(f) of f into first order arithmetic is deducible in a very simple arithmetic system. Two extensions of \({\mathcal T}_ 0\) are proposed which allow to introduce some auxiliary definitions. Some nonstandard completeness results are proved for these systems. In particular, the stronger of them is as powerful as Peano arithmetic, i.e. \({\mathcal T}_ 2\vdash f\) iff PA\(\vdash p(f)\).