The power of temporal proofs
type: Item
instance of: scholarly article
title: The power of temporal proofs
zbMATH Open document ID: 0669.03010
DOI: 10.1016/0304-3975(89)90138-2
author: Martín Abadi
published in: Theoretical Computer Science
publication date: 1989-01-01T00:00:00Z
review text: 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)\).
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 4095429
zbMATH Keywords: axiomatic system complete with respect to nonstandard models of FTL
zbMATH Keywords: first order temporal logic
zbMATH Keywords: auxiliary definitions
MaRDI profile type: Publication
full work available at URL: 0304-3975(89)90138-2
OpenAlex ID: W2024016985
cites work: Axioms for tense logic. II: Time periods
cites work: Q4342094
cites work: Q3743300
cites work: Q4342097
cites work: Q5737082
cites work: Q4343990
cites work: Q5604443
cites work: Q5812175
cites work: Q4745241
cites work: Adequate proof principles for invariance and liveness properties of concurrent programs
cites work: Q3690194
cites work: Q3956390
cites work: Proving Liveness Properties of Concurrent Programs
cites work: The temporal semantics of concurrent programs
cites work: Q5573961
cites work: Q3698302
cites work: Provability interpretations of modal logic
cites work: Q4342096
description: scientific article; zbMATH DE number 4095429