FO = FO3 for linear orders with monotone binary relations

TL;DR

This paper proves that monadic first-order logic over linear orders with certain monotone binary relations has the three-variable property, extending known results and providing a new proof via translation to star-free PDL.

Contribution

It generalizes the three-variable property to a broader class of linear orders with monotone relations and introduces a novel proof method using translation to star-free PDL.

Findings

Monadic first-order logic has the three-variable property over these classes.

The proof involves translating formulas into star-free PDL.

The results extend known cases and answer open questions.

Abstract

We show that over the class of linear orders with additional binary relations satisfying some monotonicity conditions, monadic first-order logic has the three-variable property. This generalizes (and gives a new proof of) several known results, including the fact that monadic first-order logic has the three-variable property over linear orders, as well as over (R,<,+1), and answers some open questions mentioned in a paper from Antonopoulos, Hunter, Raza and Worrell [FoSSaCS 2015]. Our proof is based on a translation of monadic first-order logic formulas into formulas of a star-free variant of Propositional Dynamic Logic, which are in turn easily expressible in monadic first-order logic with three variables.

Equations

$${\left({\mathcal{R}}_1\cdot {\mathcal{R}}_2\right)}^{-1}={{\mathcal{R}}_2}^{-1}\cdot {{\mathcal{R}}_1}^{-1}{\left({\mathcal{R}}^{\mathsf{c}}\right)}^{-1}={\left({\mathcal{R}}^{-1}\right)}^{\mathsf{c}}{\left({\mathcal{R}}_1\cap {\mathcal{R}}_2\right)}^{-1}={\mathcal{R}}_1^{-1}\cap {\mathcal{R}}_2^{-1}.$$

$$({\mathcal{R}}_1\cdot {\mathcal{R}}_2)(I)={\mathcal{R}}_2({\mathcal{R}}_1(I))={\mathcal{R}}_2(J\cap {\mathcal{R}}_1(A))=({\mathcal{R}}_2\cap {\mathcal{R}}_3)(J).$$

$$\Phi ::=P(x)\mid x\le y\mid x=y\mid \alpha (x,y)\mid \Phi \vee \Phi \mid \neg \Phi \mid \exists x.\Phi ,\text{where }x,y\in \mathcal{X},P\in \mathcal{P},\alpha \in \Gamma .$$

$$\exists z.p(x)=z\wedge \exists x.(p(y)=x\wedge z\le x).$$

$$\min (x)=$$

$$\left(\exists z.x<z\wedge \forall y.(x\le y<z⟹p(x)\le p(y))\right).$$

$$\exists y.y\le x\wedge (\min (y)\vee \max (y))\wedge \exists z.z<y\wedge (\min (z)\vee \max (z))\wedge \exists y.y<z\wedge (\min (y)\vee \max (y)).$$

$$\phi$$

$$\pi$$

$${[[P]]}^{\mathcal{M}}$$

$${[[\neg \phi ]]}^{\mathcal{M}}$$

$${[[\alpha ]]}^{\mathcal{M}}$$

$${[[\le ]]}^{\mathcal{M}}$$

$${[[{\pi }_1\cup {\pi }_2]]}^{\mathcal{M}}$$

$${[[{\pi }^{\mathsf{c}}]]}^{\mathcal{M}}$$

$$P{\mathsf{U}}_{(q,r)}Q\equiv ⟨(+q\cdot <)\cap (+r\cdot >)\cap {(<\cdot \{\neg P\}?\cdot <)}^{\mathsf{c}}⟩Q.$$

$$\mathsf{left}\text{leavevmode}\pi$$

$$\mathsf{right}\text{leavevmode}\pi$$

$${\pi }^{c1}$$

$${\pi }^{c2}$$

$${\pi }^{c3}$$

$${\pi }^{c4}$$

$$\phi$$

$$\pi$$

$$\phi$$

$$\pi$$

$${\pi }^{\mathsf{c}}\equiv$$

$$(\le \cdot \{\neg ⟨{\pi }^{-1}⟩\}?)\cup (\ge \cdot \{\neg ⟨{\pi }^{-1}⟩\}?)\cup$$

$$({\pi }^{c1})\cup ({\pi }^{c2})\cup ({\pi }^{c3})\cup ({\pi }^{c4}).$$

$$I{⊑}_{\text{left}}J$$

$$I{⊑}_{\text{right}}J$$

$$\Phi =\exists x.\left(\tilde{\phi }(x)\wedge \underset{1\le i\le n}{\bigwedge }\widetilde{{\pi }_i}(x_i,x)\right)(x_i\ne x\text{ for all i})$$

$$\Psi =\underset{1\le i,j\le n}{\bigwedge }\widetilde{({\pi }_i\cdot \{\psi \}?\cdot {\pi }_j^{-1})}(x_i,x_j).$$

$$\mathcal{M},\nu \models \Phi ⟺\bigcap _{1\le i\le n}{I}_i\ne \varnothing .$$

$$\mathcal{M},\nu \models \Phi$$

$$⟺\text{for all 1≤i,j≤n},(\nu (x_i),\nu (x_j))\in [[{\pi }_i\cdot \{\psi \}?\cdot {\pi }_j^{-1}]]$$

$$⟺\mathcal{M},\nu \models \Psi .$$

$$\exists x.{\rm Y}\equiv {{\rm Y}}_1\wedge \exists x.\left({{\rm Y}}_2\wedge \tilde{\phi }(x)\right)$$

$$(\le \cdot \{\phi \}?\cdot \ge )(x_1,x_1)\vee (\ge \cdot \{\phi \}?\cdot \le )(x_1,x_1).$$

Full text

1 Introduction

Logics with a bounded number of variables have been extensively studied, in particular in the context of descriptive complexity [17, 18, 10, 21] and temporal logics [20, 7, 14, 16]. One recurring question of interest [7, 25, 19, 4, 26, 1] is to determine, in a given class $\mathcal{C}$ of structures, whether all properties expressible in monadic first-order logic (FO) can be defined in the fragment $\textup{FO}^{k}$ consisting of formulas which use at most $k$ variables. (A same variable may be quantified over several times in a formula.) In fact, several non-equivalent versions of this question appear in the literature, many of which are compared in [15]. We say that $\mathcal{C}$ has the $k$-variable property if every formula of FO with at most $k$ free variables is equivalent over $\mathcal{C}$ to a formula of $\textup{FO}^{k}$. Note that this is strictly stronger than requiring that all sentences (without free variables) of FO are equivalent to some $\textup{FO}^{k}$ formulas. Indeed, Hodkinson and Simon gave an example of a class of structures where no sentence requires more than 3 variables, but which does not have the $k$-variable property for any $k$ [15].

The problem of whether a given class of structures has the $k$-variable property is closely related to the question of the existence of an expressively complete temporal logic (with a finite set of FO-definable modalities). A temporal logic is called expressively complete if any first-order formula with a single free variable can be expressed in it. For instance, it is well-known that linear temporal logic (LTL) over Dedekind-complete time flows, or its extension with Stavi connectives over all time flows, are expressively complete for first-order logic [20, 8]. More recently, it was shown that over the real numbers equipped with binary relations $+q$ for all $q\in\mathbb{Q}$, metric temporal logic (MTL) is expressively complete [16]. However, the questions of having the $k$-variable property for some $k$ or admitting an expressively complete temporal logic are incomparable in general: there exist a class of structures which admits a finite expressively complete set of temporal connectives but which does not have the $k$-variable property for any $k$ [15], and one which has the $3$-variable property but for which no temporal logic is expressively complete [14]. However, Gabbay established that having the $k$-variable property implies the existence of a multi-dimensional expressively complete temporal logic, with multiple reference points [7].

Another classical approach to proving or disproving that a class of structures has the $k$-variable property is through Ehrenfeucht-Fraïssé games, with a bounded number of pebbles [12, 25, 19, 1]. This was applied by Immerman and Kozen to linear orders and bounded-degree trees [19], and by Antonopoulos et al. to real-time signals [1].

