On the interpretability of arithmetic in temporal logic

DOI10.1016/0304-3975(90)90161-AMaRDI QIDQ915718zbMATH OpenFDO

Authors Fred Kröger

Publication date 1990

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(90)90161-A

zbMATH Keywords

arithmeticextending first-order temporal theories

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Review text

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.

Recommendations

• Arithmetical axiomatization of first-order temporal logic
• Arithmetical interpretations of dynamic logic
• On the proofs of arithmetical completeness for interpretability logic
• Arity hierarchy for temporal logics
• Temporal interpretation of intuitionistic quantifiers
• On the complexity of arithmetical interpretations of modal formulae
• On the expressive power of temporal logic
• A Road Map of Interval Temporal Logics and Duration Calculi
• A decidable intuitionistic temporal logic
• scientific article; zbMATH DE number 3957097

Cites work

• Concerning the semantic consequence relation in first-order temporal logic
• scientific article; zbMATH DE number 3982506 (Why is no real title available?)
• scientific article; zbMATH DE number 3985193 (Why is no real title available?)
• scientific article; zbMATH DE number 4049002 (Why is no real title available?)
• scientific article; zbMATH DE number 3248792 (Why is no real title available?)
• Incompleteness of first-order temporal logic with until
• Model theory

Cited in

(17)

• Arithmetical axiomatization of first-order temporal logic
• The power of temporal proofs
• Completeness of a first-order temporal logic with time-gaps
• Specification of abstract dynamic-data types: A temporal logic approach
• Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic
• The scope of Gödel's first incompleteness theorem
• LTL over integer periodicity constraints
• Invertible infinitary calculus without loop rules for restricted FTL
• Linear-time temporal logics with Presburger constraints: an overview
• Decidability and incompleteness results for first-order temporal logics of linear time
• A decidability result for the model checking of infinite-state systems
• scientific article; zbMATH DE number 1882007 (Why is no real title available?)
• A Branching Time Logical System for Open Distributed Systems Development
• Similarity saturation for first order linear temporal logic with UNLESS
• Proof-theoretical investigation of temporal logic with time gaps
• Incompleteness of a first-order Gödel logic and some temporal logics of programs
• Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics

This page was built for publication: On the interpretability of arithmetic in temporal logic

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