Tero Tulenheimo

Logic of Time Division on Intervals of Finite Size

. It is syntactically like basic modal logic with an additional unary operator but it has an intervalbased semantics. The formula ψ is interpreted as meaning 'the current interval has a finite partition of size at least two such that all its members are non-empty and satisfy ψ.' In the present paper the expressive power of TD is studied on the class K fin of all intervals of finite size. This logic is characterized from the viewpoint of formal language theory by using certain regular-like operators. We prove that TD is not translatable into first-order logic over K fin . An extension TDN of TD is considered, obtained by making the additional operator 'and next' available. The logic TDN is characterized in terms of regular operators and it is seen to coincide for its expressive power with monadic second-order logic over K fin . We also study some closure properties of definable classes of intervals in connection with certain fragments of TDN.

Introduction

Logic of time division or TD was introduced and studied in [START_REF] Tulenheimo | Modal Logic of Time Division[END_REF]. Conceptually this logic was motivated by G. H. von Wright's discussion of 'real contradictions' [START_REF] Von Wright | Time, Change, and Contradiction[END_REF]. In his terminology, an interval exemplifies a real contradiction if at least one part of any division of this interval involves the presence of contradictorily related (though non-simultaneous) states. Now, von Wright used a modal-logical formalism to explicate this notion. However, as spelled out in [START_REF] Tulenheimo | Negation and Temporal Ontology[END_REF], his characterization of real contradictions was mistaken: in his formulation he used negation in an ambiguous way, without distinguishing the two negations 'does not hold at an interval' and 'fails throughout an interval.' The logic TD is an interval-based modal logic in which those two negations are distinguished and whose modal operators are so interpreted that the logic can be used to describe divisibility properties of temporal intervals. In computer scientist's jargon, then, TD is a tool for reasoning about divisibility. In philosophical discussions on the nature of time, considerations related to divisibility have had a role at least since Zeno of Elea (5th c. BC). The logic TD identifies a simple framework to study properties of temporal flows describable in terms of divisibility statements. The general semantics of TD is defined on intervals of any cardinality and any order type. In the present paper we take up one of the questions left open in [START_REF] Tulenheimo | Modal Logic of Time Division[END_REF], namely looking into the behavior of this logic on intervals of finite size.

Basic notions

Given a fixed finite set π of propositional atoms, temporal flows are represented as triples (T, <, V ), where T is a finite set, < is an irreflexive linear order on T , and V is a valuation function which associates every element t of T with a subset V (t) of π. These triples (T, <, V ) are termed intervals. If i = (T, <, V ), the set T is the domain of i, denoted dom(i). Intuitively, T is a set of instants and < is an earlier than relation on T . The function V specifies how the events represented by propositional atoms are distributed over the abstract time structure (T, <). Note that because the set T is assumed to be finite, it has automatically both a minimum and a maximum relative to the relation <. Also, the relation < is automatically discrete in the sense that every instant t ∈ T distinct from max(T ) has an immediate successor, and every instant t ∈ T distinct from min(T ) has an immediate predecessor. If i = (T, <, V ) is an interval, the structure (T ′ , < ′ , V ′ ) is its subinterval provided that T ′ ⊆ T , and < ′ and V ′ are the restrictions of < and V , respectively, to the set T ′ . The structure (T ′ , < ′ , V ′ ) is itself an interval, and we say more specifically that it is the subinterval of i determined by the set T ′ , denoted i T ′ . If an interval i = (T, <, V ) is clear from the context and t, t ′ ∈ T , we write [[t, t ′ ]] for the subinterval i [t,t ′ ] and ((t, t ′ ]] for the subinterval i (t,t ′ ] , where [t, t ′ ] := {x : t ≤ x ≤ t ′ } and (t, t ′ ] := {x : t < x ≤ t ′ }. If t = t ′ , the domain of the subinterval [[t, t ′ ]] is the singleton {t}; we denote this interval simply by [[t]].

Note 1.1 In the terminology of the present paper, intervals are structures with a builtin order and a built-in valuation. By contrast, in the common mathematical usage, an interval I is simply a set, specified relative to a fixed linear order ≺ on some set T in terms of bounds a, b ∈ T with a b. For example, the sets [a, b] := {x : a x b} and (a, b] := {x : a ≺ x b} are such intervals. This common usage could be generalized by defining an interval I as any inwards-closed subset of T : if t 1 , t 2 ∈ I and x is any element of T with t 1 ≺ x ≺ t 2 , then x ∈ I. In this generalized sense for instance the set {x ∈ Q : 2 < x 2 < 5} would be an interval relative to the set of rational numbers ordered by magnitude, although the set in question could not be expressed in terms of bounds: the relevant infimum and supremum do not exist in Q.

Regarding intervals construed as structures (as opposed to sets), an external and an internal viewpoint may be distinguished. If some structure (T, <, V ) has been fixed, an interval in the external sense is any substructure (T ′ , < ′ , V ′ ) of (T, <, V ) such that the set T ′ is inwards-closed. In the present paper we speak of intervals in the internal sense. Intervals of this kind are not defined with reference to any larger structures. For example, if [0, 1] and [2, 3] are inwards-closed sets of rational numbers ('rational intervals' in the sense of the common usage), < is the order of rationals by magnitude, and V is any valuation, then the substructure of (Q, <, V ) determined by the set [0, 1] ∪ [2, 3] is an interval in the internal sense. But it is not an interval in the external sense relative to (Q, <, V ), as its domain [0, 1] ∪ [2, 3] is not inwards-closed.

We allow the domain of an interval to be empty. There is exactly one empty interval, namely the structure (∅, ∅, ∅) which will be denoted by Λ. If S is a set, we denote by |S| its cardinality. The size of an interval i is denoted by |i|; by definition |i| := |dom(i)|. We write t ∈ i to indicate that t belongs to the domain of i. We let K fin stand for the class of all intervals -which by definition are of finite size. Further, we write K fin (π) for the class of those intervals (T, <, V ) whose associated valuation is of type T → P(π). 1The notion of division is crucial throughout the paper. We think of divisions as triggered by division points. Because the temporal flows considered are finite, a fortiori the sets of division points are finite as well. The division of an interval i is a tuple i 1 , . . . , i n of intervals such that (a) it has at least two members (the division is proper, so to say), (b) the set {dom(i 1 ), . . . , dom(i n )} is a partition of the set dom(i), (c) no set dom(i j ) is empty, (d) if j < k, t ∈ dom(i j ) and t ′ ∈ dom(i k ), then t precedes t ′ in the order of the interval i, and (e) the members of the partition are determined by the correlated set of division points. For simplicity, we will apply the following specific definition. If i is an interval and min(i) ≤ t 1 < . . . < t n < max(i), we take the division D i (t 1 , . . . , t n ) of i by the points t 1 , . . . , t n to be the tuple [[min(i), t 1 ]], ((t 1 , t 2 ]], . . . , ((t n-1 , t n ]], ((t n , max(i)]] .

The members of a division are called its parts. We write j ∈ D i (t 1 , . . . , t n ) to indicate that j is a part of the division D i (t 1 , . . . , t n ) of the interval i.

If K is a class of intervals and L and L ′ are logics whose semantics are defined over intervals, L is translatable into

L ′ over K (written L ≤ K L ′ ) if for every φ ∈ L, there is ψ φ ∈ L ′ such that for all i ∈ K: i |= φ iff i |= ψ φ .
This is the standard definition of a logic being at most as expressive as another one; cf., e.g., (Ebbinghaus and Flum, 1999, Def. 7.1.3). It is not required that there be a computable function providing the translation. Below we indeed comment on the computability aspect in connection with certain translations, but it is not a part of the definition. We say that L ′ is more expressive than L over K (denoted

L < K L ′ ) if L ≤ K L ′ but L ′ ≤ K L.
The logics L and L ′ are said to have the same expressive power over K (in symbols

L = K L ′ ) if L ≤ K L ′ and L ′ ≤ K L. Finally, L and L ′ are incomparable over K (written L || K L ′ ) if L ≤ K L ′ and L ′ ≤ K L.
In this paper we will speak in a generalized sense of translatability even between logics and certain classes of expressions other than logical formulas.

It is assumed that the reader is familiar with the standard formulation of first-order logic (FO), when the semantic relation M, γ |= φ is defined for all models M with a nonempty domain M , first-order formulas φ and variable assignments γ : Free(φ) → M , where Free(φ) is the set of free individual variables of φ. We restrict attention to vocabularies which contain only relation symbols (no constant or function symbols). In the present paper we allow the case that the domain of a model is empty. 2 Strictly speaking there is one such 'empty model' for every vocabulary; in each case every relation symbol of the vocabulary is interpreted by the empty set. For every vocabulary τ , the relation M, γ |= φ is defined in this generalized setting for all models M of vocabulary τ (including the empty ones), first-order formulas φ of vocabulary τ , and assignments γ : Free(φ) → M . It should be noted that if M is empty, there are no assignments of type Free(φ) → M unless also the set Free(φ) is empty, i.e., unless φ is a sentence (formula whose all occurrences of variables are bound). If indeed Free(φ) = ∅, there is exactly one assignment of type Free(φ) → ∅, namely the empty assignment, which set-theoretically speaking equals the empty set. The semantic clauses for quantifiers are kept intact. If M is an empty model and Q ∈ {∀, ∃}, the condition M, γ |= Qxψ is defined iff γ is the empty assignment and the only free variable of ψ is x. If Q = ∀, the condition holds trivially and if Q = ∃, it fails trivially. In the former case this is because for every a ∈ ∅, we have M, γ ∪ {(x, a)} |= ψ; in the latter case, again, because for every a ∈ ∅, we have M, γ ∪ {(x, a)} |= ψ. Both conditions hold because there are no elements a in ∅. The quantifier rank of an FO formula is its maximum number of nested quantifiers. For the technique of using Ehrenfeucht-Fraïssé games to prove the elementary equivalence of two structures up to a given quantifier rank, see [START_REF] Ebbinghaus | Finite Model Theory[END_REF]. Monadic second-order logic (MSO) is obtained from FO by allowing atomic formulas Xy and complex formulas ∀Xφ and ∃Xφ, where X is a unary relation variable and y is an individual variable; see e.g. [START_REF] Ebbinghaus | Mathematical Logic[END_REF]. The unary relation variables range over arbitrary subsets of the domain. Here the relation M, γ |= φ is defined for MSO formulas φ and assignments γ : Free(φ) ∪ Free 2 (φ) → M , where Free 2 (φ) is the set of free relation variables of φ, by extending the corresponding definition for FO sketched above. Note that if M = ∅, the condition M, γ |= φ is defined iff the set Free(φ) is empty; the condition is indeed defined even if the formula φ contains free relation variables, because the power set of M is non-empty even if M is empty. We will write FO[τ ] (respectively MSO[τ ]) for the set of all sentences of first-order logic (monadic-second order logic) of vocabulary τ .

Logic of time division

Let us begin by recalling the syntax and semantics of the logic of time division or TD, here formulated with an eye on our present interests, i.e., assuming that the relevant intervals of evaluation are finite. Basic semantic properties of this logic are then briefly discussed before we proceed, from Section 3 on, to a more systematic study of the expressive power of this logic.