Natural candidates for classes $\mathcal{C}$ which might have the $k$-variable property are classes of linearly ordered structures. Indeed, a typical counter-example to unrestricted structures having the $k$-variable property is a formula such as “there exists $k+1$ distinct elements which satisfy some predicate $P$”. It is in general not expressible in $\textup{FO}^{k}$, but it is easily expressible in $\textup{FO}^{2}$ if all models are equipped with a linear order $<$. For instance for $k=2$, we take the formula $\exists x.\ P(x)\land\exists y.(x<y\land P(y)\land\exists x.(y<x\land P(x)))$. As mentioned before, Immerman and Kozen showed that the class of linear orders has the $3$-variable property [19]. However, adding a single binary relation suffices to obtain a class of linearly ordered structures which does not have the $k$-variable property for any $k$. Venema gave an example of a dense linear order with a single equivalence relation which does not have the $k$-variable property for any $k$ [29]; this was adapted in [1] to give another example where the equivalence relation is replaced with a bijection. In fact, even for finite linear orders, Rossman [26] proved that the class of linearly ordered graphs does not have the $k$-variable property for any $k$, resolving a problem which had been open for more than 25 years [17]. Therefore, adding binary relations to linear orders while keeping the $k$-variable property requires some restrictions on the interpretation of the relation symbols.

On the positive side, Antonopoulos et al. proved that the class of structures over $(\mathbb{R},<,+1)$ (or signals) has the $3$-variable property [1]. Such structures have been studied in the context of real-time verification. As a corollary, they also showed that $(\mathbb{R},<,f)$ has the $3$-variable property for any linear function $f:x\mapsto ax+b$.

Contribution.

We consider the class of linearly ordered structures with an additional (finite or infinite) number of binary interval-preserving relations. These are binary relations $\mathrel{\mathcal{R}}$ such that, for all intervals $I$, any point which is in between two points of ${\mathrel{\mathcal{R}}}(I)$ and has a preimage by $\mathrel{\mathcal{R}}$ must have one in $I$. (We also require a symmetric condition of the converse relation ${\mathrel{\mathcal{R}}}^{-1}$.) We show that FO over this class of structures also has the $3$-variable property.

This generalizes results from [19] and [1] described above. Moreover, this answers some open questions mentioned in the conclusion of [1], which asked if the result could be extended from linear functions to polynomials over the reals, or other linear orders and families of monotone functions. In fact, all increasing or decreasing partial functions (over arbitrary linear orders) are special cases of interval-preserving relations, and thus covered by our result.

Our proof relies on different techniques than [19, 1], which were based on Ehrenfeucht-Fraïssé games. We give an effective translation from FO to $\textup{FO}^{3}$ which goes through a star-free variant of Propositional Dynamic Logic (PDL) with converse. Propositional dynamic logic was introduced by Fischer and Ladner [6] to reason about program schemes, and has now found a large range of applications in artificial intelligence and verification [11, 5, 23, 22, 9]. It combines local formulas containing modal operators, and path formulas using the concatenation, union and Kleene star operations. Several extensions have been studied, including PDL with converse [27], intersection [3], or negation of atomic programs [24]. The particular star-free variant of PDL we use here is in fact very similar to Tarski’s relation algebras [28], which was used as a basis for formalizing set theory. It also corresponds to a two-dimensional temporal logic in the sense of Gabbay [7].

We applied similar proof techniques in [2], where we introduced a star-free variant of PDL and proved that it is equivalent to FO over message sequence charts (MSCs) (and thus obtained a 3-variable property result for MSCs as a corollary). MSCs are discrete partial orders which represent behaviors of concurrent message passing systems. They consist of a fixed, finite number of linear orders called process orders (one for each process in the system), together with FIFO binary message relations connecting matching send and receive actions. Having a (fixed) finite number of total orders instead of a single one is not an important difference, as we could always put them one after the other to extend them into a single linear order. FIFO relations are a special case of interval-preserving relations, thus the result of the present paper can in fact be seen as a strict generalization of our previous result in [2]. More importantly, a major difference between MSCs studied in [2] and the setting we consider here is that MSCs are discrete structures, whereas here we allow arbitrary linear orders. In fact, [2] relied on the definition of formulas describing the minimum or the maximum of some binary relations. As such, it is interesting to see that the same kind of techniques can still be applied to a priori very different linear orders.

Outline.

In Section 2, we introduce interval-preserving relations and monadic first-order logic. In Section 3, we define star-free PDL, and prove some properties of its formulas. In Section 4, we give an effective translation from FO to star-free PDL, and explain its consequences. We conclude in Section 5.

2 Interval-preserving relations and first-order logic

In this section, we define the class of structures covered by our results, and recall the syntax of first-order logic.

Interval-preserving binary relations.

Let ${\mathrel{\mathcal{R}}}\subseteq{A}\times{B}$ be a binary relation between sets ${A}$ and ${B}$. We write $a\mathrel{\mathcal{R}}b$ if $(a,b)\in{\mathrel{\mathcal{R}}}$, and ${\mathrel{\mathcal{R}}}(a)=\{b\in{B}\mid a\mathrel{\mathcal{R}}b\}$. For a subset ${A}^{\prime}\subseteq{A}$, we also write ${\mathrel{\mathcal{R}}}({A}^{\prime})=\bigcup_{a\in{A}^{\prime}}{\mathrel{\mathcal{R}}}(a)$. We define the converse of a relation $\mathrel{\mathcal{R}}$ as ${\mathrel{\mathcal{R}}}^{-1}=\{(b,a)\in{B}\times{A}\mid(a,b)\in{\mathrel{\mathcal{R}}}\}$, and the composition of two binary relations ${\mathrel{\mathcal{R}}}_{1}\subseteq{A}\times{B}$ and ${\mathrel{\mathcal{R}}}_{2}\subseteq{B}\times{C}$ as ${\mathrel{\mathcal{R}}_{1}}\cdot{\mathrel{\mathcal{R}}_{2}}=\{(a,c)\in{A}\times{C}\mid\exists b\in{B}.\ (a,b)\in{\mathrel{\mathcal{R}}_{1}}\land(b,c)\in{\mathrel{\mathcal{R}}_{2}}\}$. Finally, we write ${\mathrel{\mathcal{R}}}^{\mathsf{c}}=({A}\times{B})\setminus{\mathrel{\mathcal{R}}}$ for the complement of $\mathrel{\mathcal{R}}$. Note that we have the following identities:

[TABLE]

A linear order ${\leq}$ over a set ${A}$ is a reflexive, transitive and antisymmetric relation ${\leq}\subseteq{A}\times{A}$ such that for all $a,b\in{A}$, we have $a\leq b$ or $b\leq a$. Let $({A},\leq)$ be a linearly ordered set. For ${A}^{\prime}\subseteq{A}$, we will also denote by $\leq$ the restriction of $\leq$ to ${A}^{\prime}$, so that $({A}^{\prime},\leq)$ is still a linearly ordered set. Moreover, for $a\in{A}$, we write $a<{A}^{\prime}$ if for all $a^{\prime}\in{A}^{\prime}$, $a<a^{\prime}$, and ${A}^{\prime}<a$ if for all $a^{\prime}\in{A}^{\prime}$, $a^{\prime}<a$.

An interval of $({A},\leq)$ is a set $I\subseteq{A}$ such that for all $a\leq b\leq c$ with $a,c\in I$, we have $b\in I$. For $a,b\in{A}$, we denote by $[a,b)$ the interval $\{c\in{A}\mid a\leq c<b\}$, and similarly for the intervals $[a,b]$, $(a,b]$, $(a,b)$. We call a relation ${\mathrel{\mathcal{R}}}\subseteq{A}\times{B}$ between two linearly ordered sets $({A},\leq_{A})$ and $({B},\leq_{{B}})$ interval-preserving if:

• •

