On Almost Future Temporal Logics

Abstract

Kamp’s theorem established the expressive completeness of the temporal modalities Until and Since for the First-Order Monadic Logic of Order (FOMLO) over real and natural time flows. Over natural time, a single future modality (Until) is sufficient to express all future FOMLO formulas. These are formulas whose truth value at any moment is determined by what happens from that moment on. Yet this fails to extend to real time domains: here no finite basis of future modalities can express all future FOMLO formulas. Almost future formulas extend future formulas; they depend just on the very near past, and are independent of the rest of the past. For almost future formulas finiteness is recovered over Dedekind complete time flows. In this paper we show that there is no temporal logic with finitely many modalities which is expressively complete for the almost future fragment of FOMLO over all linear flows.

Dedicated to Yuri Gurevich on the occasion of his 75th birthday.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Temporal Logic ($TL$) introduced to Computer Science by Pnueli in [7] is a convenient framework for reasoning about “reactive” systems. This made temporal logics a popular subject in the Computer Science community, enjoying extensive research in the past 30 yrs. In $TL$ we describe basic system properties by atomic propositions that hold at some points in time, but not at others. More complex properties are expressed by formulas built from the atoms using Boolean connectives and Modalities (temporal connectives): A k-place modality $\mathsf{M}$ transforms statements $\varphi _1\ldots \varphi _k$ possibly on ‘past’ or ‘future’ points to a statement $\mathsf{M}(\varphi _1\ldots \varphi _k)$ on the ‘present’ point $t_0$. The rule to determine the truth of a statement $\mathsf{M}(\varphi _1\ldots \varphi _k)$ at $t_0$ is called a Truth Table. The choice of particular modalities with their truth tables yields different temporal logics. A temporal logic with modalities $M_1,\dots ,M_k$ is denoted by $TL (M_1,\dots ,M_k)$.

The simplest example is the one place modality $\mathsf{F}X$ saying: “X holds some time in the future”. Its truth table is formalized by $\varphi _{{}_{\!\mathsf{F}}} (t_0,X)\equiv (\exists t>t_0) X(t)$. This is a formula of the First-Order Monadic Logic of Order (FOMLO) - a fundamental formalism in Mathematical Logic where formulas are built using atomic propositions P(t), atomic relations between elements $t_1=t_2$, $t_1<t_2$, Boolean connectives and first-order quantifiers $\exists t$ and $\forall t$. Most modalities used in the literature are defined by such FOMLO truth tables, and as a result every temporal formula translates directly into an equivalent FOMLO formula. Thus, the different temporal logics may be considered a convenient way to use fragments of FOMLO. FOMLO can also serve as a yardstick by which to check the strength of temporal logics: A temporal logic is expressively complete for a fragment L of FOMLO if every formula of L with a single free variable is equivalent to a temporal formula.

Actually, the notion of expressive completeness is with respect to the type of the underlying model since the question whether two formulas are equivalent depends on the domain over which they are evaluated. Any (partially) ordered set with monadic predicates is a model for $TL$ and FOMLO, but the main, canonical, linear time intended models are the naturals $\langle \mathbb {N}, <\rangle$ for discrete time and the reals $\langle \mathbb {R}, <\rangle$ for continuous time.

A major result concerning $TL$ is Kamp’s theorem [2, 6], which states that the pair of modalities “$X{~ until~} Y$”$\ { and}\ ``X{~ since~} Y$” is expressively complete for FOMLO over the above two linear time canonical models.

Many temporal formalisms studied in computer science concern only future formulas - whose truth value at any moment is determined by what happens from that moment on. For example the formula X until Y says that X will hold from now (at least) until a point in the future when Y will hold. The truth value of this formula at a point $t_0$ does not depend on the question whether X(t) or Y(t) hold at earlier points $t<t_0$.

Over the discrete model $\langle \mathbb {N}, <\rangle$ Kamp’s theorem holds also for future formulas of FOMLO: The future fragment of FOMLO has the same expressive power as $TL (\mathsf{Until})$ [2, 4]. The situation is radically different for the continuous time model $\langle \mathbb {R}, <\rangle$. In [5] it was shown that $TL (\mathsf{Until})$ is not expressively complete for the future fragment of FOMLO and there is no easy way to remedy it. In fact it was shown in [5] that there is no temporal logic with a finite set of modalities which is expressively equivalent to the future fragment of FOMLO over the reals.

It was proved in [2] that all future formulas are expressible over the reals in a temporal language based on the future modality $\mathsf{Until}$ plus the modality $\mathsf{K^{-}}$. The formula $\mathsf{K^{-}}(P)$ holds at a time point $t_0$ if given any ‘earlier’ t, no matter how close, we can always come up with a $t'$ in between ($t < t' < t_0$) where P holds. This is of course not a future modality - the formula $\mathsf{K^{-}}(P)$ is past-dependent. This future-past mixture of $\mathsf{Until}$ and $\mathsf{K^{-}}$ is somewhat better than the standard $\mathsf{Until}$ - $\mathsf{Since}$ basis in the following sense: Although $\mathsf{K^{-}}$ is (like $\mathsf{Since}$) a past modality, it does not depend on much of the past: The formula $\mathsf{K^{-}}(P)$ depends just on an arbitrarily short ‘near past’, and is actually independent of most of the past. In this sense we may say that it is an “almost future” formula (see Sect. 3 for precise definitions).

