The power of temporal proofs

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)\).

Recommendations

Cites work

Cited in

(30)

This page was built for publication: The power of temporal proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1118578)