For all intervals $I$ of $({A},\leq_{A})$, ${\mathrel{\mathcal{R}}}(I)$ is an interval of $({\mathrel{\mathcal{R}}}({A}),\leq_{B})$.

• •

For all intervals $J$ of $({B},\leq_{B})$, ${\mathrel{\mathcal{R}}}^{-1}(J)$ is an interval of $({\mathrel{\mathcal{R}}}^{-1}({B}),\leq_{A})$.

In other terms, for all $a_{1}\mathrel{\mathcal{R}}b_{1}$ and $a_{2}\mathrel{\mathcal{R}}b_{2}$ with $a_{1},a_{2}\in I$, for all $b_{1}\leq_{B}b\leq_{B}b_{2}$, if there exists some $a\in{A}$ such that $a\mathrel{\mathcal{R}}b$, then there exists one in $I$ (cf. Figure 1). Note that we do not require that all elements between $b_{1}$ and $b_{2}$ are in ${\mathrel{\mathcal{R}}}(I)$, but only those which are in the image of ${\mathrel{\mathcal{R}}}$. The second condition is symmetric: for all $a_{1}\mathrel{\mathcal{R}}b_{1}$ and $a_{2}\mathrel{\mathcal{R}}b_{2}$ with $b_{1},b_{2}\in J$, for all $a_{1}\leq_{A}a\leq_{A}a_{2}$, if there exists some $b\in{B}$ such that $a\mathrel{\mathcal{R}}b$, then there exists one in $J$.

Example 2.1**.**

For any linear order $({A},\leq)$ and partial function $f:{A}\to{A}$, if $f$ is increasing or decreasing then the relation $\{(a,f(a))\mid a\in\text{dom}(f)\}$ is interval-preserving.

As another example, consider a temporal structure $({A},\leq,\lambda)$ over a set of atomic propositions AP, where $\lambda:{A}\to 2^{\text{AP}}$ indicates the set of propositions which are true at a given point. For $P,Q\in\text{AP}$, we let $\mathsf{until}_{P,Q}=\{(a,b)\in{A}\times{A}\mid a<b\land Q\in\lambda(b)\land\forall a<c<b,P\in\lambda(c)\}$. Then $\mathsf{until}_{P,Q}$ is interval-preserving.

The following lemma states some simple closure properties of interval-preserving relations.

Lemma 2.2**.**

Let $({A},\leq_{A})$, $({B},\leq_{B})$, $({C},\leq_{C})$ be linearly ordered sets.

For all interval-preserving relation ${\mathrel{\mathcal{R}}}\subseteq{A}\times{B}$, ${\mathrel{\mathcal{R}}}^{-1}$ is interval-preserving. 2. 2.

For all interval-preserving relations ${\mathrel{\mathcal{R}}}_{1},{\mathrel{\mathcal{R}}}_{2}\subseteq{A}\times{B}$, ${\mathrel{\mathcal{R}}}_{1}\cap{\mathrel{\mathcal{R}}}_{2}$ is interval-preserving. 3. 3.

For all interval-preserving relations ${\mathrel{\mathcal{R}}}_{1}\subseteq{A}\times{B}$ and ${\mathrel{\mathcal{R}}}_{2}\subseteq{B}\times{C}$, ${\mathrel{\mathcal{R}}}_{1}\cdot{\mathrel{\mathcal{R}}}_{2}$ is interval-preserving.

Proof 2.3**.**

Part 1 follows from the fact that ${({\mathrel{\mathcal{R}}}^{-1})}^{-1}={\mathrel{\mathcal{R}}}$.

Let us prove 2. Since $({\mathrel{\mathcal{R}}}_{1}\cap{\mathrel{\mathcal{R}}_{2}})^{-1}={\mathrel{\mathcal{R}}}_{1}^{-1}\cap{\mathrel{\mathcal{R}}}_{2}^{-1}$, by symmetry, it suffices to prove that for all interval $I$ of $({A},\leq)$, $({\mathrel{\mathcal{R}}}_{1}\cap{\mathrel{\mathcal{R}}}_{2})(I)$ is an interval of $(({\mathrel{\mathcal{R}}}_{1}\cap{\mathrel{\mathcal{R}}}_{2})({A}),\leq)$. Let $a_{1},a_{2}\in I$ and $b_{1}\leq b\leq b_{2}$ such that $(a_{1},b_{1}),(a_{2},b_{2})\in({\mathrel{\mathcal{R}}}_{1}\cap{\mathrel{\mathcal{R}}}_{2})$ and $(a,b)\in({\mathrel{\mathcal{R}}}_{1}\cap{\mathrel{\mathcal{R}}}_{2})$ for some $a\in{A}$. If $a\in I$, then we are done. Otherwise, suppose for instance that $a<a_{1}\leq a_{2}$ (the other cases are similar). Since $\mathrel{\mathcal{R}}_{1}$ is interval-preserving, there exists $a_{1}\leq a^{\prime}\leq a_{2}$ such that $a^{\prime}\mathrel{\mathcal{R}}_{1}b$. Then, since $a<a_{1}\leq a^{\prime}$ and ${\mathrel{\mathcal{R}}}_{1}^{-1}(b)$ is an interval of $({\mathrel{\mathcal{R}}}_{1}^{-1}({B}),\leq_{A})$, we obtain $a_{1}\mathrel{\mathcal{R}}_{1}b$. Similarly, $a_{1}\mathrel{\mathcal{R}}_{2}b$. Hence $a_{1}\mathrel{(\mathrel{\mathcal{R}}_{1}\cap\mathrel{\mathcal{R}}_{2})}b$.

Let us show that 2 implies 3. Again, by symmetry, it suffices to prove that for all interval $I$ of $({A},\leq_{A})$, $({\mathrel{\mathcal{R}}_{1}}\cdot{\mathrel{\mathcal{R}}_{2}})(I)$ is an interval of $(({\mathrel{\mathcal{R}}_{1}}\cdot{\mathrel{\mathcal{R}}_{2}})(A),\leq_{C})$. Let ${\mathrel{\mathcal{R}}_{3}}\subseteq{B}\times{C}$ denote the relation ${\mathrel{\mathcal{R}}_{1}}({A})\times{C}$. It is an interval-preserving relation between $({B},\leq_{B})$ and $({C},\leq_{C})$. Moreover, we have $({\mathrel{\mathcal{R}}_{1}}\cdot{\mathrel{\mathcal{R}}_{2}})(A)=({\mathrel{\mathcal{R}}_{2}}\cap{\mathrel{\mathcal{R}}_{3}})(B)$. Now, let $I$ be some interval of $({A},\leq_{A})$, and $J=\{b\in{B}\mid\exists b_{1},b_{2}\in{\mathrel{\mathcal{R}}_{1}}(I),b_{1}\leq b\leq b_{2}\}$. Then $J$ is an interval of $({B},\leq_{B})$. Moreover, since $\mathrel{\mathcal{R}}_{1}$ is interval-preserving, we have ${\mathrel{\mathcal{R}}_{1}}(I)=J\cap{\mathrel{\mathcal{R}}_{1}}(A)$, hence

[TABLE]

Then, according to 2, $({\mathrel{\mathcal{R}}_{1}}\cdot{\mathrel{\mathcal{R}}_{2}})(I)$ is an interval of $(({\mathrel{\mathcal{R}}_{2}}\cap{\mathrel{\mathcal{R}}_{3}})(B),\leq_{C})$, i.e., an interval of $(({\mathrel{\mathcal{R}}_{1}}\cdot{\mathrel{\mathcal{R}}_{2}})(A),\leq_{C})$.

Models.