In [8] it was proved that $TL (\mathsf{Until},\mathsf{K^{-}})$ is expressively equivalent over the reals (and over all Dedekind complete time domains) to the almost future fragment of FOMLO.

Kamp’s theorem was generalized by Stavi who introduced two new modalities $\mathsf{Until}'$ and $\mathsf{Since}'$ and proved that $TL (\mathsf{Until}, \mathsf{Since}, \mathsf{Until}', \mathsf{Since}')$ and FOMLO have the same expressive power over all linear time flows [2, 4].

Our main theorem shows that Stavi’s theorem cannot be generalized to almost future fragments. We show that there is no temporal logic with a finite set of modalities which is expressively equivalent to the almost future fragment of FOMLO over all linear time flows.

The rest of the paper is organized as follows: In Sect. 2 we recall the definitions of the monadic logic, the temporal logics and Kamp’s and Stavi’s theorems. In Sect. 3 we define “future” and “almost future” fragments of $\textit{FOMLO}$ and state expressive completeness results for these fragments. In Sect. 4 we prove that over the class of all linear orders there is no finite basis for a temporal logic which is expressively complete for almost future formulas. The ideas and techniques are similar to those in [5]. We will define a sequence of future formulas $\psi _i$ such that given any (finite or infinite) set B of modalities definable in the almost future fragment of $\textit{FOMLO}$ by formulas of quantifier depth at most n, there is k such that $\psi _{k}$ is not expressible in $TL (B)$. Thus, in particular, no logic with finitely many almost future modalities can express all $\psi _i$.

2 Preliminaries

We start with the basic definitions of First-Order Monadic Logic of Order (FOMLO) and Temporal Logic (TL), and some well known results concerning their expressive power.

Fix a signature (finite or infinite) $\mathcal {S}$ of atoms. We use $P, Q, R, S \dots$ to denote members of $\mathcal {S}$. Syntax and semantics of both logics are defined below with respect to such a fixed signature.

2.1 First-Order Monadic Logic of Order

Syntax: In the context of FOMLO, the atoms of $\mathcal {S}$ are referred to (and used) as unary predicate symbols. Formulas are built using these symbols, plus two binary relation symbols, $<$ and $=$, and a finite set of first-order variables (denoted by $x,y, z, \dots$). Formulas are defined by the grammar:

$$\begin{aligned} atomic\, {:}{:}= ~~x < y ~~|~~ x = y ~~|~~P(x)~~~~~~~~~~ (\mathrm{where} ~~ P \in \mathcal {S}) \end{aligned}$$

$$\begin{aligned} \varphi \, {:}{:}= ~~ atomic ~~|~~ \lnot \varphi _1 ~~|~~ \varphi _1 \vee \varphi _2 ~~|~~ \varphi _1 \wedge \varphi _2 ~~|~~ \exists x \varphi _1 ~~|~~ \forall x \varphi _1 \end{aligned}$$

The notation $\varphi (x_1, \dots , x_n)$ implies that $\varphi$ is a formula where the $x_i$’s are the only variables that may occur free; writing $\varphi (x_1, \dots , x_n, P_1, \dots , P_k)$ additionally implies that the $P_i$’s are the only predicate symbols that may occur in $\varphi$. We will also use the standard abbreviated notation for bounded quantifiers, e.g.: $(\exists x)_{> z}(\dots )$ denotes $\exists x ((x > z) \wedge (\dots ))$, $(\forall x)^{\le z}(\dots )$ denotes $\forall x ((x \le z) \rightarrow (\dots ))$, ${(\forall {x})_{> {l}}^{< {u}} (\dots )}$ denotes $\forall x ((l < x < u) \rightarrow (\dots ))$, etc. Finally, as usual, True(x) denotes $P(x) \vee \lnot P(x)$ and False(x) denotes $P(x) \wedge \lnot P(x)$.

Semantics: Formulas are interpreted over structures. A structure over $\mathcal {S}$ is a triplet $\mathcal {M}= (\mathcal {T}, <, \mathcal {I})$ where $\mathcal {T}$ is a set - the domain of the structure, $<$ is an irreflexive partial order relation on $\mathcal {T}$, and $\mathcal {I}: \mathcal {S} \rightarrow \mathcal {P} (\mathcal {T})$ is the interpretation of the structure (where $\mathcal {P}$ is the powerset notation). We use the standard notation $\mathcal {M}, t_1, t_2, \dots t_n \,\models \,\varphi (x_1, x_2, \dots x_n)$. The semantics is defined in the standard way. Notice that for formulas with at most one free first-order variable, this reduces to:

$$\begin{aligned} \mathcal {M}, t \,\models \,\varphi (x). \end{aligned}$$

We will often abuse terminology, and shortly refer to such formulas as monadic formulas (or to the corresponding syntactical fragment - as FOMLO).

2.2 Propositional Temporal Logics