Syntax and semantics of TD

Syntactically, the logic of time division is simply basic modal logic (ML) with an additional unary operator (∼). Let π be a finite (possibly empty) set of atoms. The syntax of the logic TD[π] is given by the grammar

φ ::= p | ⊥ | ⊤ | ∼φ | ¬φ | (φ ∨ φ) | (φ ∧ φ) | φ | φ,
with p ∈ π. When making claims which hold for every set of atoms π, we simply write TD. In this case, then, we speak of the logic of time division generically.

The way in which the symbols and are interpreted is totally unrelated to ML. Here we use these operators to speak of divisibility properties of intervals relative to which the formulas are evaluated. Both ¬ and ∼ are negation symbols, to be referred to as the 'contradictory negation' and 'universal negation,' respectively. The formula ¬φ denies what φ affirms: ¬φ is true at an interval iff φ is not true at it. By contrast, ∼ φ states that φ fails throughout the interval of evaluation: ∼φ is true at i iff φ is false separately at every time point that belongs to i. 3 We may construe the symbols ⊥ and ⊤ as nullary connectives.

The semantics of TD[π] is specified by defining recursively the relation 'i |= φ' for all intervals i = (T, <, V ) in the class K fin (π) and for all formulas φ of TD[π]:

• i |= p iff p ∈ V (t) for all t ∈ i • i |= ⊥ iff t = t for all t ∈ i • i |= ⊤ iff t = t for all t ∈ i • i |= ∼ψ iff [[t]] |= ψ for all t ∈ i • i |= ¬ψ iff i |= ψ • i |= (ψ ∧ χ) iff i |= ψ and i |= χ • i |= (ψ ∨ χ) iff i |= ψ or i |= χ • i |= ψ iff
for some positive integer n there are instants t 1 , . . . , t n with min(i) ≤ t 1 < . . . < t n < max(i) such that for each part j of the division D i (t 1 , . . . , t n ), we have j |= ψ

• i |= ψ iff for all positive integers n and all instants t 1 , . . . , t n with min(i) ≤ t 1 < . . . < t n < max(i), there is a part j of the division D i (t 1 , . . . , t n ) such that j |= ψ.

Seen as a generalized quantifier, the unary operator involves semantically secondorder existential and first-order universal quantification. To make this explicit, note that the truth-condition of φ relative to the interval i is as follows: there exists a non-empty set {t 1 , . . . , t n } of division points (existential quantification over sets), φ holds at the interval [[min(i), t 1 ]], and for all t i and t j which are successive in the set {t 1 , . . . , t n , max(i)}, the formula φ holds at the interval ((t i , t j ]] (here we have first-order universal quantification). Dually, φ asserts at i that for any division of i, at least one of its parts makes φ true.4

Examples of definable properties

If φ is a formula of TD[π], we write Mod(φ) for the set {i ∈ K fin (π) : i |= φ}. A formula φ is said to define a class K of intervals, if K = Mod(φ). By the above semantics, the empty interval Λ belongs to the set Mod(p) for every p ∈ π. Regarding the nullary connectives ⊤ and ⊥, we may note the following:

Mod(⊤) = K fin , Mod(⊥) = {Λ}, Mod(¬⊥) = K fin \ {Λ}, Mod(¬⊤) = ∅.
In the present setting, then, due to the availability of the empty interval, ⊥ cannot be defined as ¬⊤, nor can ⊤ be defined as ¬⊥. In particular, ¬⊥ has existential force: it states that in the interval considered there is at least one time point. The formula ⊤, again, lacks existential force. It is also worth noting that ⊥ is not equivalent to the formula (p ∧ ¬p) for any p ∈ π. Namely, the formula ¬p has existential force (it states that there is at least one point at which p fails), while ⊥ does not have. On the other hand, ⊤ is indeed equivalent to (p ∨ ¬p), for any p ∈ π.

The operator has a limited capacity to speak of the size of the interval of evaluation: it is a necessary condition for the truth of the formula φ at i that i be of size at least 2. This is because divisions by definition have at least 2 parts. The following are examples of conditions on the size of the interval of evaluation that can be expressed.

Example 2.1 If n ≥ 1, write n for the string consisting of n occurrences of ; define n similarly.

(i) Mod( n ⊤) = {i ∈ K fin : |i| ≥ 2 n } (ii) Mod( n ⊥) = {i ∈ K fin : |i| ≤ 2 n -1} (iii) Mod(¬⊥ ∧ ⊥) = {i ∈ K fin : |i| = 1}.
In particular, then, the condition 'being of size 1' is definable in TD: the defining formula (¬⊥ ∧ ⊥) simply says of its interval of evaluation that it is non-empty (the left conjunct) but is not of size at least 2 (the right conjunct). The formula ⊥ cannot be true at any interval of size at least two, since those intervals do have divisions into at least two nonempty parts, while no non-empty part can make ⊥ true. Conversely, the formula ⊥ is clearly trivially true at any interval of size at most 1.

If p is atomic, then ¬p holds at i iff there is at least one instant in i at which p does not hold. By the combined use of the two negations, using the formula ¬ ∼ p, it can be positively stated that at some instant of i, the atom p holds. Moving to complex formulas, note that for example ¬ q does not state that there is an instant at which q fails (there is, of course, no such instant); instead the formula states that the interval has a division such that q fails at all parts of the division. Observe also that a complex formula may hold at i without holding at all instants of this interval. Here is a strong counterexample: a formula which is true at a certain interval while failing at all of its instants. Let i 0 be an interval consisting of just two instants, one making p true and q false, the other making q true and p false. Consider the formula φ := ¬(p ∨ q). Then clearly i 0 |= φ, while i 0 |= ∼φ. The latter condition prevails due to the fact that both instants in i 0 indeed fail to satisfy φ, because both of them do satisfy (p ∨ q).

To illustrate why the distinction between the two negations is of interest in the setting of arbitrary intervals, and specifically why this distinction was useful when critically discussing von Wright's notion of real contradiction in [START_REF] Tulenheimo | Negation and Temporal Ontology[END_REF], let us allow for the sake of example the use of intervals with an infinite domain; recall the notion of real contradiction from the beginning of Section 1. Von Wright correctly noted that an interval i manifests in his sense a real contradiction iff the formula (p ∨ ∼ p) does not hold at i,5 for some atom p. (He considered atoms as representing the sorts of states of the world that he was interested in.) However, operating with a single negation, he took this negative condition to be positively expressible by the formula ∼ (p ∨ ∼ p), which he furthermore also took to be expressed by the formula (p ∧ ∼p). Thus, von Wright thought ∼ to be capable of representing the contradictory negation 'does not hold at an interval.' Yet he was also committed to ∼p being true of an interval iff p fails throughout the interval. But if ∼ is the contradictory negation, ∼p means something less: that somewhere within the interval p fails. If ∼ has the force 'does not hold at an interval,' it cannot also have the force 'fails throughout an interval.' In fact, the notion of real contradiction is correctly captured by making joint use of the two negations of TD: the relevant condition is expressed by the formula ¬ (p ∨ ∼p) or, equivalently, by (¬p ∧ ¬ ∼p).

Example 2.2 Let T be the set of all integers. Write < for their usual order (order by magnitude). Define an order ≺ on T as follows:

z ≺ z ′ iff (0 ≤ z < z ′ ) or (z < z ′ ≤ -1)
or (z ≥ 0 and z ′ ≤ -1). The order type of the order (T, ≺) is, then, ω +ω * . The minimum of T w.r.t. ≺ is 0 and its maximum is -1. Let V be a valuation satisfying p ∈ V (z) iff the absolute value of z is even. Then the interval i = (T, ≺, V ) exemplifies a real contradiction. Namely, let the points t 1 , . . . , t n with 0 t 1 ≺ . . . ≺ t n ≺ -1 be arbitrary, and consider the division D determined by these points. Let s be the greatest non-negative integer in the set {0, t 1 , . . . , t n , -1} w.r.t. the order ≺, and let s ′ be the smallest negative integer of this set w.r.t. the same order. Thus, one of the parts of D is the interval ((s, s ′ ]]. Now, there are infinitely many integers z with s ≺ z ≺ s ′ . Among them there are points making p true and points making p false. Therefore the interval ((s, s ′ ]] satisfies neither p nor ∼p. As the division D was assumed to be arbitrary, it follows that i |= (p ∨ ∼p).

It is not difficult to see that when attention is restricted to finite intervals of size at least 2, real contradictions may not occur. At any interval of size at most 1, all formulas of the form φ fail. Under the above definition they exemplify, then, a real contradiction, but they do not do so because of the way in which their constituent states are distributed over the interval (which is where the interest lies in connection with real contradictions), but because they are 'too small.'

Fact 2.3 If i is a finite interval with |i| ≥ 2 and p is an atom, then i |= (p ∨ ∼p).
Proof. Let i be a finite interval of size at least 2. If its domain is {t 1 , . . . , t n } with t 1 < . . . < t n , consider its division by the points t 1 , . . . , t n-1 . The parts of the division are the singleton intervals [[t j ]] with 1 ≤ j ≤ n. Since every point t j either satisfies p or does not satisfy it, it follows that this division witnesses the claim i |= (p ∨ ∼p).

We may note that in the general formulation of TD, infinity and finiteness are definable properties of intervals.

Example 2.4 We have that i |= ( ⊤ ∧ ⊤) iff i is infinite. The left conjunct states that the interval of evaluation can be divided (is at least of size 2) and the right conjunct adds that an arbitrary division of the interval has at least one part which can be further divided. Together these conditions evidently exclude all finite intervals. Conversely, the formula is plainly true at every infinite interval. It follows, then, that i |= ( ⊥ ∨ ⊥) iff i is finite. (Note that while ⊥ is not equivalent to ¬⊤, still ⊥ is equivalent to ¬⊤.) Thus, relative to the class K fin , ( ⊥ ∨ ⊥) is valid and ( ⊤ ∧ ⊤) is contradictory.

Dropping superfluous operators

Often in logics certain syntactically given operators may be defined in terms of other syntactically given operators. It is clear that if we are exclusively interested in the expressive power of the logic TD, not all of its operators are needed. Obviously ∧ may be (contextually) defined in terms of ∨ and ¬, and may be (contextually) defined using and ¬: for any formulas φ and ψ, we have that (φ ∧ ψ) is equivalent to (¬φ ∨ ¬ψ), while φ is equivalent to ¬ ¬φ. Further, ⊤ may be defined in terms of ⊥, ∨ and ¬: indeed ⊤ is equivalent to (⊥ ∨ ¬⊥). From now on we will freely use the operators ∧, and ⊤construing the expressions in which they appear as abbreviations of expressions in which they do not appear. More interestingly, since we are considering finite intervals, even the universal negation ∼ becomes superfluous: it is definable from , ¬ and ⊥. In fact, over the class K fin any formula ∼φ is equivalent to the formula