Let $\mathcal{P}=\{P,Q,\ldots\}$ be an infinite set of monadic predicates, and $\Gamma=\{\alpha,\beta,\ldots\}$ be a finite or infinite set of binary relation symbols. Throughout the paper, $\mathcal{M}$ will denote a structure $\mathcal{M}=(A,\leq,({\alpha}^{\mathcal{M}})_{\alpha\in\Gamma},({P}^{\mathcal{M}})_{P\in\mathcal{P}})$ where $\leq$ is a linear order over $A$, ${\alpha}^{\mathcal{M}}\subseteq A\times A$ is an interval-preserving relation for all $\alpha\in\Gamma$, and ${P}^{\mathcal{M}}\subseteq A$ for all $P\in\mathcal{P}$.

Monadic first-order logic.

We assume an infinite supply of variables $\mathcal{X}=\{x,y,\ldots\}$. The set $\textup{FO}[\Gamma,\leq]$ of monadic first-order logic formulas over $\Gamma$ is defined as follows:

[TABLE]

We assume that all formulas are interpreted over structures $\mathcal{M}$ defined as above. Given an $\textup{FO}[\Gamma,\leq]$ formula $\Phi$, we denote by $\mathsf{Free}(\Phi)$ its set of free variables. We define the satisfaction relation $\mathcal{M},\nu\models\Phi$ as usual, where $\mathcal{M}=(A,\leq,({\alpha}^{\mathcal{M}})_{\alpha\in\Gamma},({P}^{\mathcal{M}})_{P\in\mathcal{P}})$ and $\nu:\mathsf{Free}(\Phi)\to A$ is an interpretation of the free variables of $\Phi$. We say that two formulas $\Phi,\Psi\in\textup{FO}[\Gamma,\leq]$ are equivalent, written $\Phi\equiv\Psi$, if for all $\mathcal{M}=(A,\leq,({\alpha}^{\mathcal{M}})_{\alpha\in\Gamma},({P}^{\mathcal{M}})_{P\in\mathcal{P}})$ and $\nu:\mathsf{Free}(\Phi)\cup\mathsf{Free}(\Psi)\to A$, we have $\mathcal{M},\nu|_{\mathsf{Free}(\Phi)}\models\Phi$ if and only if $\mathcal{M},\nu|_{\mathsf{Free}(\Psi)}\models\Psi$.

For $k\in\mathbb{N}$, we denote by $\textup{FO}^{k}[\Gamma,\leq]$ the set of first-order formulas with at most $k$ variables. Note that a same variable may be quantified over several times in the formula.

Example 2.4**.**

Let $p:\mathbb{R}\to\mathbb{R}$ be a polynomial function, and $m_{1}<\cdots<m_{n}$ its local extrema (we suppose that $n\geq 1$). Fix $\Gamma=\{p\}$. For convenience, we will write $p(x)=y$ instead of $p(x,y)$ in $\textup{FO}[\Gamma,\leq]$ formulas. We focus on models of the form $\mathcal{M}={(\mathbb{R},\leq,{p}^{\mathcal{M}},({P}^{\mathcal{M}})_{P\in\mathcal{P}})}$ where $\leq$ is the usual ordering of the reals, and ${p}^{\mathcal{M}}=\{(x,p(x))\mid x\in\mathbb{R}\}$. Let us describe an $\textup{FO}^{3}[\Gamma,\leq]$ formula $m_{i}\leq x$ such that for all $\mathcal{M}$ and $r\in\mathbb{R}$, we have $\mathcal{M},[x\mapsto r]\models m_{i}\leq x$ if and only if $m_{i}\leq r$. First, we write $p(x)\leq p(y)$ for the $\textup{FO}^{3}[\Gamma,\leq]$ formula

[TABLE]

We can then define formulas $\min(x)\in\textup{FO}^{3}[\Gamma,\leq]$ and $\max(x)\in\textup{FO}^{3}[\Gamma,\leq]$ which state that $x$ is a local minimum (resp. maximum) of $p$, for instance:

[TABLE]

The formula $m_{i}\leq x$ then states that there exists at least $i$ local extrema before $x$, alternating existential quantifications over $y$ and $z$ to identify them; for instance, $m_{3}\leq x$ is the formula

[TABLE]

3 Star-free Propositional Dynamic Logic

Star-free Propositional Dynamic Logic.

Propositional dynamic logic (PDL) [6] consists of two sorts of formulas: state formulas which are evaluated at single elements, and path formulas which are evaluated at pairs of elements and allow to navigate inside the model. Here we consider a star-free variant of PDL (with converse). The syntax of star-free propositional dynamic logic over $\Gamma$, written $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$, is given below:

[TABLE]

where $P\in\mathcal{P}$ and $\alpha\in\Gamma$.

Compared to classical PDL, star-free PDL uses the operators $(\cdot,\cup,\cap,\mathsf{c})$ of star-free expressions, instead of the rational operators $(\cdot,\cup,\ast)$.

Let $\mathcal{M}=(A,\leq,({\alpha}^{\mathcal{M}})_{\alpha\in\Gamma},({P}^{\mathcal{M}})_{P\in\mathcal{P}})$. The semantics ${\llbracket{\varphi}\rrbracket}^{\mathcal{M}}\subseteq A$ or ${\llbracket{\pi}\rrbracket}^{\mathcal{M}}\subseteq A\times A$ of a state or path formula in $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ is defined below. The state formula $\mathop{\langle\pi\rangle}{\varphi}$ is true at a point $a\in A$ in $\mathcal{M}$ (that is, $a\in{\llbracket{\mathop{\langle\pi\rangle}{\varphi}}\rrbracket}^{\mathcal{M}}$) if there exists some $b\in A$ such that $(a,b)$ satisfies $\pi$ and $\varphi$ is true at $b$. The path formula $\{\varphi\}?$ is stationary and tests if the state formula $\varphi$ is true. The semantics of other formulas is straightforward:

[TABLE]

For simplicity, we will often write $\llbracket{\varphi}\rrbracket$ or $\llbracket{\pi}\rrbracket$ instead of ${\llbracket{\varphi}\rrbracket}^{\mathcal{M}}$ and ${\llbracket{\pi}\rrbracket}^{\mathcal{M}}$. We also write $\mathcal{M},a\models\varphi$ if $a\in{\llbracket{\varphi}\rrbracket}^{\mathcal{M}}$, and $\mathcal{M},a,b\models\pi$ if $(a,b)\in{\llbracket{\pi}\rrbracket}^{\mathcal{M}}$.

We will use the abbreviations $\mathit{true}:=P\lor\lnot P$, $\mathit{false}:=\lnot\mathit{true}$, ${\geq}:=(\leq)^{-1}$, ${<}:={\geq}^{\mathsf{c}}$, ${>}:={\leq}^{\mathsf{c}}$ and $\mathop{\langle\pi\rangle}:=\mathop{\langle\pi\rangle}{\mathit{true}}$. For all $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ formulas $\pi$, we also define a state formula $\mathsf{loop}(\pi):=\mathop{\langle\pi\cap\{\mathit{true}\}?\rangle}$ which holds at $a$ if and only if $(a,a)\in\llbracket{\pi}\rrbracket$.

Example 3.1**.**

Suppose that $\Gamma=\{+q\mid q\in\mathbb{Q}\}$, and that we consider only models over $\mathbb{R}$ and with $\llbracket{+q}\rrbracket=\{(r,r+q)\mid r\in\mathbb{R}\}$. Let $q,r\in\mathbb{Q}_{\geq 0}$ and $P,Q\in\mathcal{P}$. The formula $P\mathbin{\mathsf{U}}_{(q,r)}Q$ of metric temporal logic, which holds at time $t\in\mathbb{R}$ if there exists $t+q<t^{\prime}<t+r$ such that $t^{\prime}\in\llbracket{Q}\rrbracket$ and for all $t<t^{\prime\prime}<t^{\prime}$, $t^{\prime\prime}\in\llbracket{P}\rrbracket$, can be expressed in $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ as follows:

[TABLE]

An interval-preserving fragment of star-free PDL.