Syntax: In the context of TL, the atoms of $\mathcal {S}$ are used as atomic propositions (also called propositional atoms). Formulas are built using these atoms, and a set (finite or infinite) B of modality names, where a non-negative integer arity is associated with each $\mathsf{M}\in B$. The syntax of TL with the basis B over the signature $\mathcal {S}$, denoted by TL(B), is defined by the grammar:

$$\begin{aligned} F{:}{:}= ~~P ~~|~~ \lnot F_1 ~~|~~ F_1 \vee F_2 ~~|~~ F_1 \wedge F_2 ~~|~~ \mathsf{M}(F_1,F_2,\dots ,F_n) \end{aligned}$$

where $P \in \mathcal {S}$ and $\mathsf{M}\in B$ an n-place modality (that is, with arity n). As usual True denotes $P \vee \lnot P$ and False denotes $P \wedge \lnot P$.

Semantics: Formulas are interpreted at time-points (or moments) in structures (elements of the domain). The domain $\mathcal {T}$ of $\mathcal {M}= (\mathcal {T}, <, \mathcal {I})$ is called the time domain, and $(\mathcal {T}, <)$ - the time flow of the structure. The semantics of each n-place modality $\mathsf{M}\in B$ is defined by a ‘rule’ specifying how the set of moments where $\mathsf{M}(F_1, \dots , F_n)$ holds (in a given structure) is determined by the n sets of moments where each of the formulas $F_i$ holds. Such a ‘rule’ for $\mathsf{M}$ is formally specified by an operator $\mathcal {O}_{\mathsf{M}}$ on time flows, where given a time flow $\mathcal {F} = (\mathcal {T}, <)$, $\mathcal {O}_{\mathsf{M}} (\mathcal {F})$ is an operator in $(\mathcal {P}(\mathcal {T}))^n \longrightarrow \mathcal {P}(\mathcal {T})$.

The semantics of $TL (B)$ formulas is then defined inductively: Given a structure $\mathcal {M}= ( \mathcal {T}, <, \mathcal {I})$ and a moment $t \in \mathcal {M}$ (read $t \in \mathcal {M}$ as $t \in \mathcal {T}$), define when a formula F holds in $\mathcal {M}$ at t - notation: $\mathcal {M}, t\,\models \,F$ - as follows:

• $\mathcal {M}, t\,\models \,P$ iff $t \in \mathcal {I}(P)$, for any propositional atom P.

• $\mathcal {M}, t\,\models \,F \vee G$ iff $\mathcal {M}, t\,\models \,F$ or $\mathcal {M}, t\,\models \,G$; similarly (“pointwise”) for $\wedge$, $\lnot$.

• $\mathcal {M}, t\,\models \,\mathsf{M}(F_1, \dots , F_n) \ \text {iff} \ t \in [\mathcal {O}_{\mathsf{M}} (\mathcal {T}, <)](T_1, \dots , T_n)$ where $\mathsf{M}\in B$ is an n-place modality, $F_1, \dots , F_n$ are formulas and $T_i =_{def} \{ s \in \mathcal {T}: \mathcal {M}, s\,\models \,F_i \}$.

Truth Tables: Practically most standard modalities studied in the literature can be specified in FOMLO: A FOMLO formula $\varphi (x, P_1, \dots , P_n)$ with a single free first-order variable x and with n predicate symbols $P_i$ is called an n -place first-order truth table. Such a truth table $\varphi$ defines an n-ary modality $\mathsf{M}$ (whose semantics is given by an operator $\mathcal {O}_{\mathsf{M}}$) iff for any time flow $(\mathcal {T}, <)$, for any $T_1, \dots , T_n \subseteq \mathcal {T}$ and for any structure $\mathcal {M}= (\mathcal {T}, <, \mathcal {I})$ where $\mathcal {I}(P_i) = T_i$:

$$\begin{aligned}{}[\mathcal {O}_{\mathsf{M}}(\mathcal {T}, <)](T_1, \dots , T_n) = \{ t \in \mathcal {T} : \mathcal {M}, t\,\models \,\varphi (x, P_1, \dots , P_n) \} \end{aligned}$$

Example 2.1

Below are truth-table definitions for the well known “Eventually” and “Globally”, the (binary) strict-${{\mathbf {\mathsf{{Until}}}}}$ and strict-${{\mathbf {\mathsf{{Since}}}}}$ of [6] and for ${{\mathbf {\mathsf{{K}}}}}^{+}$ and ${{\mathbf {\mathsf{{K}}}}}^{-}$ of [2]:

• $\Diamond$ (“Eventually”) defined by: $\varphi _{_{\Diamond }}(x, P) =_{def} (\exists x') _{> x} P(x')$

• $\Box$ (“Globally”) defined by: $\varphi _{_{\Box }}(x, P) =_{def} (\forall x') _{> x} P(x')$