(⊥ ∨ ψ φ ∨ ψ φ ),
where ψ φ := ( ¬⊥ ∧ ⊥ ∧ ¬φ). To see this, recall from Example 2.1 that the subformula (¬⊥∧ ⊥) is true at all and only intervals of size 1. Therefore, ψ φ states that the interval of evaluation is of size at least 2 and has a division all of whose parts are singletons, each singleton making φ false. The remaining two disjuncts of (⊥ ∨ ψ φ ∨ ψ φ ) cover the case that the interval is empty (in which case ∼φ is trivially true), and the case that the interval itself is a singleton and makes φ false.

From now on, in this paper we will take the 'official syntax' of TD[π] to be the one specified by the grammar φ ::

= p | ⊥ | ¬φ | (φ ∨ φ) | φ, with p ∈ π.

Characterization of the expressive power of TD

We will next present a characterization of the expressive power of TD on certain intervals (to be termed 'word intervals') using an independent tool from formal language theory, namely regular-like expressions.

Regular-like expressions

Let us define some basic notions. An alphabet is a finite (possibly empty) set Σ = {s 1 , . . . , s k }. Any finite string w = a 1 . . . a n of symbols a i from Σ is a word over Σ. The empty string (corresponding to the case that n = 0) is denoted by λ. We write Σ * for the set of all words over the alphabet Σ, and we write Σ + = Σ * \ {λ} for the set of all non-empty words over Σ. A (formal) language over Σ is any subset of Σ * , i.e., any set of words over Σ. If w = a 1 . . . a n and w ′ = b 1 . . . b m , their catenation ww ′ is the word

ww ′ = c 1 . . . c n+m , where c i = a i (1 ≤ i ≤ n) and c n+j = b j (1 ≤ j ≤ m).
We note that λw = w = wλ for all w ∈ Σ * . We say that v is a subword of w if there are u 1 , u 2 ∈ Σ * such that w = u 1 vu 2 . A factorization of a word w is any tuple w 1 , . . . , w n of words such that w = w 1 . . . w n ; a division of a word is its factorization into at least two factors all of which are non-empty. The length of a word w, in symbols |w|, is the number of symbols in w, when each symbol is counted as many times as it occurs. Given an alphabet Σ, the relative complement

L c of L is the set {w ∈ Σ * : w / ∈ L}. The catenation of languages L 1 and L 2 is the set L 1 • L 2 := {ww ′ : w ∈ L 1 and w ′ ∈ L 2 }, the catenation closure of the language L is the set L * := {w 1 . . . w n : w i ∈ L and n ≥ 0}, while the positive catenation closure of L is the set L + := {w 1 . . . w n : w i ∈ L and n ≥ 1}. Note that λ ∈ L + iff λ ∈ L.
Finally, we define a unary operation • on languages by setting L • = {w 1 . . . w n : w i ∈ L and w i = λ and n ≥ 2}. In the absence of better terminology, we refer to L • as the 2positive catenation closure of L; every element of L • has a division whose all parts belong to L. Note that while

L * \ ({λ} ∪ L) is included in L • , the converse need not hold: a word in L • may belong to L as well. For instance if L = {a, b, ab}, then ab ∈ (L • ∩ L).
Let an alphabet Σ be fixed, and let ∅ and 1 be symbols not in Σ. For the purposes of the present paper, the set RLE(Σ) of regular-like expressions over Σ is the smallest set containing all symbols from the set Σ ∪ {∅, 1} and closed under the following rules:6

• If r and s are in RLE(Σ), then so are (r ∪ s) and (r ∩ s) and (r • s).

• If r is in RLE(Σ), then so are r c and r * and r • .

The denotations [r] of regular-like expressions r are defined recursively as follows:

• [∅] = ∅ and [1] = {λ}. • [a] = {a} for all a ∈ Σ. • [r ∪ s] = [r] ∪ [s] and [r ∩ s] = [r] ∩ [s] and [r • s] = [r] • [s]. • [r c ] = [r] c and [r * ] = [r] * and [r • ] = [r] • .
If r is a regular expression over Σ, the elements of the set [r] are words over Σ; hence the denotations are languages over Σ. We refer to ∅, 1, c , * , • , ∪, ∩ and • as regular-like operators and to the correlated operations on languages as regular-like operations. The operators ∅ and 1 are nullary. We note that ∅ behaves, so to say, as a zero element w.r.t. catenation, while 1 can be said to behave as a unit element:

[∅ • r] = [∅] • [r] = [∅] = [r] • [∅] = [r • ∅] and [1 • r] = [1] • [r] = [r] = [r] • [1] = [r • 1].
If F is any subset of {∅, 1, ∪, ∩, •, c , * , • } and Σ is an alphabet, we write RLE(Σ, F) for the smallest set of regular-like expressions generated from the alphabet Σ by closing it under the operators from F. That is, RLE(Σ, F) consists of those regular-like expressions over the alphabet Σ in which no symbols from the set {∅, 1, ∪, ∩, •, c , * , • } \ F occur. By definition, the set RE(Σ) of regular expressions over Σ is the set

RLE(Σ, {∅, ∪, •, * }). A language L ⊆ Σ * is regular, if there is r ∈ RE(Σ) such that L = [r].
As a matter of fact, RLE(Σ, {∅, 1, ∪, ∩, •, c , * , • }) = RE(Σ), that is, the set of all regular expressions over Σ is closed under the operations 1, ∩, c and • : for every regular-like expression r over Σ there is an expression r ′ ∈ RE(Σ) such that [r] = [r ′ ]. It is well known -though not absolutely immediate -that the set RE(Σ) is closed under relative complement. This is easiest proven by making use of the connection of regular expressions to finite automata; cf., e.g., (Salomaa, 1981, Thm. 2.7). Intersection is, then, obviously definable from c and ∪. Further,

[1] = [∅ * ]. Finally, let r + := (1 c ∩ r * ). Thus, [r + ] = Σ + ∩ [r * ] = [r] + . We observe that [r • ] = [r] • = [r + ] • [r + ] = [r + • r + ].
Although the operators 1, ∩, c and • need not be separately given when considering regular expressions, there are sets F of regular-like operators for which the fragment RLE(Σ, F) is not closed under the operations expressed by some or all of the remaining regular-like operators. In what follows, we encounter some such sets.

Characterizing TD with regular-like operators

Let us agree on some definitions which enable us to make precise the connection between words and certain sorts of intervals; this connection is needed in order to formulate a characterization of TD in terms of certain regular-like expressions.

Given an alphabet Σ, we write π Σ for the set {p a : a ∈ Σ} of propositional atoms. By definition a word interval (relative to Σ) is an interval i = (T, <, V ) of finite size satisfying the following three conditions: (i) i belongs to the class K fin (π Σ ); (ii) for every t ∈ T there is a ∈ Σ such that p a ∈ V (t); and (iii) for any distinct a and b in Σ, there is no t ∈ T such that {p a , p b } ⊆ V (t). There is a straightforward correspondence between words and word intervals. On the one hand, every word interval (T, <, V ) induces a word w = a 1 . . . a n such that n = |T |, and if t i denotes the i-th element of T w.r.t. the order <, then a i is the unique a ∈ Σ such that p a ∈ V (t i ). The word w may be termed the word induced by i and denoted by w i . Conversely, for every word w = a 1 . . . a n over Σ, there is a unique associated word interval (T, <, V ) such that T = {1, . . . , n}, < is the relation 'strictly smaller than' among the elements of T , and for every 1 ≤ i ≤ n, we have p a ∈ V (t i ) iff a = a i . The word interval (T, <, V ) is called the word interval induced by the word w and denoted i w . We will denote by K word the class {i : there is an alphabet Σ and a word w ∈ Σ * such that i is isomorphic to i w } consisting of intervals isomorphic to intervals induced by words. Evidently K word is a proper subset of K fin . We write K word (π) for the class K word ∩ K fin (π). In what follows, for simplicity we allow writing w |= φ when what we mean is i w |= φ. No confusion should be possible, given the immediate correspondence between a word w and its induced word interval i w .

We will apply the following notion of translation to compare a logic defined on (structures encoding) words and a fragment of the set of all regular-like expressions.

Definition 3.1 (Translation, characterization) Let L be a logic evaluated on (structures encoding) words. Given an alphabet Σ and a set F of regular-like operators, let R = RLE(Σ, F). (a) We say that L is translatable into R, in symbols L ≤ R, if there is a (possibly non-computable) function f : L → R such that for all formulas φ ∈ TD and words w ∈ Σ * , we have:

w |= φ iff w ∈ [f (φ)]. (b) Conversely, we say that R is translatable into L, symbolically R ≤ L, if
there is a (possibly non-computable) function g : R → L such that for all regular-like expressions r ∈ R and words w ∈ Σ * , we have:

w ∈ [r] iff w |= g(r). (c) If L ≤ R
and R ≤ L, we write L = R and say that R characterizes L on the class of all (structures encoding) words.

We note that if R ≤ L, then every subset of Σ * denoted by an expression r ∈ R is definable by a formula φ of L in the sense that [r] = Mod(φ) ∩ K word (π Σ ). And if L ≤ R, then every subset of Σ * defined by some formula of L relative to the class K word is denoted by some expression of R.

We will now show that over word intervals, the logic TD is characterized by the set RLE(Σ, {1, ∪, • , c }). For simplicity, we will refer to this set of regular-like expressions as R 0 (Σ). Note that the operation * is definable in R 0 (Σ): for any expression r ∈ R 0 (Σ), we have

[r * ] = [1 ∪ r ∪ r • ]. Theorem 3.2 Let Σ be an alphabet. Then TD[π Σ ] = R 0 (Σ). Proof. We will first prove that R 0 (Σ) ≤ TD[π Σ ]. Define a map T : R 0 (Σ) → TD[π Σ ] as follows: T (1) = ⊥, T (a) = ( ¬⊥ ∧ ⊥ ∧ p a ), T (r c ) = ¬T (r), T (r ∪ s) = (T (r) ∨ T (s)), T (r • ) = T (r).
We proceed to show that for all words w ∈ Σ * and all r ∈ R 0 (Σ), we have w ∈ Let us still consider the expression r • . Suppose w ∈ [r • ]. Then for some n ≥ 2 there are words w i = λ such that w i ∈ [r] (with 1 ≤ i ≤ n) and w = w 1 . . . w n . By the inductive hypothesis, then, w i |= T (r) for every i. Since n ≥ 2, it follows that w |= T (r), where T (r) = T (r • ). The converse direction is proven similarly.

[r] iff w |= T (r). Now, w ∈ [1] iff w = λ iff w |= ⊥.
It remains to show that conversely, TD[π Σ ] ≤ R 0 (Σ). Let a map S : TD[π Σ ] → R 0 (Σ) be defined in the following way:

S(⊥) = 1, S(p a ) = (1 ∪ a ∪ a • ), S(¬φ) = S(φ) c , S(φ ∨ ψ) = (S(φ) ∪ S(ψ)), S( φ) = S(φ) • . We claim that for all words w ∈ Σ * and all formulas φ of TD[π Σ ], we have w |= φ iff w ∈ [S(φ)]. Note that w |= p a iff p a ∈ V (t) for all t ∈ i w iff for some n ≥ 0, we have that w = a 1 . . . a n , where a i = a for all 1 ≤ i ≤ n iff w ∈ [a * ], where [a * ] = [1 ∪ a ∪ a • ].
It is obvious that the claim holds for ⊥, as well as for negations, disjunctions, and formulas of the form φ.