We say that a path formula $\pi\in\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ is interval-preserving if for all $\mathcal{M}$, ${\llbracket{\pi}\rrbracket}^{\mathcal{M}}$ is interval-preserving. Notice that $\leq$ and $\{\varphi\}?$ (for all $\varphi$) are interval-preserving. By Lemma 2.2 (and assumption on $\llbracket{\alpha}\rrbracket$), all $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ formulas constructed without the boolean operators $\cup$ and $\mathsf{c}$ are interval-preserving. However, the complement or the union of interval-preserving relations are not in general interval-preserving. We define below a fragment of $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ where all path formulas are interval-preserving, and which will turn out to be as expressive as $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ (and in fact, $\textup{FO}[\Gamma,\leq]$) when it comes to state formulas. To do so, we will introduce several restrictions of ${\pi}^{\mathsf{c}}$ which will turn out to be interval-preserving, and which will suffice to characterize ${\pi}^{\mathsf{c}}$.

Let us first look at the different reasons for which we may have $(a,b)\in\llbracket{{\pi}^{\mathsf{c}}}\rrbracket$, assuming that $\pi$ is interval-preserving. To begin with, we focus on $a$. One first sufficient condition for having $b\notin\llbracket{\pi}\rrbracket(a)$ is that $\llbracket{\pi}\rrbracket(a)=\emptyset$. Now, suppose $\llbracket{\pi}\rrbracket(a)\neq\emptyset$. If $\pi$ is interval-preserving, there are only three possible cases in which $b\notin\llbracket{\pi}\rrbracket(a)$: $b<\llbracket{\pi}\rrbracket(a)$, or $\llbracket{\pi}\rrbracket(a)<b$, or $\llbracket{\pi^{-1}}\rrbracket(b)=\emptyset$. We define formulas ${\mathsf{left}\leavevmode\nobreak\ }{\pi}$ and ${\mathsf{right}\leavevmode\nobreak\ }{\pi}$ corresponding respectively to the first two cases. We let

[TABLE]

Now, if we look at $\llbracket{\pi^{-1}}\rrbracket(b)$ instead of $\llbracket{\pi}\rrbracket(a)$, we can make the same observations, by symmetry: we have $(a,b)\in\llbracket{{\pi}^{\mathsf{c}}}\rrbracket$ if and only if $a\notin\llbracket{\pi^{-1}}\rrbracket(b)$, and if $\pi$ is interval-preserving, there are again only four possible cases: $\llbracket{\pi^{-1}}\rrbracket(b)=\emptyset$, or $a<\llbracket{\pi^{-1}}\rrbracket(b)$, or $a>\llbracket{\pi^{-1}}\rrbracket(b)$, or $\llbracket{\pi}\rrbracket(a)=\emptyset$.

Unfortunately, the formulas ${\mathsf{left}\leavevmode\nobreak\ }{\pi}$ and ${\mathsf{right}\leavevmode\nobreak\ }{\pi}$ are still not interval-preserving in general. However, if we take a more symmetric restriction of ${\pi}^{\mathsf{c}}$, where we look at all the possible positions of $b$ and $a$ relatively to $\llbracket{\pi}\rrbracket(a)$ and $\llbracket{\pi^{-1}}\rrbracket(b)$, we obtain four cases, illustrated in Figure 2, which we will later show correspond to interval-preserving restrictions of ${\pi}^{\mathsf{c}}$.

More precisely, let

[TABLE]

Notice that ${\pi}^{\mathsf{c3}}\equiv{({(\pi^{-1})}^{\mathsf{c2}})}^{-1}$.

Let $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,{\cap},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$ be the following restriction of $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$:

[TABLE]

Lemma 3.2**.**

All $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,{\cap},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$ formulas are interval-preserving.

Proof 3.3**.**

We proceed by induction on the formula. By assumption, $\alpha$ is interval-preserving for all $\alpha\in\Gamma$. Moreover, $\leq$ and $\{\varphi\}?$ are interval-preserving. For $\pi^{-1}$, $\pi_{1}\cdot\pi_{2}$ and $\pi_{1}\cap\pi_{2}$, we apply Lemma 2.2.

Suppose that $\pi$ is interval-preserving. Let us show that ${\pi}^{\mathsf{c1}}$ is interval-preserving. Notice that ${({\pi}^{\mathsf{c1}})}^{-1}\equiv{(\pi^{-1})}^{\mathsf{c1}}$. So we only need to show that for all intervals $I$, for all $b_{1},b_{2}\in\llbracket{{\pi}^{\mathsf{c1}}}\rrbracket(I)$ and $b_{1}\leq b\leq b_{2}$ such that $\llbracket{({\pi}^{\mathsf{c1}})^{-1}}\rrbracket(b)\neq\emptyset$, there exists $a\in I$ such that $(a,b)\in\llbracket{{\pi}^{\mathsf{c1}}}\rrbracket$. Let $a_{2}\in I$ such that $(a_{2},b_{2})\in\llbracket{{\pi}^{\mathsf{c1}}}\rrbracket$. Let us show that we can in fact take $a=a_{2}$. The proof is illustrated in the picture below.

I$$J$$a_{2}$$b_{2}$$b$$b_{1}$$\llbracket{\pi}\rrbracket(a_{2})$$<$$c$$c_{2}$$\pi^{-1}$$\pi^{-1}$$\leq$$\leq$$\leq$$<

First, we have $b\leq b_{2}<\llbracket{\pi}\rrbracket(a_{2})\neq\emptyset$. Moreover, $\llbracket{\pi^{-1}}\rrbracket(b)\neq\emptyset$ (since $\llbracket{({\pi}^{\mathsf{c1}})^{-1}}\rrbracket(b)\neq\emptyset$). Now, suppose towards a contradiction that $a_{2}\not<\llbracket{\pi^{-1}}\rrbracket(b)$. Let $c\in\llbracket{\pi^{-1}}\rrbracket(b)$ such that $c\leq a_{2}$. Since $(a_{2},b_{2})\in\llbracket{{\pi}^{\mathsf{c1}}}\rrbracket$, there exists $c_{2}>a_{2}$ such that $(b_{2},c_{2})\in\llbracket{\pi^{-1}}\rrbracket$. We then have $c\leq a_{2}<c_{2}$ and $\llbracket{\pi}\rrbracket(a_{2})\neq\emptyset$. Since $\pi$ is interval-preserving, we obtain $a_{2}\in\llbracket{\pi^{-1}}\rrbracket([b,b_{2}])$, a contradiction with the fact that $b_{2}<\llbracket{\pi}\rrbracket(a_{2})$. Thus, $(a_{2},b)\in\llbracket{{\pi}^{\mathsf{c1}}}\rrbracket$.

Let us show that ${\pi}^{\mathsf{c2}}$ is also interval-preserving. Similarly to the previous case, we show that for all $(a_{2},b_{2})\in\llbracket{{\pi}^{\mathsf{c2}}}\rrbracket$ and $b\leq b_{2}$ such that $\llbracket{({\pi}^{\mathsf{c2}})^{-1}}\rrbracket(b)\neq\emptyset$, we have $(a_{2},b)\in\llbracket{{\pi}^{\mathsf{c2}}}\rrbracket$.

I$$J$$a_{2}$$b_{2}$$b$$b_{1}$$\llbracket{\pi}\rrbracket(a_{2})$$<$$c_{2}$$c$$\leq$$\leq$$\leq$$<