• ${{\mathbf {\mathsf{{Until}}}}}$ defined by: $\varphi _{_{\mathsf{Until}}}(x, Q, P) =_{def} (\exists x') _{> x} (Q(x') \wedge (\forall y) _{> x} ^{< x'} P(y))$

• ${{\mathbf {\mathsf{{Since}}}}}$ defined by: $\varphi _{_{\mathsf{Since}}}(x, Q, P) =_{def} (\exists x') ^{< x} (Q(x') \wedge (\forall y) _{> x'} ^{< x} P(y))$

• ${{\mathbf {\mathsf{{K}}}}}^{+}$ defined by: $\varphi _{_{\mathsf{K^{+}}}}(x, P) =_{def} (\forall x') _{> x} (\exists y) _{> x} ^{< x'} P(y)$

• ${{\mathbf {\mathsf{{K}}}}}^{-}$ defined by: $\varphi _{_{\mathsf{K^{-}}}}(x, P) =_{def} (\forall x') ^{< x} (\exists y) _{> x'} ^{< x} P(y)$

We will use infix notation for the binary modalities $\mathsf{Until}$ and $\mathsf{Since}$: $P {~\mathsf Until ~}Q$ denotes $\mathsf{Until}(Q, P)$, meaning “there is some future moment where Q holds, and P holds all along till then”. The non-strict version $\mathsf{Until}^{ns}$ is defined as $P \wedge (P {~\mathsf Until ~}Q)$, requiring that P should hold at the “present moment” as well.

The formula $\mathsf{K^{-}}(P)$ holds at the “present moment” $t_0$ iff given any earlier $t < t_0$ - no matter how close - there is a moment $t'$ in between ($t < t' < t_0$) where the formula P holds. Notice that $\mathsf{K^{+}}$ and $\mathsf{K^{-}}$ are definable in terms of $\mathsf{Until}$ and $\mathsf{Since}$:

$$\begin{aligned} \mathsf{K^{+}}(P) \equiv \lnot (\lnot P {~\mathsf Until ~}True) \end{aligned}$$

$$\begin{aligned} \mathsf{K^{-}}(P) \equiv \lnot (\lnot P {~\mathsf Since ~}True) \end{aligned}$$

2.3 Kamp’s and Stavi’s Theorems

We are interested in the relative expressive power of TL (compared to FOMLO) over the class of linear structures. Major results in this area are with respect to the subclass of Dedekind complete structures - where the order is Dedekind complete, that is, where every non empty subset (of the domain) which has an upper bound has a least upper bound.

Equivalence between temporal and monadic formulas is naturally defined: $F \equiv \varphi (x)$ iff for any $\mathcal {M}$ and $t \in \mathcal {M}$: $\mathcal {M}, t\,\models \,F \Leftrightarrow \mathcal {M}, t\,\models \,\varphi (x)$. We will occasionally write $\equiv _{_{\mathcal {L}}}$ / $\equiv _{_{\mathcal {DC}}}$ / $\equiv _{_{\mathcal {C}}}$ to distinguish equivalence over linear / Dedekind complete / any class $\mathcal {C}$ of structures.

Definability: A temporal modality is definable in FOMLO iff it has a FOMLO truth table; a temporal formula F is definable in FOMLO over a class $\mathcal {C}$ of structures iff there is a monadic formula $\varphi (z)$ such that $F \equiv _{_{\mathcal {C}}}\varphi (z)$. In this case we say that $\varphi$ defines F over $\mathcal {C}$. Similarly, a monadic formula $\varphi (z)$ may be definable in $TL (B)$ over $\mathcal {C}$.

Expressive Completeness / Equivalence: A temporal language $TL (B)$ (as well as the basis B) is expressively complete for (a fragment of) FOMLO over a class $\mathcal {C}$ of structures iff all monadic formulas (of that fragment) $\varphi (z)$ are definable over $\mathcal {C}$ in $TL (B)$. Similarly, one may speak of expressive completeness of FOMLO for some temporal language. If we have expressive completeness in both directions between two languages - they are expressively equivalent.

As $\mathsf{Until}$ and $\mathsf{Since}$ are definable in FOMLO, it follows that FOMLO is expressively complete for $TL (\mathsf{Until},\mathsf{Since})$. The fundamental theorem of Kamp shows that for Dedekind complete structures the opposite direction holds as well:

Theorem 2.2

(Kamp [2, 6, 9]). $TL (\mathsf{Until},\mathsf{Since})$ is expressively equivalent to FOMLO over Dedekind complete structures.

This was further generalized by Stavi who introduced two new modalities $\mathsf{Until}'$ and $\mathsf{Since}'$ and proved

Theorem 2.3

(Stavi [2, 4]). $TL (\mathsf{Until}, \mathsf{Since}, \mathsf{Until}', \mathsf{Since}')$ is expressively equivalent to FOMLO over all linear time structures.

The definitions of Stavi’s modalities are not needed for the proofs of our main result. However, for the sake of completeness, they are described below.

A gap of a linearly ordered set $({T}, <)$ is a downward closed non-empty set $C \subseteq {T}$ which has an upper bound in $({T}, <)$, yet has no least upper bound. Informally, we can think of a gap as a hole in the Dedekind-incomplete order.

$P\mathsf{Until}' Q$ holds at t if there is a gap C such that:

• $t\in C$, i.e., C is in the future of t,

• P is true on $(t,\infty )\cap C$, i.e., P holds from t until the gap,

• for every $t_1\notin C$ there is $t_2\in (-\infty ,t_1)\setminus C$ such that $\lnot P(t_2)$, i.e., in the future of the gap, P is false arbitrary close to the gap, and

• there is $t'\notin C$ such that Q is true on $(-\infty ,t')\setminus C$, i.e., Q is true from the gap into the future for some uninterrupted stretch of time.