By Theorem 3.2, instead of asking whether a formula φ ∈ TD[π Σ ] is true at an interval i ∈ K word (π Σ ), we may equivalently ask whether the word w i ∈ Σ * induced by the word interval i is an element of the language [S(φ)], where S is the map defined in the above proof. The size of the expression S(φ) is linearly bounded by the size of the input formula φ (i.e., by the number of occurrences of symbols it contains). Therefore, the model-checking problem of TD over word intervals can be reduced in linear time to the membership problem for R 0 . Since [START_REF] Stockmeyer | Word Problems Requiring Exponential Time[END_REF], we may conclude that the model-checking problem for TD over word intervals is solvable in EXPTIME.

[r • ] = [(1 c ∩ r * ) • (1 c ∩ r * )], it is possible to translate R 0 (Σ) = RLE(Σ, {1, ∪, • , c }) into RLE(Σ, {1, ∪, •, c , * }) in exponential time. As the membership problem for RLE(Σ, {1, ∪, •, c , * }) is contained in PTIME
Observe that we have not characterized the expressive power of TD on the full class K fin , only on its subclass consisting of word intervals. We will later see how our result can be utilized to prove general facts about the expressivity of TD on all intervals (Theorem 5.2). Further, the proof of Fact 6.6 will tell us that as a matter of fact, word intervals are in a precise sense representative of arbitrary intervals in connection with the logic TD.

Properties of TD

To illustrate features of TD, let us turn attention to two closure properties of definable classes of intervals: closure under 'multiplication' and closure under 'mirror images.' The logic TD lacks the former property but enjoys the latter.

Contradictory negation is not superfluous

It was seen above that the universal negation ∼ is superfluous as an operator of the logic TD when attention is restricted to the class K fin . We will now show that the contradictory negation ¬ is not superfluous: it cannot be defined from the other operators of this logic.7 This fact can be proven in a variety of ways. One way would be to work at the level of regular-like languages and show that RLE(Σ, {1, ∨, • , c }) = RLE(Σ, {1, ∨, • }). Then, making use of (the proof of) Theorem 3.2 which states that TD[π Σ ] = RLE(Σ, {1, ∨, • , c }), it could be shown that if negation was definable from the other connectives of TD, then also complementation could be defined using the operators 1, ∨ and • , which precisely is not possible. However, we will present a model-theoretic proof for the indispensability of negation.

Let us define the notion of multiplication of an interval. First, consider intervals i 1 = (T 1 , < 1 , V 1 ) and i 2 = (T 2 , < 2 , V 2 ), supposing their domains are disjoint. Their ordered sum is by definition the interval i 1 ⊕ i 2 = (T, <, V ), where

T := T 1 ∪ T 2 , < := < 1 ∪ < 2 ∪ (T 1 × T 2 ) and V := V 1 ∪ V 2 .
If the intersection of the domains T 1 and T 2 is non-empty, some standard operation is used to produce isomorphic copies i ′ 1 of i 1 and i ′ 2 of i 2 with disjoint domains, and we define i

1 ⊕ i 2 := i ′ 1 ⊕ i ′ 2 .
Recall from Note 1.1 that in the present paper we consider intervals in the 'internal sense.' The structure i 1 ⊕ i 2 as defined above is indeed an interval according to the definition provided at the beginning of Subsection 1.1. Thus, if for instance [[0, 1]] and [[2, 3]] are subintervals of an interval whose domain is the set of rational numbers and whose order is the order of rationals by magnitude, indeed [[0, 1]] ⊕ [[2, 3]] is an interval in the sense of the present paper, although it is not an interval in the external sense, since its domain [0, 1] ∪ [2, 3] of course is not inwards-closed.

If i is an interval, we define recursively the multiplication of an interval by a positive integer as follows: 1⊗i := i and (n+1)⊗i := (n⊗i)⊕i. We observe that n⊗i is an interval which results from having 'concatenated' the interval i with itself n times: i ⊕ . . . ⊕ i (n times). Note that n⊗Λ = Λ for all n. The intervals n⊗i are called multiples of the interval i and the operation of producing these intervals multiplication. Now, write TD(⊥, ∨, ) for the fragment of TD generated without negation. We show that any class defined by a formula of TD(⊥, ∨, ) is actually closed under arbitrary multiplications. Then we point out that not all classes definable in TD are closed in this way.

Lemma 4.1 Let φ be a formula of TDN(⊥, ∨, ). If i ∈ Mod(φ), then (n ⊗ i) ∈ Mod(φ) for all n ≥ 1.

Proof. The claim holds evidently for ⊥ and for atomic formulas p ∈ π. Assume, then, inductively that for all χ ∈ {φ, ψ} and all intervals j we have: if j |= φ, then (k ⊗ j) |= φ for all positive integers k. The claim holds for the formula (φ ∨ ψ). For, suppose i |= (φ ∨ ψ). So i |= φ or i |= ψ. By the inductive hypothesis, (n ⊗ i) |= φ for all n ≥ 1, or (n ⊗ i) |= ψ for all n ≥ 1. Thus, (n ⊗ i) |= (φ ∨ ψ) for all n ≥ 1. Suppose, then, that i |= φ, whence there is a division D = j 1 , . . . , j r with r ≥ 2 such that j m |= φ for all m. Let n ≥ 1 be arbitrary and consider the interval (n ⊗ i). This interval has by construction a partition into n subintervals i 1 , . . . , i n each of which is isomorphic to the interval i. Therefore the division D of i induces on each of these subintervals i j a division i 1 j , . . . , i r j such that every i m j is isomorphic to i m . Since φ holds at every i m , this formula also holds at every i m j . But then i 1 1 , . . . , i r 1 , . . . , i 1 n , . . . , i r n is a division of the interval (n ⊗ i) each of whose parts makes φ true. This means, again, that (n ⊗ i) |= φ. (Note that the inductive hypothesis is not needed in the case of formulas of the form φ.) Theorem 4.2 TD(⊥, ∨, ) < K fin TD.

Proof. Trivially TD(⊥, ∨, ) ≤ K fin TD. To see that the translatability does not hold in the converse direction, observe that using negation, the class of all intervals of size exactly 1 can be defined in TD: Mod(¬⊥ ∧ ⊥) = {i ∈ K fin : |i| = 1}. Obviously this class is not closed under multiplication. By Lemma 4.1, then, this class cannot be defined in TD(⊥, ∨, ). So TD cannot be translated into TD(⊥, ∨, ).

While the result of Theorem 4.2 might appear obvious, in some logics negation is actually not needed as a syntactically given connective, but can be expressed in terms of other operators. An example is furnished by the interval-based modal logic MLR (modal logic of regular expressions) studied in [START_REF] Hella | On the Existence of a Modal-Logical Basis for Monadic Second-Order Logic[END_REF]).8

Mirror images

We just saw that while the TD(⊥, ∨, ) definable classes of intervals are closed under multiplication, this is not so for all TD definable classes. We will now discern a closure property that TD has; it will be useful later in connection with certain expressivity considerations. If w = a 1 . . . a n is a word over an alphabet Σ, also the string a n . . . a 1 is a word over Σ, known as the mirror image of w and denoted mi(w). The empty word is its own mirror image. 9 More generally, if i = (T, <, V ) is any interval, we define its mirror image mi(i) to be the interval (T, < -1 , V ), where < -1 is the converse of the relation <. Note that mi(mi(i)) = i for all i. Let us show that if a class K is defined by a TD formula, then it is closed under taking mirror images.

Lemma 4.3 Let φ ∈ TD and i ∈ K fin be arbitrary. If i ∈ Mod(φ), then mi(i) ∈ Mod(φ).

Proof. We prove by induction on the formula φ of TD[π] the following more general claim: i ∈ Mod(φ) iff mi(i) ∈ Mod(φ), for all intervals i. (The more specific claim appearing in the statement of the lemma could not be proven by induction on φ for negated formulas.) The base case of formulas φ ∈ {⊥} ∪ π holds trivially. Suppose, then, inductively that for all χ ∈ {φ, ψ} and for all intervals j, we have: j |= χ iff mi(j) |= χ. It is immediate that the claim holds for formulas ¬φ and (φ ∨ ψ). In particular, i |= ¬φ iff i |= φ iff (ind. hyp.) mi(i) |= φ iff mi(i) |= ¬φ. Let us, then, consider the formula φ. Suppose first that i |= φ. So there is a division j 1 , . . . , j n of i with n ≥ 2 such that every part j i of the division satisfies: j i |= φ. By the inductive hypothesis, we have for every i that mi(j i ) |= φ. But then mi(j n ), . . . , mi(j 1 ) is a division of the interval mi(i) whose every part satisfies the formula φ. Therefore, we have mi(i) |= φ. The direction from mi(i) |= φ to i |= φ can be proven similarly. Lemma 4.3 marks an obvious limitation of TD as a temporal logic: it is characteristic of time that it has a 'direction,' but by the lemma, the logic TD does not capture this feature of time. Whenever a statement made using TD is true of an interval, it is also true of its mirror image. However, this does not diminish the interest of TD, since it is not even meant to be first and foremost a temporal logic, but a logic applicable when reasoning about durations and their divisions. And neither the notion of duration nor the notion of divisibility appears conceptually dependent on the direction of time. In Section 6 we will formulate an extension of TD in which direction of time can indeed be discussed.

Comparing TD with first-order logic

Next we wish to settle the question of how TD is related to first-order logic. Many instant-based modal logics are semantically fragments of FO. Relative to arbitrary modal structures, for example basic modal logic equals the bisimulation invariant fragment of FO. And relative to Dedekind-complete linear orders, the logic of Until and Since simply coincides with first-order logic. 10 In these cases the first-order translation of a modal formula φ is an FO formula ψ φ (x) of one free variable, x, such that ψ φ (x) uses in its vocabulary one binary predicate symbol, interpreted as the modal accessibility relation, and unary predicate symbols corresponding to the propositional atoms appearing in the modal formula. The question of translatability that interests us in the present paper in connection with our interval-based logic TD (and its extensions) is formulated in terms of FO sentences (instead of formulas with free variables), as follows.11

An interval i = (T, <, V ) with V of type T → P({p 1 , . . . , p n }) induces in a straightforward manner a first-order structure, namely the structure M i = (T, ≺ M i , P M i 1 , . . . , P M i n ) of vocabulary {≺, P 1 , . . . , P n } such that ≺ M i := < and P M i i := {t : p i ∈ V (t)}. Note that if i is empty, the induced first-order structure is the (n + 2)-tuple each member of which is the empty set. From now on, when considering abstract logics L (such as FO or MSO), we will write i |= ψ to indicate that the sentence ψ of L is true in the model M i . That is, we do not notationally distinguish intervals from their corresponding first-order structures. We proceed to pose the following question of translatability related to FO: is there for every formula φ ∈ TD a sentence ψ φ ∈ FO such that for all intervals i ∈ K fin , we have i |= φ iff i |= ψ φ ? This question is shown to receive a negative answer.

