Completeness through Flatness in Two-Dimensional Temporal Logic

12 years 5 months ago
Completeness through Flatness in Two-Dimensional Temporal Logic
We introduce a temporal logic TAL and prove that it has several nice features. The formalism is a two-dimensional modal system in the sense that formulas of the language are evaluated at pairs of time points. Many known formalisms with a two-dimensional flavor can be expressed in TAL, which can be seen as the temporal version of square arrow logic. We first pin down the expressive power of TAL to the three-variable fragment of first-order logic; we prove that this induces an expressive completeness result of `flat' TAL with respect to monadic first order logic (over the class of linear flows of time). Then we treat axiomatic aspects: our main result is a completeness proof for the set of formulas that are `flatly' valid in well-ordered flows of time and in the flow of time of the natural numbers.
Yde Venema
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Where ICTL
Authors Yde Venema
Comments (0)