Note that a natural formalization of the above definition of $\mathsf{Until}'$ uses a second-order quantifier - “there is a gap”; however, $\mathsf{Until}'$ has a first-order truth table [2].

$\mathsf{Since}'$ is the mirror image of $\mathsf{Until}'$.

3 Future and Almost Future Formulas

We use standard interval notations and terminology for subsets of the domain of a structure $\mathcal {M}= (\mathcal {T}, <, \mathcal {I})$, e.g.: ${(t, \infty ) =_{def} \{t' \in \mathcal {T} | t' > t\}}$; similarly we define $(t, t'), [t, t'), (t, \infty ), [t, \infty )$, etc., where $t < t'$ are the endpoints of the interval. The sub-structure of $\mathcal {M}$ restricted to an interval is defined naturally. In particular: $\mathcal {M}|_{_{>t_{0}}}$ denotes the sub-structure of $\mathcal {M}$ restricted to $(t_0, \infty )$: Its domain is $(t_0, \infty )$ and its order relation and interpretation are those of $\mathcal {M}$, restricted to this interval. $\mathcal {M}|_{_{\ge t_{0}}}$ is defined similarly with respect to $[t_0, \infty )$. Notice that if $\mathcal {M}$ is Dedekind complete then so is any sub-structure of $\mathcal {M}$. If structures $\mathcal {M}, \mathcal {M}'$ have domains $\mathcal {T}, \mathcal {T'}$, and if I is an interval of $\mathcal {M}$, with endpoints $t_1 < t_2$ in $\mathcal {M}$, such that $I \cup \{ t_1, t_2 \} \subseteq \mathcal {T} \cap \mathcal {T'}$ and the order relations of both structures coincide on $I \cup \{ t_1, t_2 \}$ - we will say that I is a common interval of both structures. This is defined similarly for intervals with $\infty$ or $-\infty$ as either endpoint. Two structures coincide on a common interval iff the interpretations coincide there. Two structures agree on a formula at a given common time-point (or along a common interval) iff the formula has the same truth value at that point (or along that interval) in both structures.

Definition 3.1

(Future and Almost Future Formulas and Modalities). A formula (temporal, or monadic with at most one free variable) F is (semantically):

• A future formula iff whenever two linear structures coincide on a common interval $[t, \infty )$ they agree on F at t; equivalently, whenever two linear structures coincide on a common interval $[t, \infty )$ they agree on F all along $[t, \infty )$.

• A pure future formula iff whenever two linear structures coincide on a common interval $(t, \infty )$ they agree on F at t; equivalently, whenever two linear structures coincide on a common interval $(t, \infty )$ they agree on F all along $[t, \infty )$.

• An almost future formula iff whenever two linear structures coincide on a common interval $(t, \infty )$ they agree on F all along $(t, \infty )$.

Past and pure past formulas are defined similarly. A temporal modality is a first-order future (almost future) modality iff it is definable in FOMLO by a future (almost future) truth table.

Looking at their truth tables, it is easy to verify that $\mathsf{Until}$ is a (pure) future modality and $\mathsf{Since}$ is a past modality and $\mathsf{K^{-}}$ is almost future modality. The pair $\{\mathsf{Until}, \mathsf{Since}\}$ forms an expressively complete (finite) basis in the sense of Kamp’s theorem. Do we have a finite basis of future modalities which is expressively complete for all future formulas? Here are some answers:

Theorem 3.2

([4]). $TL (\mathsf{Until})$ is expressively equivalent to the future fragment of FOMLO over discrete time flows (naturals, integers, finite).

Theorem 3.3

([5]). There is no temporal logic with a finite basis which is expressively equivalent to the future fragment of FOMLO over real time flows.

However, for the almost future fragment there is a finite base over Dedekind complete time flows.

Theorem 3.4

([8]). $TL (\mathsf{Until},\mathsf{K^{-}})$ is expressively equivalent to the almost future fragment of FOMLO over Dedekind complete time flows.

The situation is radically different for the class of all linear flows. Our main result shows that there is no finite base for the almost future fragment over all linear flows.

Theorem 3.5

(Main). There is no temporal logic with a finite basis which is expressively equivalent to the almost future fragment of FOMLO over all linear time flows.

4 No Finite Base for Almost Future Formulas

Observe that if a temporal logic is expressively equivalent to the almost future fragment of FOMLO, then all its modalities are almost future and are definable by FOMLO truth tables. The main theorem is a consequence of the next proposition:

Proposition 4.1

Assume that B is a set of almost future modalities definable by FOMLO truth tables of quantifier depth at most n. Then, TL(B) is not expressively complete for the future fragment of FOMLO over all linear time flows.

Note that Proposition 4.1 is much stronger than Theorem 3.5.