First, $b\leq b_{2}<\llbracket{\pi}\rrbracket(a_{2})\neq\emptyset$, and $\llbracket{\pi^{-1}}\rrbracket(b)\neq\emptyset$. Suppose towards a contradiction that $\llbracket{\pi^{-1}}\rrbracket(b)\not<a_{2}$. Let $c\in\llbracket{\pi^{-1}}\rrbracket(b)$ such that $a_{2}\leq c$, and $c_{2}\in\llbracket{\pi^{-1}}\rrbracket(b_{2})$. We have $c_{2}<a_{2}\leq c$, and $\llbracket{\pi}\rrbracket(a_{2})\neq\emptyset$. Since $\pi$ is interval-preserving, we obtain $a_{2}\in\llbracket{\pi^{-1}}\rrbracket([b,b_{2}])$, a contradiction with the fact that $b_{2}<\llbracket{\pi}\rrbracket(a_{2})$. Symmetrically, let $J$ be an interval, $a_{1},a_{2}\in\llbracket{({\pi}^{\mathsf{c2}})^{-1}}\rrbracket(J)$, and $a_{1}\leq a\leq a_{2}$ such that $\llbracket{{\pi}^{\mathsf{c2}}}\rrbracket(a)\neq\emptyset$. Then for any $b_{1}\in J$ such that $(a_{1},b_{1})\in\llbracket{{\pi}^{\mathsf{c2}}}\rrbracket$, we also have $(a,b_{1})\in\llbracket{{\pi}^{\mathsf{c2}}}\rrbracket$, hence $a\in\llbracket{({\pi}^{\mathsf{c2}})^{-1}}\rrbracket(J)$.

Since ${\pi}^{\mathsf{c3}}\equiv{({(\pi^{-1})}^{\mathsf{c2}})}^{-1}$, this also implies that ${\pi}^{\mathsf{c3}}$ is interval-preserving.

Finally, the case of ${\pi}^{\mathsf{c4}}$ is symmetric to the case of ${\pi}^{\mathsf{c1}}$: for all $(a_{1},b_{1})\in\llbracket{{\pi}^{\mathsf{c4}}}\rrbracket$ and $b_{1}\leq b$ such that $\llbracket{({\pi}^{\mathsf{c4}})^{-1}}\rrbracket(b)\neq\emptyset$, we have $(a_{1},b)\in\llbracket{{\pi}^{\mathsf{c4}}}\rrbracket$.

4 Star-free PDL is expressively equivalent to FO

Let $\varphi$ be a state formula in $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$, and $\Phi(x)$ an $\textup{FO}[\Gamma,\leq]$ formula with a single free variable $x$. We say that $\varphi$ and $\Phi$ are equivalent, written $\varphi\equiv\Phi(x)$, if for all $\mathcal{M}$ and elements $a$ in $\mathcal{M}$, we have $\mathcal{M},a\models\varphi$ if and only if $\mathcal{M},[x\mapsto a]\models\Phi(x)$. Similarly, for a path formula $\pi\in\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ and an $\textup{FO}[\Gamma,\leq]$ formula $\Phi(x,y)$ with exactly two free variables $x$ and $y$, we write $\pi\equiv\Phi(x,y)$ if for all $\mathcal{M}$ and elements $a,b$ in $\mathcal{M}$, we have $\mathcal{M},a,b\models\pi$ if and only if $\mathcal{M},[x\mapsto a,y\mapsto b]\models\Phi(x,y)$.

From $\boldsymbol{\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]}$ to $\boldsymbol{\textup{FO}^{3}[\Gamma,\leq]}$.

An easy induction shows that any formula in $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ can be translated into an $\textup{FO}[\Gamma,\leq]$ formula which uses at most three distinct variables:

Lemma 4.1**.**

For every state formula $\varphi\in\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$, there exists a formula $\widetilde{\varphi}(x)\in\textup{FO}^{3}[\Gamma,\leq]$ such that $\varphi\equiv\widetilde{\varphi}(x)$. For every path formula $\pi\in\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$, there exists a formula $\widetilde{\pi}(x,y)\in\textup{FO}^{3}[\Gamma,\leq]$ such that $\pi\equiv\widetilde{\pi}(x,y)$.

For the other direction, we will see that the fragment $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$ of $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ defined below will be sufficient:

[TABLE]

This fragment is a restriction of $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,{\cap},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$, where the intersection is only used for $\mathsf{loop}(\pi)$ formulas.

From $\boldsymbol{\textup{FO}[\Gamma,\leq]}$ to $\boldsymbol{\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]}$.

The main result of the paper is an effective translation of $\textup{FO}[\Gamma,\leq]$ formulas into positive boolean combinations of formulas in $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$:

Theorem 4.2**.**

Every formula $\Phi\in\textup{FO}[\Gamma,\leq]$ with at least one free variable is equivalent to a positive boolean combination of formulas of the form $\widetilde{\pi}(x,y)$, where $x,y\in\mathsf{Free}(\Phi)$ and $\pi\in\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$.

Note that the equivalent formula may also contain subformulas of the form $\widetilde{\pi}(x,x)$.

Before proving Theorem 4.2, we state some of its consequences.

Corollary 4.3**.**

Every formula $\Phi\in\textup{FO}[\Gamma,\leq]$ with a single free variable is equivalent to some $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$ state formula. Every formula $\Phi\in\textup{FO}[\Gamma,\leq]$ with two free variables is equivalent to some $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ path formula.

Proof 4.4**.**

If $\Phi$ has a single free variable $x$, it is equivalent to a positive boolean combination of formulas of the form $\widetilde{\pi}(x,x)$, which are themselves equivalent to the formulas $\mathsf{loop}(\pi)$. The combination of these $\mathsf{loop}(\pi)$ formulas is then a state formula of ${\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]}$.

If $\Phi$ has two free variables $x$ and $y$, we obtain an equivalent positive boolean combination of formulas of the form $\widetilde{\pi}(x,y)$, $\widetilde{\pi}(y,x)$, $\widetilde{\pi}(x,x)$, or $\widetilde{\pi}(y,y)$. We can replace any subformula $\widetilde{\pi}(y,x)$ with $\widetilde{\pi^{-1}}(x,y)$, and any subformula $\widetilde{\pi}(x,x)$ with $\widetilde{\pi_{1}}(x,y)\lor\widetilde{\pi_{2}}(x,y)$, where $\pi_{1}=(\{\mathsf{loop}(\pi)\}?\cdot{\leq})$ and $\pi_{2}=(\{\mathsf{loop}(\pi)\}?\cdot{\geq})$, and similarly for formulas $\widetilde{\pi}(y,y)$. We obtain an equivalent positive boolean combination of formulas of the form $\widetilde{\pi}(x,y)$. Since $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ allows union and intersection of path formulas, this is equivalent to a $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ formula.

Another consequence is that $\textup{FO}[\Gamma,\leq]$ over linear orders with interval-preserving relations has the three-variable property. More precisely:

Theorem 4.5**.**

Any $\textup{FO}[\Gamma,\leq]$ formula is equivalent to a boolean combination of formulas in $\textup{FO}^{3}[\Gamma,\leq]$.

This also allows us to answer an open question from [1], namely, whether structures over the real numbers with polynomial functions have the $3$-variable property. Suppose that $\Gamma$ is a set of polynomials $p:\mathbb{R}\to\mathbb{R}$. Let $\mathcal{M}_{\Gamma}=(\mathbb{R},\leq,({p}^{\mathcal{M}_{\Gamma}})_{p\in\Gamma})$, where $\leq$ is the usual ordering of the real numbers, and ${p}^{\mathcal{M}_{\Gamma}}=\{(x,p(x))\mid x\in\mathbb{R}\}$ for all $p\in\Gamma$. Given an interpretation $h:\mathcal{P}\to 2^{\mathbb{R}}$ of the monadic predicates, we denote by $(\mathcal{M}_{\Gamma},h)$ the structure $(\mathbb{R},\leq,({p}^{\mathcal{M}_{\Gamma}})_{p\in\Gamma},(h(P))_{P\in\mathcal{P}})$. We say that two formulas $\Phi,\Psi\in\textup{FO}[\Gamma,\leq]$ are equivalent over $\mathcal{M}_{\Gamma}$, written $\Phi\equiv_{\mathcal{M}_{\Gamma}}\Psi$, if for all $h:\mathcal{P}\to 2^{\mathbb{R}}$ and $\nu:\mathsf{Free}(\Phi)\cup\mathsf{Free}(\Psi)\to\mathbb{R}$, we have $(\mathcal{M}_{\Gamma},h),\nu|_{\mathsf{Free}(\Phi)}\models\Phi$ if and only if $(\mathcal{M}_{\Gamma},h),\nu|_{\mathsf{Free}(\Psi)}\models\Psi$.

