The needs of computer science demanded other kinds of temporal logic. One of them is so-called Linear Temporal Logic (Manna and Pnueli 1992; Manna and Pnueli 1995; Kontchakov, Kurucz, Wolter, Zakharyaschev 2007, 527-528; Kröger, Merz 2008).
In the LTL, there are two symmetrical parts, one for the past and another for the future. The structure of operators is the same for the past and future parts. The flow of time is considered as any strict linear order (W, <), where W is a set of time points w ∈ W and < is the precedence relation. A particular case when W = ℕ is of specific interest (cf. above about the role of graphs in the space representations). The language of the LTL does not allow saying (using Aristotle’s examples which were inspiring the most of modern temporal logicians) “it is necessary that there will be a sea-battle tomorrow” or “it is possibly that there will be a sea-battle tomorrow,” but only “there will be a sea-battle tomorrow.”
The main operators of the LTL are the binary operator U (“until”) for the future part of the LTL and S (“since”) for its past part, “sometime in the future” and “always in future” (⃟F and ⃞F, correspondingly, with symmetrical operators for the past), and the operator “at the next moment” (with its counterpart “at the previous moment”). The operator “always” is dual of the operator “sometime”: ⃞φ= ¬⃟¬φ, where φ is a formula of LTL.
As it has been noted, the operators ⃞ and ⃟ are analogous to the classical quantifiers ∀ and ∃, respectively, and so, a formula ⃟A is the temporal closure of A (Kröger, Merz 2008, 32). We can add, that, in the same sense, a formula ⃞A is the temporal interior of A.
Therefore, leaving aside technical details of the LTL itself, we can summarize its basic ideas as following. The time is considered as a kind of a topological space, where the operators of necessity (any) and possibility (some) are applicable as, respectively, time interior and time closure. The precedence relation is interpreted as a ‹1, 1, 1› type operator analogous to the same type operators of the space and preferences logics.
The ‹1, 1› type operators are presented, though implicitly, as a triplet “somewhere in time,” “anywhere in time,” and “nowhere in time.”
Here we are not interested in practical purposes of the creators of the LTL, and so, need not going deeper into its details. The only basic intuition of the linear approach to time is what we really interested in. Thus, we can see, that the time could be treated as a dimension of the space.
Indeed, in this dimension, the first metrical axiom holds: d (x, y) = 0 iff x = y (identity of indiscernibles). The third axiom (triangle inequality) is inapplicable to a one-dimension space. The second axiom d (x, y) = d (y, x) (symmetry) holds only for some kinds of time perception, as it is the case for the space.
Indeed, for our time thinking, a journey back in time is not a problem, and so, our time thinking logic is not to be divided into past and present parts. Moreover, if we are “speaking about” our present state, then, our present has no preference over other time modalities, and so, there is no need to introduce “at the next moment of time” as a specific operator.
Our final conclusion is that, for the human cognitive sphere, there is no time as something different by nature from the space. Our cognitive time is rather a dimension of our cognitive space. Thus, there is no specific logic of time in the human cognitive sphere. The logic of space is enough.