First, it allows for a temporal logic to have infinitely many almost future modalities and only requires that the quantifier depth of their truth table is bounded. Second, it concludes that such a temporal logic cannot express not only all almost future formulas, but even all future formulas.

We are going to define a sequence of future formulas $\psi _i$ such that for any (finite or infinite) set B of modalities definable in the almost future fragment of FOMLO by formulas of quantifier depth at most n, there is a k such that $\psi _{k}$ is not expressible in $TL (B)$.

For our proof of Proposition 4.1 we need some rudimentary facts on the ordinal numbers. Not much set theory is needed for our purpose; it suffices to say that every ordinal is a chain. We use the following ordinals which we define directly:

• The ordinal $\omega$ is the set of natural numbers with its natural order.

• The ordinal $\omega ^2$ is an $\omega$-sequence of blocks, each isomorphic to $\omega$. We also declare each point to be bigger than every point in a previous block.

• More generally, $\omega ^{n+1}$ is an $\omega$-sequence of blocks, each isomorphic to $\omega ^n$. Each point is declared larger than all points in previous blocks.

An alternative definition of the ordered set $\omega ^n$ is the set of n-tuples of natural numbers ordered lexicographically. The element which corresponds to a tuple $\langle m_{n-1},m_{n-2},\dots ,m_0\rangle$ is denoted by $\omega ^{n-1}m_{n-1}+\omega ^{n-2}m_{n-2}+\cdots + m_0$.

An easy induction proves the following useful feature of these ordinals:

Lemma 4.2

Every suffix of the ordinal $\omega ^k$ is isomorphic to $\omega ^k$.

We are going to define linear orders and chains which are very homogeneous with respect to almost future formulas:

Define the following linear orders:

$$\begin{aligned} (\mathcal {A}^k,<):=\big ((0,1)\cup (1,2)\big )\times \omega ^k, \end{aligned}$$

where (0, 1) and (1, 2) are subintervals of the reals and for $\langle a,\alpha \rangle , \langle b,\beta \rangle \in \mathcal {A}^k$, $\langle a,\alpha \rangle <\langle b,\beta \rangle$ if $\alpha <\beta$ or $\alpha =\beta$ and $a<b$.

Note that $(\mathcal {A}^k,<)$ are Dedekind-incomplete. For every $\beta \in \omega ^k$, the sets $C^1_\beta :=\{\langle a,\alpha \rangle \mid a<1\wedge \alpha \le \beta \}$ and $C^2_\beta :=\{\langle a,\alpha \rangle \mid a<2\wedge \alpha \le \beta \}$ are bounded and downward closed, yet none has a least upper bound.

Define a unary predicate $P^k:=(0,1)\times \omega ^k$ on $\mathcal {A}^k$ and define the following chains inthe signature $\{<,P\}$:

$$\begin{aligned}\mathcal {C}^k:=(\mathcal {A}^k,<,P^k).\end{aligned}$$

A unary predicate is said to be trivial on a chain in the signature $\{<,P\}$ if it is equal to P, $\lnot P$, ${True}$ or ${False}$.

Proposition 4.1 immediately follows from the next two lemmas.

Lemma 4.3

For every k there is a FOMLO future formula $\psi _k$ such that for every $m>k$, $\psi _k$ is equivalent to ${True}$ in $\mathcal {C}^m$ and $\psi _k$ is equivalent to ${False}$ in $\mathcal {C}^k$.

Lemma 4.4

Assume that B is any (finite or infinite) set of almost future modalities definable by $\textit{FOMLO}$ truth tables of quantifier depth at most n, then there is an infinite subset $J\subseteq \mathbb {N}$ such that for every formula $\varphi \in TL(B)$, and all $m,i\in J$ one of the following holds:

• 1. $\varphi$ is equivalent to P(x) in $\mathcal {C}^m$ and in $\mathcal {C}^i$.

• 2. $\varphi$ is equivalent to $\lnot P(x)$ in $\mathcal {C}^m$ and in $\mathcal {C}^i$.

• 3. $\varphi$ is equivalent to ${True}$ in $\mathcal {C}^m$ and in $\mathcal {C}^i$.

• 4. $\varphi$ is equivalent to ${False}$ in $\mathcal {C}^m$ and in $\mathcal {C}^i$.

Proof

(of Proposition 4.1 ). Take two numbers $i<m$ in J. By Lemma 4.3, $\psi _{i}$ is equivalent to ${False}$ in $\mathcal {C}^{i}$ and is equivalent to ${True}$ in $\mathcal {C}^{m}$. Hence, by Lemma 4.4 it is not equivalent to any formula $\varphi \in TL(B)$.       $\square$

Lemmas 4.3 and 4.4 are proved in the next two subsections. Subsection 4.3 states a generalization of Proposition 4.1.

4.1 Proof of Lemma 4.3