Henceforth, if an alphabet Σ is given, we write τ Σ for the vocabulary {P a : a ∈ Σ}∪{<}, where the P a are unary and < is binary. Taking advantage of our characterization result (Theorem 3.2), we take a detour via the fragment R 0 of regular-like expressions and prove that not all languages denoted by expressions in R 0 (Σ) are first-order definable, given that the size of the alphabet Σ is at least 2. By Theorem 3.2 it then follows that TD

[π Σ ] cannot be translated into FO[τ Σ ] whenever |Σ| ≥ 2.
The idea of proof is as follows. Given that {a, b} ⊆ Σ, we find a certain expression r 0 of R 0 (Σ) whose denotation contains in particular all words of the form (aabbaabbaabb) n with n ≥ 1, but no word of the form (aabbaabbaabb) n aabb with n ≥ 1. Then we show, using a simple Ehrenfeucht-Fraïssé game argument, that for any natural number n there is k n ≥ 1 such that the words (aabbaabbaabb) kn and (aabbaabbaabb) kn aabb cannot be distinguished by any FO sentence of quantifier rank at most n. It follows that the expression r 0 cannot be translated into FO. For if it could, let n 0 be the quantifier rank of its translation χ. Since χ translates r 0 , we have (aabbaabbaabb) kn 0 |= χ while (aabbaabbaabb) kn 0 aabb |= χ. Still the two words (aabbaabbaabb) kn 0 and (aabbaabbaabb) kn 0 aabb cannot be distinguished by any formula of quantifier rank at most n 0 and therefore not by χ. This is a contradiction, and we may conclude that indeed r 0 cannot be translated into FO.

In the proof presented below a specific regular-like expression r 0 is constructed; therefore the proof offers us (via a translation of R 0 into TD) a concrete example of a TD formula not translatable into FO. We take this to be a sufficient motivation for formulating the proof as we do. In Section 7 we will note that the result could be alternatively approached with reference to certain results known from the literature that characterize FO in terms of regular-like expressions.

We recall that [r * ] is definable as [1 ∪ r ∪ r • ], for any r in R 0 . To facilitate the discussion, let us agree on writing r * for the 'dual' of the expression r * , that is, for the expression r c * c . Hence the set [r * ] contains exactly those words whose every factorization has at least one factor that belongs to the denotation of r.

Lemma 5.1 Let |Σ| ≥ 2. There is no map f : R 0 (Σ) → FO[τ Σ ] such that for all expressions r ∈ R 0 (Σ) and all words w ∈ Σ * , we have:

w ∈ [r] iff w |= f (r).
2011). If we agree to confine attention to intervals defined in terms of bounds, like [ [t, t ′ ] ] or ((t, t ′ ] ], then interval-based modal logics can be understood as 2-dimensional modal logics. However, if we allow any inwards-closed set to determine an interval, this is no longer the case. For example, the subinterval of an interval (Q, <, V ) determined by the set {x : 2 < x 2 < 5} cannot be defined in terms of bounds.

Proof. We single out an expression r 0 witnessing that no translation of R 0 (Σ) into FO[τ Σ ] exists. First, define the expressions r 1 , r 2 , r 3 and r 4 as follows:

• r 1 := ((a • ∪ b) * ∩ a * c ∩ b * c ) and r 2 := ((b • ∪ a) * ∩ a * c ∩ b * c );
• r 3 := ((a∪b∪r 1 ) * ∩a c ∩b c ∩1 c ∩(a∪b) * ) and r 4 := ((a∪b∪r 2 ) * ∩a c ∩b c ∩1 c ∩(a∪b) * ).

We observe that [r 1 ] consists of those words over the alphabet {a, b} which contain as a subword at least one of the words aab or baa. So there are no words of size less then 3 in [r 1 ], and the only words of size 3 in it are aab and baa. Similarly, [r 2 ] consists of the words over {a, b} containing bba or abb as a subword, and the shortest words in [r 2 ] are bba and abb. Let us, then, consider the expressions r 3 and r 4 . First, we note that in [(a ∪ b ∪ r 1 )] there are no words whose size equals 2. For, in [a] and in [b] there are only words of size 1, and in [r 1 ] only words of size at least 3. Similarly, in [(a ∪ b ∪ r 2 )] there are no words of size 2. Which are the words in the denotation of [r 3 ], then? It is explicitly said that [r 3 ] ⊆ {a, b} * \ {λ, a, b}. In addition it is said that every factorization of a word in [r 3 ] has some part belonging to the denotation of (a ∪ b ∪ r 1 ). This rather strong condition excludes a whole lot of words. Indeed, it excludes all words of even size: any such word has a factorization each of whose parts is of size exactly 2, but there is no word of size 2 in [(a∪b∪r 1 )]. What about words of odd size, then? In particular, each word of size 2n+3 has n+1 factorizations into factors of which exactly one is of size 3 and the rest are of size 2. For each of those factorizations the factor of size 3 must be in [r 1 ], i.e., must either equal aab or else equal baa. This again imposes a rather strong restriction on what sort of words of odd size are accepted by the expression (a∪b∪r 1 ) * . A moment's reflection reveals that -apart from a and b which are excluded from [r 3 ] anyway -the odd words in [(a ∪ b ∪ r 1 ) * ] are as follows: aab, baa; aabaa, baaab; aabaaab, baaabaa; aabaaabaa, baaabaaab; etc. Similarly we may observe that the set [r 4 ] consists of the words bba, abb; bbabb, abbba; bbabbba, abbbabb; bbabbbabb, abbbabbba; etc. Consider, then, words w satisfying the following three conditions: (1) w is the result of concatenating some finite number of words in [r 3 ], ( 2 2), the set of words considered is actually a subset of {aab, baa, baaab} * . Namely, all words in [r 3 ] except for aab, baa and baaab contain at least one occurrence of b which is neither immediately followed nor immediately preceded by another occurrence of b, and which is neither in the beginning nor in the end of the word in question. Therefore, no word which contains as a subword a word from the set [r 3 ] \ {aab, baa, baaab} may satisfy condition (2). Now, in the set {aab, baa, baaab} * , there is only one word which satisfies both conditions (2) and (3), namely aabbaa. In particular, the shortest word satisfying these conditions and containing the word baaab as a subword, namely aabbaaabbaa can be divided into 5 parts each belonging to [a • ] or to [b • ] (hence a fortiori the number of such parts is at least 4). Write, then,

r 5 := r 3 * ∩ (a • ∪ b • ) * ∩ (a • ∪ b • ) ••c . So we note that [r 5 ] = {aabbaa}. Similarly, letting r 6 := r 4 * ∩ (a • ∪ b • ) * ∩ (a • ∪ b • ) ••c
, we have that [r 6 ] = {bbaabb}. Finally, put r 0 := (r 5 ∪ r 6 ) * . We observe that the language [r 0 ] contains in particular all words of the form (aabbaabbaabb) n with n ≥ 1, but it contains no word of the form (aabbaabbaabb) n aabb.

Given n ≥ 1, let m and k n be the unique numbers such that m ∈ {4, 8} and 4 • 2 n-1 + m = 12 • k n . Further, let k 0 := k 1 . We proceed to show that for every n < ω, (the firstorder structures encoding) the words (aabbaabbaabb) kn and (aabbaabbaabb) kn aabb are FO equivalent up to quantifier rank n. 12 Consider the longer (shorter) word as factored into 3 • k n + 1 (respectively, 3 • k n ) blocks aabb of 4 symbols. Now, a moment's reflection shows that in the n-round Ehrenfeucht-Fraïssé game played relative to the words (aabbaabbaabb) kn and (aabbaabbaabb) kn aabb, an optimal strategy for Spoiler consists of letting him choose successively the following elements of the longer word: the last symbol of block 2 0 , the last symbol of block 2 1 , and so on, until the last symbol of block 2 n-1 . A strategy allowing Duplicator to win against this strategy of Spoiler's in the relevant Ehrenfeucht-Fraïssé game consists simply of choosing successively the last symbol of block 2 0 , the last symbol of block 2 1 , and so on, until the last symbol of block 2 n-1 . Since Spoiler's strategy is optimal, this strategy is winning for Duplicator. If the (n + 1)-th move was still available, Spoiler could choose the last symbol of the block 3 • k n + 1 from the longer word and to this move Duplicator could not respond without immediately losing, given that she would have already chosen the last symbol of the block 2 n-1 from the shorter word before. (If Duplicator applied a different strategy against Spoiler's first n moves, she might survive even for more than n rounds. What is relevant here is only that there is a strategy for her to survive at least n rounds.)

We are in a position to prove that the expressive powers of the logics TD and FO are incomparable. If π is a set of atoms, let us write τ π for the vocabulary {P q : q ∈ π} ∪ {<}, where the P q are unary.

Theorem 5.2 Let |π| ≥ 2. Over the class K fin , TD[π] || K fin FO[τ π ].
Proof. Fix a set π of atoms with {p a , p b } ⊆ π and let Σ be the corresponding alphabet, with {a, b} ⊆ Σ. Let us first show that TD

[π] ≤ K fin (π) FO[τ π ]. Suppose for contradiction that TD[π] ≤ K fin (π) FO[τ π ], i.e.
, that there is a function f : TD[π] → FO[τ π ] such that for all i ∈ K fin (π) and all φ ∈ TD[τ π ], we have i |= φ iff i |= f (φ). Consider the expression r 0 of alphabet Σ singled out in the proof of Lemma 5.1, and let φ := T (r 0 ) be the translation of r 0 into TD[π] with T as specified in the proof of Theorem 3.2. Hence w ∈ [r 0 ] iff w |= φ, for all words w over Σ. Let ψ φ be a first-order translation of φ, existing by the assumption that TD TD[π]. This rather obvious fact can be proven as follows. Let χ be the following FO sentence: ∃x∃y(P a x ∧ P b y ∧ x < y). Consider the two simple words ab and ba over the alphabet Σ. Now, ab |= χ but ba |= χ. Yet ba = mi(ab), so if FO[τ π ] was translatable into TD[π], by Lemma 4.3 we would have 12 In order to make sure that Duplicator will be able to make at least n moves in the Ehrenfeucht-Fraïssé game of n rounds, we want that there are at least 2 n-1 blocks aabb of 4 symbols in the longer word. Further, since we also want the word to belong to [(r5 ∪ r6) * ], we must make sure its size is divisible by 12. As a matter of fact the only relevant numbers to add to the quantity 4 • 2 n-1 are indeed 4 and 8. The number 4 • 2 n-1 + 0 is not divisible by 3 and so not by 12. Also, no odd number added to 4 • 2 n-1 can yield a number divisible by 12. Finally, out of the non-negative integers less than 12 the remaining candidates -besides 4 and 8 -namely 2, 6, and 10 are not possible since 2 • 2 n-1 + 1 and 2 • 2 n-1 + 3 and 2 • 2 n-1 + 5 are odd and therefore not divisible by 6.

[π] ≤ K fin FO[τ π ]. So for all words w over Σ, we have w |= φ iff w |= ψ φ . Therefore, w ∈ [r 0 ] iff w |= ψ φ . It follows that the language [r 0 ] is first-order definable, which is impossible in view of Lemma 5.1. It remains to show that conversely, FO[τ π ] ≤ K fin (π)
in particular that either χ is true at both words ab and ba, or else χ is false at both of them. It follows that χ has no translation into TD[π].