Theorem 4.6**.**

For all $\Phi\in\textup{FO}[\Gamma,\leq]$, there exists a boolean combination $\Psi$ of formulas in $\textup{FO}^{3}[\Gamma,\leq]$ such that $\Phi\equiv_{\mathcal{M}_{\Gamma}}\Psi$.

Proof 4.7**.**

Let $p\in\Gamma$, and $m_{1}<\cdots<m_{n}$ its local extrema. We denote by $p_{(-\infty,m_{1})}$, $p_{[m_{1},m_{2})},\ldots,p_{[m_{n},+\infty)}$ the (monotone) restrictions of $p$ to intervals delimitated by its local extrema, and $\Delta_{p}$ the set of these partial functions. Let $\Delta=\bigcup_{p\in\Gamma}\Delta_{p}$. As above, we let $\mathcal{M}_{\Delta}=(\mathbb{R},\leq,({p_{I}}^{\mathcal{M}_{\Delta}})_{p_{I}\in\Delta})$, where $\leq$ is the usual ordering of the real numbers, and ${p_{I}}^{\mathcal{M}_{\Delta}}=\{(x,p(x))\mid x\in I\}$. Note that ${p_{I}}^{\mathcal{M}_{\Delta}}$ is interval-preserving (cf. Example 2.1). We say that two formulas $\Phi\in\textup{FO}[\Gamma,\leq]$ and $\Psi\in\textup{FO}[\Delta,\leq]$ are equivalent, written $\Phi\equiv\Psi$, when for all $h:\mathcal{P}\to 2^{\mathbb{R}}$ and $\nu:\mathsf{Free}(\Phi)\cup\mathsf{Free}(\Psi)\to\mathbb{R}$, we have $(\mathcal{M}_{\Gamma},h),\nu|_{\mathsf{Free}(\Phi)}\models\Phi$ if and only if $(\mathcal{M}_{\Delta},h),\nu|_{\mathsf{Free}(\Psi)}\models\Psi$.

Let $\Phi\in\textup{FO}[\Gamma,\leq]$. The formula $\Psi\in\textup{FO}[\Delta,\leq]$ obtained by replacing each atomic formula $p(x,y)$ by $\bigvee_{p_{I}\in\Delta_{p}}p_{I}(x,y)$ is equivalent to $\Phi$. Applying Theorem 4.5 to $\Psi$, we obtain another formula $\Psi^{\prime}\in\textup{FO}[\Delta,\leq]$ such that $\Psi^{\prime}\equiv\Psi$ and $\Psi^{\prime}$ is a boolean combination of formulas in $\textup{FO}^{3}[\Delta,\leq]$.

Following Example 2.4, one can construct for each $p_{I}\in\Delta$ a formula “$x\in I$” of $\textup{FO}^{3}[\Gamma,\leq]$ such that $(\mathcal{M}_{\Gamma},h),\nu\models x\in I$ if and only if $\nu(x)\in I$. Consider now the formula $\Phi^{\prime}\in\textup{FO}[\Gamma,\leq]$ obtained by replacing each atomic formula $p_{I}(x,y)$ in $\Psi^{\prime}$ by $x\in I\land p(x,y)$. Then $\Phi^{\prime}\equiv\Psi^{\prime}$, hence $\Phi\equiv_{\mathcal{M}_{\Gamma}}\Phi^{\prime}$. Moreover, $\Phi^{\prime}$ is a boolean combination of formulas in $\textup{FO}^{3}[\Gamma,\leq]$.

The remainder of the section is devoted to the proof of Theorem 4.2.

Eliminating negations.

The fact that all $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$ path formulas are interval-preserving gives us a simple characterization of the complement of a path formula: we show below that an event $b$ is in $\llbracket{{\pi}^{\mathsf{c}}}\rrbracket(a)$ if it is to the left or to the right of all elements of $\llbracket{\pi}\rrbracket(a)$, or if it does not satisfy $\mathop{\langle\pi^{-1}\rangle}$. We can then show that the complement of a path formula in $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$ is equivalent to a union of path formulas in $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$. This will allow us to deal with negation in the translation from $\textup{FO}[\Gamma,\leq]$ to $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$.

Lemma 4.8**.**

For all path formulas $\pi\in\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$, ${\pi}^{\mathsf{c}}$ is equivalent to a union of $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$ formulas.

Proof 4.9**.**

We show that

[TABLE]

We denote by $\pi^{\prime}$ the right-hand-side formula. First, for all $a,b$ such that $\llbracket{\pi}\rrbracket(a)=\emptyset$ or $\llbracket{\pi^{-1}}\rrbracket(b)=\emptyset$, we have $(a,b)\in\llbracket{{\pi}^{\mathsf{c}}}\rrbracket$ and $(a,b)\in\llbracket{\pi^{\prime}}\rrbracket$. Now, suppose that $\llbracket{\pi}\rrbracket(a)\neq\emptyset$ and $\llbracket{\pi^{-1}}\rrbracket(b)\neq\emptyset$. We have $(a,b)\in\llbracket{\pi^{\prime}}\rrbracket$ if and only if $(a,b)\in\llbracket{{\pi}^{\mathsf{c1}}\cup{\pi}^{\mathsf{c2}}\cup{\pi}^{\mathsf{c3}}\cup{\pi}^{\mathsf{c4}}}\rrbracket$. Clearly, if $(a,b)\in\llbracket{{\pi}^{\mathsf{c1}}\cup{\pi}^{\mathsf{c2}}\cup{\pi}^{\mathsf{c3}}\cup{\pi}^{\mathsf{c4}}}\rrbracket$, then $(a,b)\in\llbracket{{\pi}^{\mathsf{c}}}\rrbracket$. Conversely, let us show that if $(a,b)\notin\llbracket{{\pi}^{\mathsf{c1}}\cup{\pi}^{\mathsf{c2}}\cup{\pi}^{\mathsf{c3}}\cup{\pi}^{\mathsf{c4}}}\rrbracket$ then $(a,b)\in\llbracket{\pi}\rrbracket$. In that case, we have either $a_{1}\leq a\leq a_{2}$ for some $a_{1},a_{2}\in\llbracket{\pi^{-1}}\rrbracket(b)$, or $b_{1}\leq b\leq b_{2}$ for some $b_{1},b_{2}\in\llbracket{\pi}\rrbracket(a)$. Since $\pi$ is interval-preserving, we obtain $(a,b)\in\llbracket{\pi}\rrbracket$.

Existential quantification.

The elimination of existential quantifiers relies on the simple lemma below:

Lemma 4.10**.**

Let $(A,\leq)$ be a linearly ordered set, and $I_{1},\ldots,I_{n}$ intervals of $(A,\leq)$. Then $\bigcap_{1\leq i\leq n}I_{i}\neq\emptyset$ if and only if for all $1\leq i,j\leq n$, $I_{i}\cap I_{j}\neq\emptyset$.

Proof 4.11**.**

We show that there exists $k$ and $\ell$ such that $\bigcap_{1\leq i\leq n}I_{i}=I_{k}\cap I_{\ell}$, which implies the result. We define relations $\sqsubseteq_{\textup{left}}$ and $\sqsubseteq_{\textup{right}}$ over $\{I_{1},\ldots,I_{n}\}$ which, intuitively, compare respectively the left and right bounds of the intervals:

[TABLE]

