Decidability and Incompleteness Results for First-Order Temporal Logics of Linear Time

Stephan Merz

Abstract

The question of axiomatizability of first-order temporal logics is studied w.r.t. different semantics and several restrictions on the language. The validity problem for logics admitting flexible interpretations of the predicate symbols or allowing at least binary predicate symbols is shown to be Π₁¹-complete. In contrast, it is decidable for temporal logics with rigid monadic predicate symbols but without function symbols and identity.

Available as:  gzip'ed Postscript 

Reference

@Article{merz:decidability,
  author = 	 "Stephan Merz",
  title = 	 "Decidability and Incompleteness Results for
                  First-Order Temporal Logics of Linear Time",
  journal =	 "Journal of Applied Non-Classical Logic",
  year =	 1992,
  volume =	 2,
  number =	 2
}