Extending TD: and next

We have seen that TD is not able to describe order-related properties of temporal flows. In order to make it possible to speak of properties of intervals which are not 'direction invariant,' we introduce a new connective and next and extend the syntax of the logic TD by this connective, obtaining a logic to be dubbed TDN.

Syntax and semantics of TDN

The syntax of TDN[π] is given by the following grammar:

φ ::= p | ⊥ | ¬φ | (φ ∨ φ) | φ | (φ and next φ),
with p ∈ π. The semantics of the novel binary connective and next is given by the following clause: i |= (φ and next ψ) iff there are intervals i 1 and i 2 such that i = i 1 ⊕ i 2 and i 1 |= φ and i 2 |= ψ. Observe that this definition allows the case that one or both of the intervals i 1 and i 2 are empty. For example, if Λ |= φ and i |= ψ, then i |= (φ and next ψ), where i = Λ ⊕ i. So, (φ and next ψ) is true at i iff one of the following conditions hold: i can be split into two non-empty pieces of which the earlier one makes φ true while the later one makes ψ true, or exactly one of φ ψ is true at the empty interval while the other is true at i, or i itself is empty and both φ and ψ are true at it. The semantic relationship between the operators and and next can be explicated as follows. Given a formula ψ of TDN, let us define: (ψ and next ψ) 0 := (ψ and next ψ) and (ψ and next ψ) n+1 := ((ψ and next ψ) n and next ψ). The operator is the 'closure' of and next in the following sense: i |= φ iff there is n ≥ 0 such that i |= (φ ∧ ¬⊥) and next (φ∧¬⊥)

n . (We recall that the semantics of calls for splitting the interval of evaluation into non-empty pieces, hence the conjunct ¬⊥.) This does not mean, of course, that we can dispense with as soon as and next is available in our language. Indeed we cannot express in terms of the other connectives of TDN. This fact may appear rather obvious; we will see a proof later (Corollary 7.3). It is even easier to get convinced of the fact that the availability of and next indeed adds to the expressive power of TD. Actually we can drop the restriction on the size of the set π in the statement of Theorem 6.1. In Section 7 we discern a certain formula (u and next u) of TDN[π] with |π| = 0; this formula is true at all and only intervals of size 2. From Fact 7.4 it will follow that the formula in question cannot be translated into TD.

Characterizing TDN

In Theorem 3.2 we characterized the expressive power of TD on the class K word by using the regular-like operators 1, ∨, • and c . Now, TDN can actually be characterized by regular operators. We recall that by definition the set RE(Σ) of regular expressions over Σ equals RLE(Σ, {∅, ∨, * , •}). Note that in this case the operator for relative complement (viz. c ) is not among the given operators. Theorem 6.2 Let Σ be an alphabet. Then TDN[π Σ ] = RE(Σ).

Proof. The proof proceeds like that of Theorem 3.2. For the direction from right to left, define a map T : RE(Σ) → TDN[π Σ ] as follows:

T (∅) = ¬⊤, T (a) = ( ¬⊥ ∧ ⊥ ∧ p a ), T (r ∪ s) = (T (r) ∨ T (s)), T (r * ) = (⊥ ∨ T (r) ∨ T (r)), T (r • s) = (T (r)
and next T (s)). Plainly the map T satisfies w ∈ [r] iff w |= T (r), for all words w ∈ Σ * and all expressions r ∈ RE(Σ). As regards the converse direction, recall that in RE(Σ) we may define the operation + satisfying [r + ] = [r] \ {λ} and use it to define the operation We may note that in the above proof the size of the expression S(φ) is linear in the size of the input formula φ. Therefore there exists a linear time reduction of the modelchecking problem of TDN over word intervals into the membership problem for regular expressions; the latter problem is NLOGSPACE complete [START_REF] Jiang | A Note on the Space Complexity of Some Decision Problems for Finite Automata[END_REF].

• , because [r • ] = [r + • r + ]. Recall also that RE(Σ) is closed under relative complement. Now, define a map S : TDN[π Σ ] → RE(Σ) by setting S(⊥) = ∅ * , S(p a ) = a * , S(¬φ) = S(φ) c , S(φ ∨ ψ) = (S(φ) ∪ S(ψ)), S( φ) = S(φ) • , S(φ and next ψ) = (S(φ) • S(ψ)).

Comparing TDN with MSO

In Section 5 we saw that TD cannot be translated into FO. Because TD is a fragment of TDN, it of course follows that neither can TDN. On the other hand, by inspecting the clauses defining the semantics of TDN we see that it can be translated into monadic second-order logic. After explaining how this translation works (the proof of Fact 6.3), we will pose the question: which fragment of MSO does TDN capture?

Let us first agree on some abbreviations. Given a vocabulary containing the binary relation symbol < interpreted as an irreflexive linear order, we write x ≤ y for (x < y ∨x = y), min(x) for ∀y(x ≤ y) and max(x) for ∀y(y ≤ x). We abbreviate by not-betw(x, y, X) the sentence ¬∃z(Xz ∧ x < z ∧ z < y), saying that there is no element of X between x and y. Observe that this is the case in particular when x = y, and likewise when x < y and y = min(X). We write succ(x, y, X) for the sentence (Xx ∧ Xy ∧ x < y ∧ notbetw(x, y, X)), stating that x and y are successive elements of X, i.e., elements of X between which there is no further element of X (though there might be elements between them which are not in X). Finally, if Φ is an MSO sentence, let Φ [x,y] and Φ (x,y] be the results of relativizing all first-order quantifiers of Φ to the set [x, y] := {z : x ≤ z ≤ y} and to the set (x, y] := {z : x < z ≤ y}, respectively. Such relativizations may be defined recursively. For example, (∃zΨ) [x,y] := ∃z(x ≤ z ∧ z ≤ y ∧ Ψ [x,y] ). Fact 6.3 TDN ≤ K fin MSO.

Proof. Let π be any set of atoms. Let us define a map F : TDN[π] → MSO[τ π ] recursively as follows. Put F (⊥) := ∀x(x = x) and F (p i ) := ∀xP i x. Assume, then, that F has already been defined on φ and on ψ. Let F (¬φ) = ¬F (φ) and F (φ∨ψ) = (F (φ)∨F (ψ)). Finally, define F ( φ) and F (φ and next ψ) by putting [x,y] ) ∧ ∀x∀y(succ(x, y, X) → F (φ) (x,y] ));

