Completeness through Flatness in Two-Dimensional Temporal Logic

Abstract. 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.