It is easy to check that $\sqsubseteq_{\textup{left}}$ and $\sqsubseteq_{\textup{right}}$ are transitive, an that for all $I$ and $J$, we have $I\sqsubseteq_{\textup{left}}J$ or $J\sqsubseteq_{\textup{left}}I$ (or both), and similarly for $\sqsubseteq_{\textup{right}}$. Thus, there exists $k$ such that $I_{i}\sqsubseteq_{\textup{left}}I_{k}$ for all $i$, and $\ell$ such that $I_{\ell}\sqsubseteq_{\textup{right}}I_{i}$ for all $i$. Then for all $a\in I_{k}\cap I_{\ell}$, for all $i$, there exists $b,b^{\prime}\in I_{i}$ such that $b\leq a\leq b^{\prime}$. Since $I_{i}$ is an interval, we obtain $a\in I_{i}$. Hence $I_{k}\cap I_{\ell}=\bigcap_{1\leq i\leq n}I_{i}$.

The next lemma follows from an application of Lemma 4.10 to intervals of the form $\llbracket{\pi_{i}}\rrbracket(a_{i})$.

Lemma 4.12**.**

Let $n\geq 1$. For all path formulas $\pi_{1},\ldots,\pi_{n}$ and all state formulas $\varphi$ in $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$, the $\textup{FO}[\Gamma,\leq]$ formula

[TABLE]

is equivalent to a positive boolean combination of formulas of the form $\widetilde{\pi}(x_{j},x_{k})$, with $1\leq j,k\leq n$ and $\pi\in\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$.

Proof 4.13**.**

Let $\psi=\varphi\land\bigwedge_{1\leq i\leq n}\mathop{\langle\pi_{i}^{-1}\rangle}$, and

[TABLE]

Notice that $\mathsf{Free}(\Psi)=\mathsf{Free}(\Phi)=\{x_{1},\ldots,x_{n}\}$.

Let us show that $\Phi\equiv\Psi$. Let $\mathcal{M}=(A,\leq,({\alpha}^{M})_{\alpha\in\Gamma},({P}^{M})_{P\in\mathcal{P}})$, and $\nu:\{x_{1},\ldots,x_{n}\}\to A$. For all $1\leq i\leq n$, let $I_{i}=\llbracket{\pi_{i}}\rrbracket(\nu(x_{i}))\cap\llbracket{\psi}\rrbracket$. Let us show that $I_{i}$ is an interval of $(\llbracket{\psi}\rrbracket,\leq)$. First, since $\pi_{i}$ is interval-preserving, $\llbracket{\pi_{i}}\rrbracket(\nu(x_{i}))$ is an interval of $(\llbracket{\mathop{\langle\pi_{i}^{-1}\rangle}}\rrbracket,\leq)$. Thus, $I_{i}$ is an interval of $(\llbracket{\mathop{\langle\pi_{i}^{-1}\rangle}}\rrbracket\cap\llbracket{\psi}\rrbracket,\leq)$. But since $\llbracket{\mathop{\langle\pi_{i}^{-1}\rangle}}\rrbracket\subseteq\llbracket{\psi}\rrbracket$, this is simply $(\llbracket{\psi}\rrbracket,\leq)$. Besides, it is easy to verify that

[TABLE]

Applying Lemma 4.10, we obtain

[TABLE]

Translation from $\boldsymbol{\textup{FO}[\Gamma,\leq]}$ to $\boldsymbol{\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]}$.

We are now ready to give the proof of Theorem 4.2.

Proof 4.14** (Proof of Theorem 4.2).**

We assume that $\Phi$ is in prenex normal form, and prove the result by induction. The translation of atomic formulas $x\leq y$ or $\alpha(x,y)$ is straightforward; moreover, $P(x)\equiv\widetilde{\{P\}?}(x,x)$, and $(x=y)\equiv\widetilde{\{true\}?}(x,y)$. Using Lemma 4.8 to eliminate negations, we obtain the result for all quantifier-free formulas.

The case $\Phi=\forall x.\Psi\equiv\lnot\exists x.\lnot\Psi$ reduces to the case of existential quantification, applying again Lemma 4.8 to eliminate negations.

We are left with the case $\Phi=\exists x.\Psi$. If $x$ is not free in $\Psi$, then $\Phi\equiv\Psi$ (since $\Psi$ has at least one free variable) and we are done by induction. Otherwise, assume that $\mathsf{Free}(\Psi)=\{x_{1},\ldots,x_{n}\}$ with $n>1$ and $x=x_{n}$. By induction, $\Psi$ is equivalent to a positive boolean combination of formulas of the form $\widetilde{\pi}(x_{i},x_{j})$ with $\pi\in\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$. We replace $\widetilde{\pi}(x_{i},x_{j})$ with $\widetilde{\pi^{-1}}(x_{j},x_{i})$ whenever $j<i$, and bring the resulting formula into disjunctive normal form. Each conjunct is then of the form $\Upsilon=\Upsilon_{1}\land\Upsilon_{2}\land\Upsilon_{3}$, where $\Upsilon_{1}$ uses only variables from $\{x_{1},\ldots,x_{n-1}\}$, $\Upsilon_{2}=\bigwedge_{i}\widetilde{\pi_{i}}(y_{i},x)$ with $y_{i}=x_{j}$ for some $1\leq j<n$, and $\Upsilon_{3}=\bigwedge_{j}\widetilde{\pi_{j}}(x,x)$. Note that $\Upsilon_{3}\equiv\widetilde{\varphi}(x)$, where $\varphi=\bigwedge_{j}\mathsf{loop}(\pi_{j})$. Then $\exists x.\Psi$ is equivalent to a finite disjunction of formulas

[TABLE]

with $\Upsilon_{1}$ and $\Upsilon_{2}$ as above. If $\Upsilon_{2}$ is empty, then we replace $\exists x.\widetilde{\varphi}(x)$ with the formula

[TABLE]

Otherwise, we apply Lemma 4.12 to $\exists x.\left(\Upsilon_{2}\land\widetilde{\varphi}(x)\right)$. In all cases, we obtain an equivalent formula which is a positive boolean combination of formulas $\widetilde{\pi}(x_{i},x_{j})$ with $1\leq i,j<n$ and $\pi\in\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$.

Remark 4.15**.**

Without the assumption that all atomic binary relations are interval-preserving, $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ is still equivalent to $\textup{FO}^{3}[\Gamma,\leq]$. Indeed, in the proof of Theorem 4.2, the assumption that all atomic binary relations are interval-preserving is only used in Lemmas 4.8 and 4.12. But this assumption is not needed in the proof of Lemma 4.12 if $\Phi$ uses only three variables $x$, $y$ and $z$. Indeed, we then have $\Phi\equiv\widetilde{(\pi\cdot\{\varphi\}?\cdot\pi^{\prime-1})}(y,z)$, where $\pi$ is the intersection of all $\pi_{i}$ such that $x_{i}=y$, and $\pi^{\prime}$ is the intersection of all $\pi_{i}$ such that $x_{i}=z$. Moreover, Lemma 4.8 is no longer needed if we translate an $\textup{FO}^{3}[\Gamma,\leq]$ formula into a positive boolean combination of $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ formulas, since $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ allows to take the complement of a path formula. Note that the equivalence with $\textup{FO}^{3}[\Gamma,\leq]$ is already proven in [28] (for the calculus of relations).

5 Conclusion

We proved that every $\textup{FO}[\Gamma,\leq]$ formula over linear orders with interval-preserving binary relations can be translated into an equivalent positive boolean combination of path formulas in $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq,\mathsf{loop},\mathsf{c1},\mathsf{c2},\mathsf{c3},\mathsf{c4}]$. In particular, any $\textup{FO}[\Gamma,\leq]$ formula is equivalent to a boolean combination of formulas in $\textup{FO}^{3}[\Gamma,\leq]$, which shows that $\textup{FO}[\Gamma,\leq]$ has the three-variable property. This generalizes several known results.

It would be interesting to see if the equivalence between $\textup{FO}[\Gamma,\leq]$ and $\textup{PDL}_{\mathsf{sf}}[\Gamma,\leq]$ can be used as an intermediate step to prove that a temporal logic is expressively complete. It is not the case in general, since [13] provides an example of a class of structures which fits our assumptions but does not admit any expressively complete temporal logic. However, the equivalence could still be useful in more restricted settings.