• F ( φ) := ∃X∃x(Xx ∧ max(x) ∧ ∃y∃z(min(y) ∧ Xz ∧ z = x ∧ (Xy → y = z) ∧ not-betw(y, z, X) ∧ F (φ)
• F (φ and next ψ) = (χ 0 ∨ ∃x∃y∃z min(x) ∧ y ≤ z ∧ max(z) ∧ (χ 1 ∨ χ 2 ) ),
where χ 0 := ∀x(x = x) ∧ F (φ) ∧ F (ψ); χ 1 := F (φ) (x,x] ∧ F (ψ) [x,z] ; and χ 2 := F (φ) [x,y] ∧ F (ψ) (y,z] ). Here the subformula χ 0 corresponds to the case that the relevant factorization i 1 , i 2 of the interval i of evaluation satisfies i 1 = Λ = i 2 , the formula χ 1 corresponds to the case that i 1 = Λ and i 2 = i, while χ 2 covers the remaining two cases. It is straightforward to prove by induction on the structure of the TDN[π] formula φ that indeed F provides a translation: for every interval i ∈ K fin (π), we have that F (φ) is an MSO[τ π ] sentence satisfying i |= φ iff i |= F (φ).

We wish to identify the fragment of MSO captured by TDN relative to the class K fin . Let us first think of word intervals (rather than arbitrary intervals). We will utilize the following well-known result which ties together regular languages, word intervals and monadic second-order logic. Proposition 6.4 [START_REF] Büchi | Weak Second-Order Arithmetic and Finite Automata[END_REF] Let Σ be an alphabet and let L ⊆ Σ * . The language L is regular if and only if there is an MSO[τ Σ ] sentence Φ such that L = {i ∈ K word (π Σ ) : i |= Φ}. That is, over K word we have RE = MSO. 13Precisely those languages are denoted by a regular expression, then, that are defined by some MSO sentence. It turns out that on the class K word , TDN is very expressive. Actually it captures the whole of MSO. Given a set π of atoms, write Σ π for the alphabet {a p : p ∈ π}. Lemma 6.5 TDN = K word MSO.

Negation in TDN

We saw in Subsection 4.1 that in TD, the contradictory negation ¬ could not be dispensed with without loss of expressive power. Is ¬ perhaps superfluous in TDN? Given the fact that TDN is characterized by regular expressions in which the operation of relative complement is indeed superfluous, one might surmise that the answer is in the affirmative. However, the situation is more nuanced. Write TDN(⊥, ∨, , and next) for the logic resulting from not allowing the use of ¬ in TDN. We may first observe that in any case the proof of Theorem 6.2 does not allow inferring that TDN can be translated into TDN(⊥, ∨, , and next) over K word . This would be possible if in the formulas belonging to the image of the map T : RE(Σ) → TDN[π Σ ], there appeared no negation signs. However, negation has been used to translate ∅ and to translate the symbol a of the alphabet Σ. Of course, this does not yet prove that we could not have avoided using negation in the translation. Could we? That the answer is negative is entailed by the following closure result pertaining to TDN(⊥, ∨, , and next). The result is a weakened version of Lemma 4.1, which was shown to hold for TD(⊥, ∨, ). This lemma cannot as such be extended to TDN(⊥, ∨, , and next). If, for example, i 0 is an interval consisting of two instants, the earlier making p true but q false and the later making q true but p false, the formula (p and next q) holds at i 0 , but does not hold at any multiple (n ⊗ i 0 ) of i 0 with n ≥ 2. Lemma 6.8 Let φ be a formula of TDN(⊥, ∨, , and next). If Mod(φ) ∩ {Λ} = ∅, then for every k < ω there is in Mod(φ) an interval of size greater than k.

Proof. There is nothing to prove if φ = ⊥, since in that case Mod(φ) = {Λ}. If φ is an atom, the claim holds trivially: then Mod(φ) contains an interval of every finite size. Suppose, then, inductively that if χ ∈ {φ, ψ} and Mod(χ)∩{Λ} = ∅, then in Mod(χ) there is no interval with a maximal size. We consider cases. (1) If i = Λ and i |= (φ ∨ ψ), there is χ ∈ {φ, ψ} such that i |= χ. For every k < ω there is by the inductive hypothesis an interval j with |j| > k such that j |= χ. So j |= (φ∨ψ). ( 2) If i = Λ and i |= (φ and next ψ), there are intervals i 1 and i 2 such that i 1 ⊕ i 2 = i and i 1 |= φ and i 2 |= ψ, and at least one of i 1 and i 2 is distinct from Λ. Suppose i 1 = Λ (the case that i 2 = Λ can be dealt with similarly). Let k < ω be arbitrary. Then by the inductive hypothesis there is an interval j with |j| > k such that j |= φ. Thus, the formula (φ and next ψ) is true at (j ⊕ i 2 ), where

|(j ⊕ i 2 )| > k. (3) Finally, if i |= φ, there is a division i 1 , . . . , i n with n ≥ 2 such that i m = Λ and i m |= φ for all 1 ≤ m ≤ n.
Let k < ω be arbitrary. Define j := (k + 1) ⊗ i 1 , whence j is an ordered sum of k + 1 of intervals each of which is isomorphic to i 1 . The terms of the ordered sum induce a division j 1 , . . . , j k+1 of j. Since i 1 |= φ and every j i is isomorphic to i 1 , we have j i |= φ for all 1 ≤ i ≤ k + 1. Further, |j| > k since i 1 = Λ. Now, evidently j |= φ. (Observe that in the case for the inductive hypothesis was not needed.) Call a formula φ strongly satisfiable if there is at least one interval i = Λ such that i |= φ. Call a set S of non-negative integers a spectrum of a formula φ if S = {|i| : i ∈ Mod(φ)}. By Lemma 6.8, every strongly satisfiable formula φ of TDN(⊥, ∨, , and next) has an infinite spectrum. We are in a position to see that TDN(⊥, ∨, , and next) is not closed under negation. Corollary 6.9 TDN(⊥, ∨, , and next) < K fin TDN.

Proof. Trivially TDN(⊥, ∨, , and next) ≤ K fin TDN. To see that the converse does not hold, let π be a set of atoms and suppose for contradiction that TDN[π] ≤ K fin (π) TDN(⊥, ∨, , and next) [π]. Recall that the spectrum of the TDN formula (¬⊥ ∧ ⊥) is {1}. A fortiori its spectrum is finite. By assumption this formula has a translation into TDN(⊥, ∨, , and next)[π], call it χ. From Lemma 6.8 it follows that the spectrum of χ is infinite. This is a contradiction in view of χ being a translation of (¬⊥ ∧ ⊥).

So it has turned out that negation is not superfluous in TDN. On the other hand, as witnessed by the proof of Theorem 6.2 (combined with Fact 6.6), only a very limited use of negation is needed to reach the full expressive power of TDN over the class K fin . Let us formulate this observation precisely. Let a set π = {p 1 , . . . , p n } of atoms be fixed. A Boolean combination of the atoms p 1 , . . . , p n is any conjunction p

f (1) 1 ∧ . . . ∧ p f (n) n
, where f is a function of type {1, . . . , n} → {0, 1} and p 1 i = p i and p 0 i = ¬p i . Write TDN 0 [π] for the fragment of TDN[π] syntactically generated by the following grammar:

φ ::= ⊥ | T | (u ∧ β) | (φ ∨ φ) | (φ and next φ) | φ,
where β is a Boolean combination of atoms in π, T is short for (¬⊥∧⊥), and u abbreviates (¬⊥ ∧ ⊥). The letter 'u' is reminiscent of the fact that the formula in question is true precisely at unit intervals (i.e., intervals of size 1). In TDN 0 , the occurrences of ¬ are very restricted indeed: they only appear in formulas of the forms ¬⊥ and ((¬⊥ ∧ ⊥) ∧ 1≤i≤n p f (i) i

); recall here that and ∧ are abbreviations, themselves defined using negation.

Theorem 6.10 Over the class K fin , TDN 0 = TDN = MSO.

Proof. Let π = {p 1 , . . . , p n } be a set of atoms. Let us show that over the class K fin (π), we have TDN 0

[π] ≤ TDN[π] ≤ MSO[τ π ] ≤ TDN 0 [π]
. Now, the first inclusion is trivial and the second holds by Fact 6.3. For the third inclusion, let Ψ be any MSO[τ π ] sentence. Applying Fact 6.6(2.a) we obtain a sentence Φ Ψ ∈ MSO[τ w(π) ] such that i |= Ψ iff w(i) |= Φ Ψ , for all i ∈ K fin (π). By the proof of Theorem 6.2 (and applying Proposition 6.4), there is a formula χ of TDN[w(π)] which is generated from formulas of the forms ⊥, T and (u ∧ p) by using the connectives ∨, and and next, and which satisfies w(i) |= Φ Ψ iff w(i) |= χ, for all i ∈ K fin (π). Then, utilizing Fact 6.6(1.b), we may conclude that there is a formula θ χ of TDN[π] which satisfies w(i) |= χ iff i |= θ χ , for all i ∈ K fin (π), and which differs from χ only in that in place of the atoms of χ there appear in θ χ Boolean combinations of atoms from the set π. But this means that θ χ is actually a formula of TDN 0 [π]. To summarize, for all i ∈ K fin (π) we have i |= Ψ iff i |= θ χ . Since Ψ ∈ MSO[τ π ] was assumed to be arbitrary, we may conclude that MSO

[τ π ] ≤ K fin (π) TDN 0 [π].

Conclusion

We have studied the logic of time division (TD) on intervals of finite size. This logic was characterized over the class K word by using the regular-like operators 1, ∨, • and c . Some of its model-theoretic properties were discussed. This logic was shown to be incomparable with first-order logic for its expressive power. The logic TD was extended to the logic TDN by making available the additional connective and next. It turned out that TDN is very expressive: it has the full expressive power of monadic-second order logic over the class K fin . We remarked that negation (¬) cannot be dropped from the syntax of TDN without loss in expressivity. However, it was observed that a very limited use of negation suffices. This observation was made explicit by discerning the expressively equivalent fragment TDN 0 of TDN. Let us conclude with a couple of remarks and systematic observations.

FO as a fragment of TDN

We already mentioned Büchi's result which establishes a connection between regular expressions and MSO. There is a corresponding result about FO. The set SFRE(Σ) of star-free regular expressions over an alphabet Σ is by definition the set RLE(Σ, {∅, ∪, •, c }).

Proposition 7.1 [START_REF] Mcnaughton | Counter-Free Automata[END_REF] Let Σ be an alphabet and let L ⊆ Σ * . The language L is denoted by a star-free regular expression if and only if there is an

FO[τ Σ ] sentence φ such that L = {i ∈ K word (π Σ ) : i |= φ}. That is, SFRE = FO. 14
Write TDN(⊥, ∨, and next, ¬) for the logic resulting from TDN when the use of is disallowed. Making use of Proposition 7.1, it can be seen that this logic coincides in expressive power with FO over K fin . Observe that in TDN(⊥, ∨, and next, ¬) the formula (¬⊥ ∧ ¬(¬⊥ and next ¬⊥)) defines the class of all intervals of size 1. In particular the subformula ¬(¬⊥ and next ¬⊥)) says that the interval cannot be divided into two nonempty parts; the only intervals meeting this condition are those whose size is at most 1.

Here we obviously cannot make use of the formula ⊥ which is indeed equivalent to the formula ¬(¬⊥ and next ¬⊥), since is not syntactically available.

Theorem 7.2 TDN(⊥, ∨, and next, ¬) = K fin FO.

Proof. Let π be any set of atoms. It is immediate that TDN(⊥, ∨, and next, ¬)[π] can be translated into FO[τ π ], cf. the proof of Fact 6.3. For the converse direction, let us first define a map T : SFRE(Σ π ) → TDN(⊥, ∨, and next, ¬)[π] recursively as follows:

T (∅) = ¬⊤, T (a p ) = ((¬⊥ ∧ ¬(¬⊥ and next ¬⊥)) ∧ p), T (r ∪ s) = (T (r) ∨ T (s)), T (r • s) = (T (r) and next T (s)), T (r c ) = ¬T (r). Clearly the map T satisfies i ∈ [r] iff i |= T (r)
, for all i ∈ K word (π) and all expressions r ∈ SFRE(Σ π ). Applying first Fact 6.6(2.a), then Proposition 7.1, then using the translation T , and then applying Fact 6.6(1.b), we find for every φ ∈ FO[τ π ] a formula χ ∈ TDN(⊥, ∨, and next, ¬)[π] such that for every i ∈ K fin (π), we have i |= φ iff i |= χ.

It is worth noting that Proposition 7.1 suggests an alternative way of proving that TD ≤ FO (cf. Theorem 5.2). This negative result was established above by first proving that R 0 cannot be translated into FO (Lemma 5.1) and then resorting to the fact that TD = R 0 . Instead, we could attempt to prove -remaining at the level of regular-like expressions -that there is an expression r ∈ R 0 such that [r] is not denoted by any expression of SFRE. By Proposition 7.1 and Theorem 3.2 it would then follow that TD cannot be translated into FO over the class K word and therefore not, a fortiori, over K fin .

Corollary 7.3 Over the class K fin , we have:

Open questions

Concerning the expressive power of the logic of time division, we have seen that semantically it determines, relative to K fin , a fragment of MSO which does not cover FO but which is also not included in FO. We leave it as a question for future research to characterize the fragment of MSO determined by the logic TD in model-theoretic terms. As a first guess, one might be tempted to think, wrongly, that TD coincides semantically with the fragment of MSO consisting of sentences Φ that are invariant under mirror images, i.e., that satisfy the following: if i |= Mod(Φ), then mi(i) ∈ Mod(Φ). By Lemma 4.3 we do know that all MSO translations of TD formulas are indeed invariant under mirror images, but as a matter of fact it is not the case that conversely, every MSO sentence (or even every FO sentence) invariant under mirror images is equivalent to a TD formula. For a counterexample, consider the TDN[∅] formula φ := (u and next u), satisfying Mod(φ) = {i ∈ K fin : |i| = 2}; recall that by definition u is the formula (¬⊥ ∧ ⊥). The MSO translations of this formula are obviously invariant under mirror images: the mirror image of any interval of size 2 is likewise an interval of size 2. The following fact implies that φ is not translatable into TD.15 Fact 7.4 Let π be any set of atoms. There is no formula χ ∈ TD[π] such that Mod(χ) ∩ K fin (π) = {i ∈ K fin (π) : |i| = 2}.

Proof. We will first prove the claim in the case π = ∅ and then generalize it to pertain to all sets of atoms. For convenience, let us use the syntax where and ∧ are available as primitives. Consider TD[∅] formulas in negation normal form, i.e., suppose they are written in a form in which the negation symbol may only appear in front of ⊥. We prove the following claim: if a formula χ of TD[∅] is true at an interval of size 2, then it is true at an interval of size 3. Once this is shown, it immediately follows that the statement of the Fact holds in the case π = ∅. If n < ω, write K n (π) for the set {i ∈ K fin (π) : |i| = n}. Now, the spectra of the formulas ⊥ and ¬⊥ are {0} and ω \ {0}, respectively, so they satisfy the claim. Note that for every n, the set K n (∅) contains, up to isomorphism, only one interval. If ψ is true at an interval i ∈ K 2 (∅), then there are i 1 , i 2 ∈ K 1 (∅) with i 1 ⊕ i 2 = i such that i j |= ψ for j := 1, 2. But then the interval i 1 ⊕ i 2 ⊕ i 2 belongs to K 3 (∅) and makes ψ true. Further, if ψ is true at an interval i ∈ K 2 (∅) and i = i 1 ⊕ i 2 with i 1 , i 2 ∈ K 1 (∅), there is, by the semantics of , a number l ∈ {1, 2} such that i l |= ψ. Let j := i 1 ⊕ i 2 ⊕ i 1 if l = 1 and let j := i 2 ⊕ i 1 ⊕ i 2 if l = 2. By the construction of j we have that j ∈ K 3 (∅) and j |= ψ. We will need the inductive hypothesis only to deal with disjunctions and conjunctions: indeed, suppose inductively that for θ ∈ {ψ, χ} we have: if θ is true at some i ∈ K 2 (∅), then θ is true at some j ∈ K 3 (∅). The claim follows trivially for disjunction. Suppose, then, that i |= (ψ ∧ χ) with i ∈ K 2 (∅). By the inductive hypothesis there are intervals j 1 and j 2 in K 3 (∅) such that j 1 |= ψ and j 2 |= χ. Since the intervals in K 3 (∅) are pairwise isomorphic, it follows in particular that j 1 |= χ and so j 1 |= (ψ ∧ χ).