Let $\mathcal {C}$ be a chain, $\varphi (x)$ be a formula, and $a<b$ be elements of $\mathcal {C}$. We say that a, b are in the same $\varphi$ interval if either all elements in [a, b] satisfy $\varphi$ or none of them satisfies $\varphi$. We say that a, b are $\varphi$-equivalent if they are in the same $\varphi$-interval. Clearly, $\varphi$-equivalence is first-order definable and the $\varphi$ equivalence classes are subintervals of $\mathcal {C}$. The set of $\varphi$-equivalence classes are naturally ordered: an equivalence class $I_1$ precedes a class $I_2$ if all elements of $I_1$ precede all elements of $I_2$. A $\varphi$-equivalence class I is (left) limit if for every $\varphi$-equivalence class $I_1<I$ there is a $\varphi$-equivalence class $I_2$ such that $I_1<I_2<I$. Note that according to this definition the minimal $\varphi$-equivalence class is limit.

Define $\varphi _0(x):=P(x)$ and $\varphi _{i+1}(x):=$“x is in a limit $\varphi _i$-equivalence class”.

In $\mathcal {C}^n$ only the points of the form $\langle a,\omega ^{n-1}m_{n-1}+\omega ^{n-2}m_{n-2}+\cdots +\omega m_1 + 0\rangle$ where $a\in (0,1)$ satisfy $\varphi _1$; only the points of the form $\langle a,\omega ^{n-1}m_{n-1}+\omega ^{n-2}m_{n-2}+\cdots +\omega ^2m_2+ \omega 0 + 0\rangle$ where $a\in (0,1)$ satisfy $\varphi _2$ and only the points of the form $\langle a,\omega ^{n-1}m_{n-1}+\omega ^{n-2}m_{n-2}+\cdots +\omega ^lm_l+ \omega ^{l-1}0+\cdots +\omega 0 +0\rangle$ where $a\in (0,1)$ satisfy $\varphi _l$.

Note that $\varphi _{k}$ is not an almost future formula, but if we define $\psi _k(x_0)$ to be $(\exists x>x_0)\varphi _{k}(x) \wedge ``x \text { is not }\varphi _k-\mathrm{equivalent to } x_0$”, then $\psi _k$ is a future formula. Moreover, if $m\le k$ then $\psi _k$ is unsatisfiable in $\mathcal {C}^m$ and if $m>k$ then $\psi _k$ holds at all elements in $C^m$.

4.2 Proof of Lemma 4.4

We start from the following observation about chains $\mathcal {C}^k$ which shows that they are very homogeneous with respect to almost future formulas. Let $a\in P^k$ then there is $b<a$ and an isomorphism from $\mathcal {C}^k$ to the subchains of $\mathcal {C}^k$ over the interval $(b,\infty )$ which maps $\langle 1/2, 0, 0,\dots ,0\rangle$ to a. Similarly, if $a\notin P^k$ then there is $b<a$ and an isomorphism from $\mathcal {C}^k$ to the subchains of $\mathcal {C}^k$ over the interval $( b,\infty )$ which maps $\langle 3/2, 0, 0,\dots ,0\rangle$ to a.

This observation and the definition of almost future formulas immediately imply the following Lemma.

Lemma 4.5

Let $\varphi (x)$ be an almost future formula. The predicate definable by $\varphi$ in $\mathcal {C}^k$ is trivial.

Proof

Let $a_0:=\langle 1/2, 0, 0,\dots ,0\rangle$ and $a_1:=\langle 3/2, 0, 0,\dots ,0\rangle$. The above observation, invariance of formulas under isomorphisms, and the definition of almost future formulas imply that for every almost future formula $\varphi (x)$:

if $\mathcal {C}^k, a_0\models \,\varphi$ and $\mathcal {C}^k, a_1\models \,\varphi$, then $\varphi$ is equivalent to ${True}$ in $\mathcal {C}^k$.

if $\mathcal {C}^k, a_0\models \,\varphi$ and $\mathcal {C}^k, a_1\models \,\lnot \varphi$, then $\varphi$ is equivalent to P(x) in $\mathcal {C}^k$.

if $\mathcal {C}^k, a_0\models \,\lnot \varphi$ and $\mathcal {C}^k, a_1\models \,\varphi$, then $\varphi$ is equivalent to $\lnot P(x)$ in $\mathcal {C}^k$.

if $\mathcal {C}^k, a_0\models \,\lnot \varphi$ and $\mathcal {C}^k, a_1\models \,\lnot \varphi$, then $\varphi$ is equivalent to ${False}$ in $\mathcal {C}^k$.       $\square$

We introduce the notation $\equiv _n$ to say that two models cannot be distinguished by a first order sentence of quantifier depth n. More precisely, let M and $M'$ be two structures of the same signature. We write $M \equiv _n M'$ if and only if for any sentence $\varphi$ with $\mathrm{qd}\,({\varphi }) \le n$ we have $M \models \,\varphi$ iff $M'\,\models \,\varphi$. There are only finitely many semantically different sentences of quantifier depth n in the signature $\{<,P\}$ (see e.g., [3]). Therefore, for every n there are finitely many $\equiv _n$-classes. Hence, by pigeon-hole principle we have¹:

Lemma 4.6

For every n there is an infinite subset $J(n)\subseteq \mathbb {N}$ such that $\mathcal {C}^j\equiv _n\mathcal {C}^i$ for every $j,i\in J(n)$.

Lemma 4.7

