The power of temporal proofs (Q1118578): Difference between revisions
From MaRDI portal
Set OpenAlex properties. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: Axioms for tense logic. II: Time periods / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4342094 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3743300 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4342097 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5737082 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4343990 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5604443 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5812175 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4745241 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Adequate proof principles for invariance and liveness properties of concurrent programs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3690194 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3956390 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proving Liveness Properties of Concurrent Programs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The temporal semantics of concurrent programs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5573961 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3698302 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Provability interpretations of modal logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4342096 / rank | |||
Normal rank |
Latest revision as of 14:52, 19 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The power of temporal proofs |
scientific article |
Statements
The power of temporal proofs (English)
0 references
1989
0 references
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)\).
0 references
axiomatic system complete with respect to nonstandard models of FTL
0 references
first order temporal logic
0 references
auxiliary definitions
0 references
0 references