Having proven the statement of the Fact for the empty set of atoms, let π = ∅ be arbitrary. Suppose for contradiction that there is a formula θ ∈ TD [π] in which at least one atom appears and which satisfies: Mod(θ)∩K fin (π) = K 2 (π). Let us say that (T, <, V ) is an f-interval if V (t) = ∅ for every t ∈ T , i.e., it renders all atoms false at every instant. For every n there is, up to isomorphism, exactly one f -interval in K n (π). Let θ ′ be the result of replacing in θ every atom by the formula ⊥. If i is an f -interval and i ∈ K n (π), we clearly have that i |= θ ′ iff n = 2. Since θ ′ contains no atoms, its truth-value must be the same at any two intervals which differ only in their valuations. Therefore we have for all intervals i in K n (π): i |= θ ′ iff n = 2. But this means that we have found a formula of TD[∅], namely θ ′ , which satisfies Mod(θ ′ ) = {i ∈ K fin : |i| = 2}. This is a contradiction in view of what already proven. By Fact 7.4, then, closure under mirror images does not suffice to yield a modeltheoretic characterization of the fragment of MSO captured by TD. This characterization issue remains open. Among further questions for future research we can mention the following. The satisfiability problem of the logic TD is decidable over K fin , since MSO-SAT is decidable over K fin and there is a translation of TD into MSO (which can actually be computed in exponential time). On the other hand, as regards MSO, its decision algorithms are far from feasible. Actually, already the satisfiability problem for FO over K fin is non-elementary: neither its time nor its space complexity is bounded above by any tower of exponentials of a fixed height; cf. (Stockmeyer, 1974, Fact 5.1, p. 162). Now, it appears to be a most reasonable conjecture that TD-SAT is non-elementary. This remains to be proven, however. Further, it might be of interest to find a fragment L of TD (not obtained by syntactically banning ¬ or ) whose satisfiability problem would indeed be elementarily decidable and which would be capable of describing independently occurring decision problems.

  Further, w ∈ [a] iff w = a iff (w is of size 1 and w |= p a ) iff w |= ((¬⊥ ∧ ⊥) ∧ p a ). Assume, then, inductively that if u ∈ {r, s} is an expression in R 0 (Σ), then for all words w ∈ Σ * we have: w ∈ [u] iff w |= T (u). Clearly the claim holds for the expressions r c and (r ∪ s).

  ) w has a factorization each of whose factors belongs to [a • ] or to [b • ], and (3) w cannot be factored into at least 4 factors each of which belongs to [a • ] or to [b • ]. By conditions (1) and (

Theorem 6. 1

 1 Let |π| ≥ 2. Then TD[π] < TDN[π]. Proof. Let π be any set of atoms. Trivially we have TD[π] ≤ TDN[π]. So it suffices to show that TDN[π] ≤ TD[π]. Consider the word ab. By Lemma 4.3, any TD[π] formula true at ab is also true at its mirror image ba. Yet the TDN[π] formula (p a and next p b ) is true at ab but not at ba. So TDN[π] is not translatable into TD[π].

  Clearly we have w |= φ iff w ∈ [S(φ)], for all words w ∈ Σ * and all formulas φ of TDN[π Σ ].

  (a) TDN(⊥, ∨, and next, ¬) < TDN; (b) If |π| ≥ 2, then TDN(⊥, ∨, and next, ¬)[π] || TD[π]. Proof. For (a), we note that over K fin , TDN(⊥, ∨, and next, ¬) = FO < MSO = TDN. The statement (b) follows immediately from Theorems 5.2 and 7.2.

If S is a set, P(S) stands for its power set.

Formulations of FO allowing empty domains are well known in the literature; see e.g.[START_REF] Mostowski | On the Rules of Proof in the Pure Functional Calculus of the First Order[END_REF];[START_REF] Hailperin | Quantification Theory and Empty Individual-Domains[END_REF];[START_REF] Hintikka | Distributive Normal Forms in the Calculus of Predicates[END_REF];[START_REF] Quine | Quantification and the Empty Domain[END_REF];[START_REF] Williamson | A Note on Truth, Satisfaction and the Empty Domain[END_REF]. There are various subtleties involved in the formulation; the choices one makes will affect the metalogical properties of the resulting language (e.g., formulas equivalent over non-empty domains may fail to be so when empty models are accepted, cf. vacuous quantification). For the purposes of the present paper it suffices that we have a semantics agreeing with the standard one on non-empty models and rendering all sentences of the form ∀xφ (respectively ∃xφ) true (false) over empty models.

Strictly speaking we wish the evaluation to be always relative to intervals. When saying that a formula holds (fails) at an instant t, what we mean is that it holds (fails) at the singleton interval[ [t] ].

It might be possible to formulate the truth-conditions of TD formulas in the framework of neighborhood semantics. Our general viewpoint on modal semantics does not lead us in that direction, however. We see no problem in allowing the use of any abstract logic (not necessarily FO) for the specification of truth-conditions. Accordingly, the semantics of and is in effect in terms of MSO. For a general formulation of this perspective, see[START_REF] Hella | On the Existence of a Modal-Logical Basis for Monadic Second-Order Logic[END_REF]; for the special case in which FO suffices for phrasing the semantics, see e.g.[START_REF] Gabbay | Temporal Logic[END_REF].

Suppose i is an arbitrary interval and t1, . . . , tn are elements of i such that t1 < . . . < tn and tn is not the last element (if any) of i. Then the division determined by these points is the tuple whose members are the subintervals of i determined by the sets {x : x ∈ i and x ≤ t1}, (t1, t2], . . . , (tn-1, tn], {x : x ∈ i and x > tn}, in this order. The general condition for the truth of φ at i is simply this: there is a finite set of division points in i such that every part of the division determined by these points makes φ true.

Nothing would prevent us from considering further operations on languages and letting them define further regular-like expressions; if this was done, the above definition of RLE(Σ) would of course be different.

The question of being superfluous is of course not absolute: here our considerations are relative to the operators ⊥, ¬, ∨, taken as primitive.

The logic MLR is defined so that it has an even more straightforward connection to regular expressions than the logic TDN to be discussed in Section 6 of the present paper. Over finite intervals, MLR has the same expressive power as TDN. Yet it turns out that in TDN negation is not superfluous. This difference stems from the different ways in which the two logics interpret atomic formulas.

So is any palindrome, i.e., any word w satisfying a1 . . . an = w = an . . . a1.

These two expressivity results are due to J. van[START_REF] Van Benthem | Modal Correspondence Theory[END_REF] and H.[START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF], respectively. For nice presentations of the respective results, see, e.g.,(Blackburn et al., 2002, Sect. 2.6) and(Gabbay et al., 1994, Sect. 10.3).

For an approach in which k-dimensional modal formulas (formulas evaluated relative to k-tuples of points) are translated by formulas of some abstract logic using k free variables, see(Hella and Tulenheimo,

Typically this result is formulated for languages L not containing the empty word; this is because usually first-order structures are taken to have a non-empty domain, while the first-order structure induced by the empty word has an empty domain. It is not difficult to show that Proposition 6.4 follows from the usual formulation of Büchi's theorem.

Like Büchi's result about MSO, also this result is typically formulated for languages L not containing the empty word. It is not difficult to show that Proposition 7.1 follows from the usual formulation of McNaughton & Papert's theorem.

If φ had a translation into TD, this translation would be in TD[∅]. Fact 7.4 establishes the stronger result that for every set π of atoms, there is no formula χ of TD[π] such that Mod(φ) ∩ K fin (π) = Mod(χ) ∩ K fin (π).

Acknowledgments

The author wishes to thank Lauri Hella for helpful discussions on formal languages and modal logics, and the anonymous referee for useful comments.

Proof. Let π be any set of atoms. By Theorem 6.2, we have that TDN[π] = RE(Σ π ). By Proposition 6.4, RE(Σ π ) = MSO[τ π ]. It follows that over the class K word (π), we have

As a matter of fact, the expressive powers of the logics TDN and MSO coincide on the whole class K fin , not only on K word . To see this, we prove the following fact. If π is the set {p i : 1 ≤ i ≤ n}, let w(π) be the set {q f : f ∈ {0, 1} n }. Now, every interval i = (T, <, V ) with V of type T → P(π) can be turned into a word interval w(i) = (T, <, U ) with U of type T → P(w(π)) by setting, for every function f : {1, . . . , n} → {0, 1}: Proof. Consider item (1); the proof of item ( 2) is entirely analogous. Let π be any set of atoms. For the case (a), if φ is any TDN[π] formula, let ψ φ be the formula of TDN[w(π)] obtained from φ by replacing in φ all occurrences of p i by the disjunction of all atomic formulas q f for which

As regards the case (b), if χ is a formula of TDN[w(π)], obtain the formula θ χ of TDN[π] from χ by replacing all occurrences of q f by the formula

, where p 1 i = p i and p 0 i = ¬p i . Obviously w(i) |= χ iff i |= θ χ , for all i ∈ K fin (π). Fact 6.6 means, in particular, that in connection with both logics TDN and MSO, word intervals are representative of the whole class K fin : instead of asking whether a formula φ of TDN (respectively, of MSO) is true at an interval i, we may equivalently ask whether ψ φ is true at the word interval w(i). Using Fact 6.6, we are in a position to generalize Lemma 6.5 to the entire class K fin . Theorem 6.7 TDN = K fin MSO.

Proof. Let π be any set of atoms. Directly by Fact 6.3, we have that TDN[π] ≤ MSO[τ π ] over K fin (π). For the converse direction, let Ψ ∈ MSO[τ π ] be arbitrary. By Fact 6.6(2.a) we find a formula Φ Ψ ∈ MSO[τ w(π) ] such that i |= Ψ iff w(i) |= Φ Ψ for all i ∈ K fin (π). Further, by Lemma 6.5 and the fact that for every j ∈ K word (w(π)) there is i ∈ K fin (π) such that j = w(i), we know that there is a formula χ ∈ TDN[w(π)] such that w(i) |= Φ Ψ iff w(i) |= χ, for all i ∈ K fin (π). Finally, applying Fact 6.6(1.b) we may conclude that there is a formula θ χ ∈ TDN[π] such that w(i) |= χ iff i |= θ χ , for all i ∈ K fin (π). It follows, then, that for all i ∈ K fin (π) we have: i |= Ψ iff i |= θ χ , that is, θ χ is a translation of Ψ in TDN[π] relative to the class K fin (π).