Let $\varphi (x)$ be an almost future $\textit{FOMLO}$ formula of quantifier depth at most n. If $\mathcal {C}^m\equiv _{n+1} \mathcal {C}^k$ then one of the following holds:

• 1. $\varphi$ is equivalent to P(x) in $\mathcal {C}^m$ and in $\mathcal {C}^k$.

• 2. $\varphi$ is equivalent to $\lnot P(x)$ in $\mathcal {C}^m$ and in $\mathcal {C}^k$.

• 3. $\varphi$ is equivalent to ${True}$ in $\mathcal {C}^m$ and in $\mathcal {C}^k$.

• 4. $\varphi$ is equivalent to ${False}$ in $\mathcal {C}^m$ and in $\mathcal {C}^k$.

If one of the conditions (1)-(4) holds for a formula $\varphi$, we say that $\varphi$ defines the same trivial predicate in $\mathcal {C}^m$ and in $\mathcal {C}^k$.

Proof

By Lemma 4.5, $\varphi$ defines a trivial predicate in every $\mathcal {C}^m$. Hence, in every $\mathcal {C}^m$ exactly one of the following sentences holds: $\forall x \big (P(x)\leftrightarrow \varphi (x)\big )$, $\forall x \big (\lnot P(x)\leftrightarrow \varphi (x)\big )$, $\forall x \varphi (x)$ or $\forall x \lnot \varphi (x)$. These sentences have quantifier depth $n+1$. Since $\mathcal {C}^m\equiv _{n+1} \mathcal {C}^k$ we obtain that one of (1)-(4) holds.       $\square$

Lemma 4.8

Assume that B is a set of almost future modalities definable by $\textit{FOMLO}$ truth tables of quantifier depth at most n. If $\mathcal {C}^m\equiv _{n+1} \mathcal {C}^k$ then for every formula $\varphi \in TL(B)$, one of the following holds:

• 1. $\varphi$ is equivalent to P(x) in $\mathcal {C}^m$ and in $\mathcal {C}^k$.

• 2. $\varphi$ is equivalent to $\lnot P(x)$ in $\mathcal {C}^m$ and in $\mathcal {C}^k$.

• 3. $\varphi$ is equivalent to ${True}$ in $\mathcal {C}^m$ and in $\mathcal {C}^k$.

• 4. $\varphi$ is equivalent to ${False}$ in $\mathcal {C}^m$ and in $\mathcal {C}^k$.

Proof

We proceed by induction.

For the atomic formulas P, ${True}$ and ${False}$ the claim is obvious.

For Boolean combinations the result follows immediately from the induction assumption.

It remains to deal with the case where $\varphi =\mathsf{M}(\varphi _1,\cdots ,\varphi _l)$ where $\mathsf{M}$ is an l place modality with almost future truth table $\varPsi (x,P_1,\cdots ,P_l)$ of quantifier depth n. By the inductive assumption $\varphi _i$ defines the same trivial predicate $T_i$ in $\mathcal {C}^m$ and in $\mathcal {C}^k$. Let $\psi$ be obtained from $\varPsi$ when $P_i$ are replaced by the corresponding trivial predicate. Note that (1) $\psi$ defines the same predicate as $\varphi$ in $\mathcal {C}^m$ and in $\mathcal {C}^k$. (2) the quantifier depth of $\psi$ is at most n and it is an almost future formula, therefore by Lemma 4.7, $\psi$ defines the same trivial predicate in $\mathcal {C}^m$ and in $\mathcal {C}^k$. Finally, (1) and (2) imply that $\varphi$ defines the same trivial predicate in $\mathcal {C}^m$ and in $\mathcal {C}^k$.      $\square$

Proof

(of Lemma 4.4 ). Define J as $J(n+1)$. By Lemma 4.6 and 4.8 this J satisfies the conclusion of Lemma 4.4.       $\square$

4.3 A Generalization

Proposition 4.1 holds even when modalities are definable in the monadic second-order logic of order. Monadic second-order logic of order (MLO) extends first-order monadic logic of order with second-order monadic variables $X,Y,Z,\dots$ that range over subsets of the domain, and allows quantification over them. It is much more expressive than $\textit{FOMLO}$ and plays a fundamental role in Mathematics and Computer Science (see Gurevich’s survey [3]). An MLOformula $\varphi (x, P_1, \dots , P_n)$ with a single free first-order variable x and with n predicate symbols $P_i$ is called an n-place MLOtruth table. Similar to a FOMLO truth table, such an MLOtruth table $\varphi$ defines an n-ary modality $\mathsf{M}$. The definition of MLO future and almost future formulas is exactly like the definition of $\textit{FOMLO}$ future and almost future formulas (Definition 3.1). Proposition 4.1 can be strengthened as follows:

Proposition 4.9

Assume that B is a set of almost future modalities definable by MLO truth tables of quantifier depth at most n. Then, TL(B) is not expressively complete for the future fragment of FOMLO.

The proof of Proposition 4.9 is almost identical to the proof of Proposition 4.1. The only change is replace “$\equiv _n$” by “${\equiv }^{MLO}_n$”, where two structures are $\equiv ^{MLO}_n$-equivalent iff they satisfy the same MLO sentences of the quantifier depth n.