AN ORDERED STRUCTURE OF RANK TWO RELATED TO DULAC’S PROBLEM

A. DOLICH AND P. SPEISSEGGER

Abstract. For a vector field ξ on ℝ^{2} we construct, under certain assumptions on ξ, an ordered model-theoretic structure associated to the flow of ξ. We do this in such a way that the set of all limit cycles of ξ is represented by a definable set. This allows us to give two restatements of Dulac’s Problem for ξ—that is, the question whether ξ has finitely many limit cycles—in model-theoretic terms, one involving the recently developed notion of U^{þ}-rank and the other involving the notion of o-minimality.

Introduction

Let ξ = a_{1} \frac{∂}{∂x} + a_{2} \frac{∂}{∂y} be a vector field on ℝ^{2} of class C^{1}, and let

S(ξ) := {(x, y) ∈ ℝ^{2} : a_{1}(x, y) = a_{2}(x, y) = 0}

be the set of singularities of ξ. By the existence and uniqueness theorems for ordinary differential equations (see Camacho and Lins Neto [1, p. 28] for details), ξ induces a C^{1}-foliation F^{ξ} on ℝ^{2} \ S(ξ) of dimension 1. Abusing terminology, we simply call a leaf of this foliation a leaf of ξ. A cycle of ξ is a compact leaf of ξ; a limit cycle of ξ is a cycle L of ξ for which there exists a non-compact leaf L′ of ξ such that L is contained in the closure of L′.

Dulac’s Problem is the following statement: “if ξ is polynomial, then ξ has finitely many limit cycles”. It is a weakening of the second part of Hilbert’s 16th problem, which states that “there is a function H : ℕ ⟶ ℕ such that for all d ∈ ℕ, if ξ is polynomial of degree d then ξ has at most H(d) limit cycles”. Both problems have an interesting history, and while Dulac’s problem was independently settled in the 1990s by Ecalle [3] and Ilyashenko [5], Hilbert’s 16th problem remains open; see [5] for more details.

In this paper, we attempt to reformulate Dulac’s Problem in model-theoretic terms. Our motivation to do so is twofold: we want to (i) find a model-theoretic structure naturally associated to ξ in which the flow of ξ and the set of limit cycles of ξ are represented by definable sets;

Date: February, 2006; Preprint.

1991 Mathematics Subject Classification. 37C27, 03C64.

Key words and phrases. Vector fields, limit cycles, model theory, ordered structures.

Supported in parts by NSERC and NSF.

(ii) know to what extent the geometry of such a structure is determined by Dulac’s Problem.

Our starting point for (i) is motivated by the piecewise triviality of Rolle foliations associated to analytic 1-forms as described by Chazal [2]. Let U ⊆ ℝ^{2} be open; a leaf L of ξ|_{U} is a Rolle leaf of ξ|_{U} if for every C^{1}-curve δ : [0, 1] ⟶ U with δ(0) ∈ L and δ(1) ∈ L, there is a t ∈ [0, 1] such that δ′(t) is tangent to ξ(δ(t)). Based on Khovanskii theory [6] over an o-minimal expansion of the real field [12], we establish (Proposition 1.5 and Theorem 3.4):

Theorem A. Assume that ξ is definable in an o-minimal expansion of the real field. Then there is a cell decomposition C of ℝ^{2} compatible with S(ξ) such that, with C_{reg} := {C ∈ C : C ∩ S(ξ) = ∅},

(1) every 1-dimensional C ∈ C_{reg} is either transverse to ξ or tangent to ξ;

(2) for every open C ∈ C_{reg}, every leaf of ξ|_{C} is a Rolle leaf of ξ|_{C};

(3) for every open C ∈ C_{reg}, the flow of ξ in C is represented by a lexicographic ordering of C.

Part (3) of this theorem needs some explanation, as it represents our understanding of the “triviality” of the flow of ξ in C. Given an open C ∈ C_{reg}, it follows from part (2) that the direction of ξ induces a linear ordering <_{Γ} on every leaf L of ξ|_{C}. We can furthermore define a relation on the set L(C) of all leaves of ξ|_{C} as follows: given a leaf L of ξ|_{C}, the fact that L is a Rolle leaf of ξ|_{C} implies (see Remark 1.2 below) that L separates C \ L into two connected components U_{L,1} and U_{L,2} such that the vector ξ^{⊥}(z) := (a_{2}(z), −a_{1}(z)) points into U_{L,2} for all z ∈ L. Thus, for a leaf L′ of ξ|_{C} different from L, we define L ≪_{C} L′ if L′ ⊆ U_{L,2} and L′ ≪_{C} L if L′ ∈ U_{L,1}. In general, though, the relation ≪_{C} does not always define an ordering, even if every leaf of ξ|_{C} is Rolle; see Example 2.2 below.

Part (3) now means that the cell decomposition C may be chosen in such a way that for every open C ∈ C_{reg}, the ordering ≪_{C} on L(C) is a linear ordering. (See Example 3.2 for such a decomposition in the situation of Example 2.2.) This leads to lexicographic orderings as follows: given C ∈ C_{reg} and z ∈ C, we denote by L_{z} the leaf of ξ|_{C} containing z. If C ∈ C_{reg} is open, we define a linear ordering <_{C} on C by x <_{C} y if and only if either L_{x} ≪_{C} L_{y}, or L_{x} = L_{y} and x <_{L_{x}} y. Letting E_{C} be a set of representatives of L(C), it is not hard to see that the structures (C, <_{C}, E_{C}) and (ℝ^{2}, <_{lex}, {y = 0}) are isomorphic, where <_{lex} is the usual lexicographic ordering of ℝ^{2}.

To complete the picture, we also define an ordering <_{C} on each 1-dimensional C ∈ C_{reg}: if C is tangent to ξ, we let <_{C} be the linear ordering induced on C by the direction of ξ, and if C is transverse to ξ, we let <_{C} be the linear ordering induced on C by the direction of ξ^{⊥}. For each open C ∈ C_{reg}, we also let <_{E_{C}} be the restriction of <_{C} to E_{C}. Each of these orderings induces a topology on the corresponding set that makes it homeomorphic to the real line. Finally, for each 1-dimensional C ∈ C_{reg} tangent to ξ, we fix an element e_{C} ∈ C.

In the situation of Theorem A, we reconnect the pieces of C according to the flow of ξ as follows: let B be the union of

• all 1-dimensional cells in C_{reg} transverse to ξ,

• the sets E_{C} for all open cells C ∈ C_{reg},

• all 0-dimensional cells in C_{reg}, and

• the singletons {e_{C}} for all 1-dimensional C ∈ C_{reg} tangent to ξ.

We define the forward progression map 𝔣 : B ∪ {∞} ⟶ B ∪ {∞} by (roughly speaking) putting 𝔣(x) equal to the next point in B on the leaf of ξ through x if x ≠ ∞ and if such a point exists, and otherwise we put 𝔣(x) := ∞. In this situation, a point x ∈ B belongs to a cycle of ξ if and only if there is a nonzero n ∈ ℕ such that 𝔣^{n}(x) = x, where 𝔣^{n} denotes the n-th iterate of 𝔣.

In fact, only finitely many iterates of 𝔣 are necessary to capture all cycles of ξ (Proposition 5.3): since a cycle of ξ is a Jordan curve in ℝ^{2}, it is a Rolle leaf of ξ and therefore intersects each C ∈ C of dimension at most 1 in at most one connected component. Hence there is an N ∈ ℕ such that for all x ∈ B, x belongs to a cycle of ξ if and only if 𝔣^{N}(x) = x.

To see how we can use this to detect limit cycles of certain ξ, we first define a cycle L of ξ to be a boundary cycle, if for every x ∈ L and every neighborhood V of x, the set V intersects some non-compact leaf of ξ. One of Poincaré’s theorems [10] (see also Perko [9, p. 217]) implies that if ξ is real analytic, then the limit cycles of ξ are exactly the boundary cycles of ξ. On the other hand, it follows from the previous paragraph that for every x ∈ B, the point x belongs to a boundary cycle of ξ if and only if x is in the boundary (relative to B considered with the topology induced on it by the various orderings defined above) of the set of all fixed points of 𝔣^{N}.

Based on the observations mentioned in the preceding paragraphs (and a few related observations), we associate to each decomposition C as in Theorem A a flow configuration Φ_{ξ} = Φ_{ξ}(C) of ξ, intended to code how the cells in C are linked together by the flow of ξ. To each flow configuration Φ, we associate in turn a unique first-order language L(Φ), in such a way that the situation described in the preceding paragraphs naturally yields an L(Φ_{ξ})-structure M_{ξ} in which the lexicographic orderings of Theorem A, the associated forward progression map 𝔣 : B ∪ {∞} ⟶ B ∪ {∞} and the set of all x ∈ B that belong to some boundary cycle of ξ are definable.

If, in the situation of Theorem A, there is an open C ∈ C_{reg}, then the induced structure on C in M_{ξ} is not o-minimal (because the structure (C, <_{C}, E_{C}) described above is definable in M_{ξ}). Thus, to answer (ii) we need to work with notions weaker than o-minimality. A natural weakening that includes lexicographic orderings is provided by the rosy ordered theories introduced by Onshuus [8]: the theory T_{lex} of the structure (ℝ^{2}, <_{lex}, {y = 0}) is rosy of U^{þ}-rank two, while every o-minimal structure is rosy of U^{þ}-rank one. (We refer the reader to [8] for the relevant definitions; for a structure M, we write U^{þ}(M) for the U^{þ}-rank of the theory of M.)

Note that our discussion above implies U^{þ}(M_{ξ}) ≥ 2. The main result of this paper is the following restatement of Dulac’s problem:

Theorem B. Assume that ξ is definable in an o-minimal expansion of the real field, and let M_{ξ} be the L(Φ_{ξ})-structure associated to some flow configuration Φ_{ξ} of ξ. Then

(1) ξ has finitely many boundary cycles if and only if U^{þ}(M_{ξ}) = 2;

(2) if ξ is real analytic, then ξ has finitely many limit cycles if and only if U^{þ}(M_{ξ}) = 2.

The proof of Theorem B is lengthy, but straightforward: we prove that M_{ξ} admits quantifier elimination in a certain expanded language (Theorem 9.11). The main ingredient in this proof is a reduction—modulo the theory of M_{ξ} in the expanded language, roughly speaking—of general quantifier-free formulas to certain quantifier-free order formulas, which allows us to deduce the quantifier elimination for M_{ξ} from quantifier elimination of the theory of (ℝ^{2}, <_{lex}, {y = 0}, π), where π : ℝ^{2} ⟶ {y = 0} is the canonical projection on the x-axis. Under the assumption of having only finitely many boundary cycles, the new predicates of the expanded language are easily seen to define subsets of the various cells obtained by Theorem A that are finite unions of points and intervals. Theorem B then follows by general U^{þ}-rank arguments.

As a corollary of Theorem B, Ecalle’s and Ilyashenko’s solutions of Dulac’s Problem imply the following:

Corollary. Assume that ξ is polynomial, and let M_{ξ} be the L(Φ_{ξ})-structure associated to some flow configuration Φ_{ξ} of ξ. Then U^{þ}(M_{ξ}) = 2. □

It remains an open question whether, in the situation of the corollary, the structures are definable in some o-minimal expansion of the real line. An answer to this question, however, seems to go far beyond our current knowledge surrounding Dulac’s Problem.

Finally, our proof of Theorem B gives rise to a second restatement of Dulac’s problem that does not involve U^{þ}-rank: let G be the union of all 1-dimensional C ∈ C_{reg} that are transverse to ξ, all 0-dimensional C ∈ C_{reg} and {∞}. Let G_{ξ} be the expansion of G by all corresponding orderings <_{C} and by the map 𝔣^{2}|_{G}. (Note that 𝔣^{2}|_{G} maps G into G.) We may view G_{ξ} as a graph whose vertices are the elements of G and whose edges are defined by 𝔣^{2}.

Theorem C. Assume that ξ is definable in an o-minimal expansion of the real field, and let G_{ξ} be as above. Then

(1) ξ has finitely many boundary cycles if and only if the structure induced by G_{ξ} on each 1-dimensional C ⊆ G is o-minimal;

(2) if ξ is real analytic, then ξ has finitely many limit cycles if and only if the structure induced by G_{ξ} on each 1-dimensional C ⊆ G is o-minimal.

Our paper is organized as follows: in Sections 1–5, we establish Theorem A and its consequences. Based on the latter, we define the notion of a flow configuration and the associated first-order language in Section 6, where we also give an axiomatization of the crucial properties satisfied by the models M_{ξ} above. Some basic facts about the iterates of the forward progression map are deduced from these axioms in Section 7. In Section 8, we extend our axioms to reflect the additional assumption that there are only finitely many boundary cycles, and we introduce additional predicates for certain definable sets related to the sets of fixed points of the iterates of the forward progression map. The quantifier elimination result is then given in Section 9, and we prove Theorems C and B in Section 10. We finish with a few questions and remarks in Section 11. Acknowledgements. We thank Lou van den Dries and Chris Miller for their suggestions and comments on the earlier versions of this paper. Global conventions. We fix an o-minimal expansion R of the real field; “definable” means “definable in R with parameters”.

For 1 ≤ m ≤ n, we denote by Π_{m} : ℝ^{n} ⟶ ℝ^{m} the projection on the first m coordinates.

Given (x, y) ∈ ℝ^{2}, we put (x, y)^{⊥} := (y, −x).

For a subset A ⊆ ℝ^{n}, we let cl(A), int(A), bd(A) := cl(A) \ int(A) and fr(A) := cl(A) \ A denote the topological closure, interior, boundary and frontier, respectively.

For n ∈ ℕ, we define the analytic diffeomorphism ϕ_{n} : ℝ^{n} ⟶ (−1, 1)^{n} by ϕ_{n}(x_{1}, …, x_{n}) := (x_{1}/\sqrt{1 + x_{1}^{2}}, …, x_{n}/\sqrt{1 + x_{n}^{2}}) . Given X ⊆ ℝ^{n}, we write X^{∗} := ϕ_{n}(X), and given a vector field η on ℝ^{n} of class C^{1}, we write η^{∗} for the push-forward (ϕ_{n})_{∗} η of η to (−1, 1)^{n}.

1. Rolle decomposition

Let U ⊆ ℝ^{2} be open and p ≥ 1 be an integer. Let ξ = a_{1} \frac{∂}{∂x} + a_{2} \frac{∂}{∂y} be a definable vector field on U of class C^{p} (that is, the functions a_{1}, a_{2} : U ⟶ ℝ are definable and of class C^{p}), and let

S(ξ) := {z ∈ U : a_{1}(z) = a_{2}(z) = 0}

be the set of singularities of ξ. By the existence and uniqueness theorems for ordinary differential equations [1, p. 28], ξ induces a C^{p}-foliation F^{ξ} on U \ S(ξ) of dimension 1. Abusing terminology, we simply call a leaf of this foliation a leaf of ξ.

Remark. Put ω := a_{2}dx − a_{1}dy; then S(ξ) is the set of singularities of ω, and the foliation F^{ξ} is exactly the foliation on U \ S(ξ) defined by the equation ω = 0. Below, we will use this observation (mainly in connection with some citations) without further mention.

Definition 1.1. Let γ : I ⟶ U of class C^{p}, where I ⊆ ℝ is an interval. We call γ a C^{p}-curve in U and usually write Γ := γ(I). If t ∈ I is such that ξ^{⊥}(γ(t)) · γ′(t) ≠ 0, we say that γ is transverse to ξ at t; otherwise, γ is tangent to ξ at t. The curve γ is transverse (tangent) to ξ if γ is transverse (tangent) to ξ at every t ∈ I.

A leaf L of ξ is a Rolle leaf of ξ if for every C^{1}-curve γ : [0, 1] ⟶ U with γ(0) ∈ L and γ(1) ∈ L, there is a t ∈ [0, 1] such that ξ^{⊥}(γ(t)) · γ′(t) = 0.

A cycle of ξ is a compact leaf of ξ. A cycle L of ξ is a limit cycle of ξ if there is a non-compact leaf L′ of ξ such that L ⊆ cl(L′). A cycle L of ξ is a boundary cycle of ξ if for every open set V ⊆ ℝ^{2} with V ∩ L ≠ ∅, there is a non-compact leaf L′ of ξ such that V ∩ L′ ≠ ∅.

Remark 1.2. Since ξ is integrable in U \ S(ξ), every Rolle leaf L of ξ is an embedded submanifold of U \ S(ξ) that is closed in U \ S(ξ). In particular, by Theorem 4.6 and Lemma 4.4 of Chapter 4 in [4], if U \ S(ξ) is simply connected, then U \ (S(ξ) ∪ L) has exactly two connected components such that L is equal to the boundary in U \ S(ξ) of each of these components.

Lemma 1.3 (Khovanskii [6]). (1) Assume that U \ S(ξ) is simply connected, and let L ⊆ U \ S(ξ) be an embedded leaf of ξ that is closed in U \ S(ξ). Then L is a Rolle leaf of ξ in U.

(2) Let L be a cycle of ξ. Then L is a Rolle leaf of ξ.

Sketch of proof. (1) Arguing as in the preceding remark, the set U \ S(ξ) has exactly two connected components U_{1} and U_{2}, such that bd(U_{i})∩(U \S(ξ)) = L for i = 1, 2. The argument of Example 1.3 in [12] now shows that L is a Rolle leaf of ξ.

(2) Since L is compact, L is an embedded and closed submanifold of ℝ^{2}. Now conclude as in part (1). □

Definition 1.4. We call ξ Rolle if S(ξ) = ∅, ξ is of class C^{1} and every leaf of ξ is a Rolle leaf of ξ.

We now let C be a C^{p}-cell decomposition of ℝ^{2} compatible with U and S(ξ), and we put C_{U} := {C ∈ C : C ⊆ U}. Refining C, we may assume that ξ|_{C} is of class C^{p} for every C ∈ C_{U}, and that every C ∈ C_{U} of dimension 1 is either tangent or transverse to ξ. Refining C again, we also assume that

(I) a_{1} and a_{2} have constant sign on every C ∈ C_{U}. Such a decomposition C is called a Rolle decomposition for ξ, because of the following:

Proposition 1.5. Let C ∈ C_{U} be open such that C ∩ S(ξ) = ∅. Then ξ|_{C} is Rolle. Moreover, if both a_{1} and a_{2} have nonzero constant sign on C, then either every leaf of ξ|_{C} is the graph of a strictly increasing C^{p} function f : I ⟶ ℝ, or every leaf of ξ|_{C} is the graph of a strictly decreasing C^{p}-function f : I ⟶ ℝ, where I ⊆ ℝ is an open interval depending on f.

Proof. If a_{1}|_{C} = 0 or a_{2}|_{C} = 0, the conclusion is obvious. So we assume that a_{1}|_{C} and a_{2}|_{C} have constant positive sign, say; the remaining three cases are handled similarly. Let L be a leaf of ξ|_{C}; we claim that L is the graph of a strictly increasing C^{p}-function f : I ⟶ ℝ, where I := Π_{1}(L).

To see this, assume first that there are x, y_{1}, y_{2} ∈ ℝ such that (x, y_{i}) ∈ L for i = 1, 2 and y_{1} ≠ y_{2}. Since ξ|_{C} is of class C^{p}, the leaf L is a C^{p}-curve, so by Rolle’s Theorem, there is an a ∈ L such that L is tangent at a to ∂/∂y. But this means that a_{1}(a) = 0, a contradiction. Thus, L is the graph of a strictly increasing C^{p}-function f : I ⟶ ℝ.

It follows from the claim that L is an embedded submanifold of C and, since C ∩ S(ξ) = ∅, that L is a closed subset of C. Thus by Lemma 1.3(1), L is a Rolle leaf of ξ|_{C}. □

2. Rolle foliations and Hausdorff limits of Rolle leaves

We continue working with ξ as in Section 1, and we fix a Rolle decomposition C for ξ. We fix an open C ∈ C_{U} such that C ∩ S(ξ) = ∅.

To simplify notation, we write ξ in place of ξ|_{C} throughout this section. Let L be a leaf of ξ. Since L is a Rolle leaf of ξ, C \ L has two connected

components U_{L,1} and U_{L,2}, and L is the boundary of U_{L,i} in C for i = 1, 2. Since ξ^{⊥}(z) ≠ (0, 0) for all z ∈ C and L is connected, there is an i ∈ {1, 2} such that ξ^{⊥}(z) points inside U_{L,i} for all z ∈ L; reindexing if necessary, we may assume that ξ^{⊥}(z) points inside U_{L,2} for every leaf L of ξ.

Definition 2.1. For a point z ∈ C, we let L_{z}^{ξ} be the unique leaf of ξ such that z ∈ L_{z}^{ξ}. For any subset X ⊆ C, we define

F^{ξ}(X) := ⋃_{z∈X} L_{z}^{ξ},

called the ξ-saturation of X, and we put

L^{ξ}(X) := {L_{z}^{ξ} : z ∈ X} .

For X ⊆ C, we define a relation ≪_{X}^{ξ} on the set L^{ξ}(X) as follows: L ≪_{X}^{ξ} M if and only if L ⊆ U_{M,1} (if and only if M ⊆ U_{L,2}).

Whenever ξ is clear from context, we omit “ξ” in the definitions and notations above.

Note that in general the relation ≪_{C} may not define an order relation on L(C):

Example 2.2. Let ζ := −y \frac{∂}{∂x} + x\frac{∂}{∂y}, and let g : ℝ^{2} ⟶ ℝ be defined by g(x, y) := (y − (x − 2))^{2}. Then gζ is a real analytic vector field on ℝ^{2} and S(gζ) = {0} ∪ {(x, y) : y = x − 1}. Let also C be the cell (α, β), where α, β : (0, 1) ⟶ ℝ are defined by α(x) := x − 2 and β(x) := x − 1.

Then C ∩ S(gζ) = ∅, and since every leaf of ζ is a Rolle leaf of ζ, the vector field gζ|_{C} is Rolle. However, ≪_{C}^{gζ} is not an ordering of L(C): pick a leaf L of ξ (that is, a circle with center (0, 0)) such that L ∩ gr(α) contains two points. Then L ∩ C consists of two distinct leaves L_{1} and L_{2} of gζ|_{C}. Since ζ^{⊥}(z) points outside the circle L for every z ∈ L, we get L_{1} ⊆ U_{L_{2},1} and L_{2} ⊆ U_{L_{1},1}, that is, L_{1} ≪_{C}^{gζ} L_{2} and L_{2} ≪_{C}^{gζ} L_{1}.

However, for certain X the relation ≪_{X} is a linear ordering of L(X), as discussed in the following lemma. For a curve γ : I ⟶ C, we write

L(t) := L_{γ(t)} for all t ∈ I;

in this situation, we have F (Γ) = ⋃_{t∈I} L(t).

Lemma 2.3. Let γ : I ⟶ C be a C^{p}-curve transverse to ξ, where I ⊆ ℝ is an interval.

(1) If I is open, then F (Γ) is open.

(2) The relation ≪_{Γ} is a linear ordering of L(Γ), and the map t ↦ L(t) : I ⟶ L(Γ) is order-preserving if ξ^{⊥}(γ(t)) · γ′(t) > 0 for all t ∈ I and order-reversing if ξ^{⊥}(γ(t)) · γ′(t) < 0 for all t ∈ I.

Proof. (1) Assume that I is open, and let t ∈ I. Because ξ is C^{p} and nonsingular and γ is transverse to ξ, by Picard’s Theorem there is an open set B_{t} ⊆ C containing γ(t) such that B_{t} ⊆ F (Γ). Put B := ⋃_{t∈I} B_{t}; then Γ ⊆ B ⊆ F (Γ), so F (Γ) = F (B). Since B is open, it follows from Theorem III.1 in [1] that F (Γ) is open.

(2) Since γ is transverse to ξ and each L(t) is Rolle, the map t ↦ L(t) : I ⟶ L(Γ) is injective. It therefore suffices to show that either

s < t ⇔ L(s) ≪_{Γ} L(t) for all s, t ∈ I,

or

s < t ⇔ L(t) ≪_{Γ} L(s) for all s, t ∈ I.

Since γ is transverse to ξ, the continuous map t ↦ ξ^{⊥}(γ(t)) · γ′(t) : I ⟶ ℝ has constant positive or negative sign. Assume it has constant positive sign; the case of constant negative sign is handled similarly. Then for every t ∈ I, the set

Γ_{<t} := {γ(s) : s ∈ I, s < t}

is contained in U_{L(t),1}. Hence L(s) ⊆ U_{L(t),1} for all s ∈ I with s < t, that is, L(s) ≪_{Γ} L(t) for all s ∈ I with s < t. Similarly, L(t) ≪_{Γ} L(s) for all s ∈ I with s > t, and since t ∈ I was arbitrary, the lemma follows. □

We assume for the rest of this section that C is bounded. Let ξ_{C} be the 1-form on C defined by

ξ_{C} := \frac{ξ|_{C}}{∥ξ|_{C}∥}.

Then ξ_{C} is a bounded, definable C^{p}-map on C, so by o-minimality, there is a finite set F_{C} ⊆ fr(C) such that ξ_{C} extends continuously to cl(C) \ F_{C}; we denote this continuous extension by ξ_{C} as well.

Let c, d ∈ ℝ and α, β : (c, d) ⟶ ℝ be definable and C^{p} such that C = (α, β). By o-minimality and because C is bounded, the limits α(c) := lim_{x→c} α(x), α(d) := lim_{x→d} α(x), β(c) := lim_{x→c} β(x) and β(d) := lim_{x→d} β(x) exist in ℝ. The points of the set

V_{C} := {(c, α(c)), (d, α(d)), (c, β(c)), (d, β(d))}

are called the corners of C.

Example 2.4. In Example 2.2, we have F_{C} ⊆ V_{C} and both gζ · (∂/∂x) and gζ ·(∂/∂y) have constant nonzero sign. The next proposition shows that under the latter assumptions, the situation of Example 2.2 is as bad as it gets.

Proposition 2.5. Suppose that F_{C} ⊆ V_{C}, a_{1}|_{C} ≠ 0 and a_{2}|_{C} ≠ 0. Let γ : [0, 1] ⟶ C be a C^{p}-curve transverse to ξ, and let t_{i} ∈ (0, 1) be such that t_{0} < t_{1} < t_{2} < ⋯ and t_{i} → 1. Then the sequence ( cl(L(t_{i}))) converges in the Hausdorff metric to a compact set K := lim cl(L(t_{i})) ⊆ cl(C), such that

(i) Π_{1}(K) = [a, b] with c ≤ a < b ≤ d; (ii) each component of K ∩ C is a leaf of ξ; (iii) K ∩ Π_{1}^{−1}(a, b) = gr(f) for some continuous function f : (a, b) ⟶ ℝ.

Proof. By Proposition 1.5, we may assume that for every t ∈ [0, 1], the leaf L(t) is the graph of a strictly increasing C^{p}-function f_{t} : (a(t), b(t)) ⟶ ℝ (the other cases are handled similarly). Since C is bounded, the limits f_{t}(a(t)) := lim_{x→a(t)} f_{t}(x) and f_{t}(b(t)) := lim_{x→b(t)} f_{t}(x) exist, and we also denote by f_{t} : [a(t), b(t)] ⟶ ℝ the corresponding continuous extension of f_{t}. Then cl(L(t)) = gr(f_{t}). By Lemma 2.3, we may also assume that the map t ↦ L(t) : [0, 1] ⟶ L(Γ) is order-preserving (again, the other case is handled similarly). Finally, since each f_{t} is strictly increasing and the map t ↦ L(t) : [0, 1] ⟶ L(Γ) is order-preserving, it follows that f_{s}(x) > f_{t}(x) for all s, t ∈ [0, 1] such that s < t and x ∈ (a(s), b(s)) ∩ (a(t), b(t)).

Since each cl(L(t_{i})) is connected, the set K is connected, so Π_{1}(K) is an interval [a, b], which proves (i). It follows in particular that for every x ∈ (a, b), there is an open interval I_{x} ⊆ (a, b) containing x such that I_{x} ⊆ (a(t_{i}), b(t_{i})) for all sufficiently large i. Thus by our assumptions,

(∗) for every x ∈ (a, b) we have f_{t_{i}}|_{I_{x}} > f_{t_{i+1}}|_{I_{x}} for sufficiently large i.

Next, we show that K ∩ C is an integral manifold of ξ. Fix a point (x, y) ∈ K ∩ C; it suffices to show that there is an open box B ⊆ C containing (x, y) such that K ∩ B is an integral manifold of ξ. Let B = I × J be an open box containing (x, y) such that I ⊆ I_{x}. Since a_{1}(x, y) ≠ 0, we may also assume (after shrinking B) that there is an ϵ > 0 such that |a_{1}(x′, y′)| ≥ ϵ for all (x′, y′) ∈ B; in particular, there is an M > 0 such that f_{t_{i}}|_{I} is M-Lipshitz for all sufficiently large i. Hence by (∗), the function f : I ⟶ ℝ defined by f(x′) := lim_{i→∞} f_{t_{i}}(x′) is Lipshitz and satisfies K ∩ (I × ℝ) = K ∩ B = gr(f). Finally, shrinking B again if necessary, the fact that F^{ξ} is a foliation gives that K ∩ B is an integral manifold of ξ, as required.

Since K is compact and K ∩C is an integral manifold of ξ, every component of K ∩ C is a leaf of ξ. It also follows from the previous paragraph that K ∩ C is the graph of a continuous function g : Π_{1}(K ∩ C) ⟶ ℝ, which proves (ii).

Let now x ∈ (a, b) be such that x ∉ Π_{1}(K ∩ C). Then (x, α(x)) or (x, β(x)) belongs to K, because (a, b) ⊆ Π_{1}(K); by (∗) we have (x, β(x)) ∉ K, so (x, α(x)) ∈ K. If (ξ_{C} · \frac{∂}{∂x})(x, α(x)) ≠ 0, then by the same arguments as used for (ii), we conclude that there are open intervals I, J ⊆ ℝ such that (x, α(x)) ∈ I ×J and K ∩(I ×J) is the graph of a continuous function defined on I. Therefore, part (iii) is proved once we show that (ξ_{C} · \frac{∂}{∂x})(x, α(x)) ≠ 0 for all x ∈ (a, b) \ Π_{1}(K ∩ C).

Assume for a contradiction that there is an x ∈ (a, b) \ Π_{1}(K ∩ C) such that (ξ_{C} · \frac{∂}{∂x})(x, α(x)) = 0. Let M > |α′(x)|, and let I, J ⊆ ℝ be open intervals such that I ⊆ I_{x} and |a_{2}/a_{1}| > M on B := I × J. Since f_{t_{i}}(x) → α(x), it follows from the fundamental theorem of calculus for all sufficiently large i that f_{t_{i}}(x_{i}) = α(x_{i}) for some x_{i} ∈ I, a contradiction. □

3. Piecewise trivial decomposition

We continue working with ξ as in Section 1, and we adopt the notations used there. Note that ξ^{∗} (as defined at the end of the introduction) is a definable vector field on U^{∗} of class C^{p}, and that C is a Rolle decomposition of ℝ^{2} for ξ if and only if C^{∗} := {C^{∗} : C ∈ C} is a Rolle decomposition of (−1, 1)^{2} for ξ^{∗}.

Let C ⊆ U be a bounded, open, definable C^{p}-cell such that ξ|_{C} is Rolle. To detect situations like the one described in Example 2.2, we associate the following notations to such a C: there are real numbers c < d and definable C^{p} functions α, β : (c, d) ⟶ ℝ such that C = (α, β). Given a C^{1}-function δ : (c, d) ⟶ ℝ such that α(x) ≤ δ(x) ≤ β(x) for all x ∈ (c, d), we define σ_{δ} : C ⟶ ℝ by

σ_{δ}(x, y) := ξ^{⊥}(x, y) · (\begin{matrix}1 \\ δ′(x) \end{matrix}) .

Note that for each x ∈ (c, d), there are by o-minimality a maximal α_{0}^{C}(x) ∈ (α(x), β(x)] and a minimal β_{0}^{C}(x) ∈ [α(x), β(x)) such that the function σ_{α} has constant sign on {x} × (α(x), α_{0}^{C}(x)) and the function σ_{β} has constant sign on {x} × (β_{0}^{C}(x), β(x)); we omit the superscript “C” whenever C is clear from context. Note that α_{0}, β_{0} : (c, d) ⟶ ℝ are definable.

Definition 3.1. A C^{p}-cell decomposition of ℝ^{2} compatible with U, bd(U) and S(ξ) is called almost piecewise trivial for ξ if

(I) every C ∈ C_{U} of dimension 1 is either tangent or transverse to ξ; (II) the components of ξ have constant sign on every C ∈ C_{U};

and for every open, bounded C ∈ C_{U} such that C ∩ S(ξ) = ∅, the following hold:

(III) F_{C} ⊆ V_{C}; (IV) the maps α_{0}, β_{0} : (c, d) ⟶ ℝ are continuous; (V) the map σ_{α} has constant sign on the cell (α, α_{0}), and the map σ_{β} has

constant sign on the cell (β_{0}, β). We call C piecewise trivial for ξ if C^{∗} is almost piecewise trivial for ξ^{∗}.

Example 3.2. Let ζ := −y \frac{∂}{∂x} +x\frac{∂}{∂y}, and let C be the cell decomposition of ℝ^{2} consisting of the sets of the form {(x, y) : x ∗ 0, y ⋆ 0} with ∗, ⋆ ∈ {=, <, >}. Then C is piecewise trivial for ζ.

Remarks 3.3. (1) Any piecewise trivial decomposition for ξ is a Rolle

decomposition for ξ.

(2) If U is bounded, then C is almost piecewise trivial for ξ if and only if C is piecewise trivial for ξ.

(3) We obtain a piecewise trivial decomposition for ξ in the following way: first, obtain a C^{p}-cell decomposition C compatible with U, bd(U) and S(ξ) satisfying (I) and (II). Then, to satisfy (III)–(V), we only need to refine Π_{1}(C) := {Π_{1}(C) : C ∈ C}.

We now fix a piecewise trivial decomposition C of ℝ^{2} for ξ. The name “piecewise trivial” is justified by:

Theorem 3.4. Let C ∈ C_{U} be open such that C ∩S(ξ) = ∅. Then the relation ≪_{C} on L(C) is a linear ordering.

To prove the theorem, we fix a bounded, open C ∈ C_{U} such that C∩S(ξ) = ∅. Establishing the theorem for this C suffices: if the theorem holds for every bounded, open D ∈ C such that D ∩ S(ξ) = ∅, then the theorem holds with C^{∗} and ξ^{∗} in place of C and ξ (because every D ∈ C^{∗} is bounded). Since ϕ_{2} is an analytic diffeomorphism, it follows that the theorem holds for every open D ∈ C such that D ∩ S(ξ) = ∅.

We need quite a bit of preliminary work (see the end of this section for the proof of the theorem). For Lemma 3.5 and Corollary 3.6 below, we fix a C^{p}-curve γ : [0, 1] ⟶ C transverse to ξ.

Lemma 3.5. Let t_{i} ∈ (0, 1), for i ∈ ℕ, such that t_{i} → t ∈ [0, 1]. Then C ∩ lim cl(L(t_{i})) = L(t).

Proof. From Proposition 2.5 we know that C ∩ K is a union of leaves of ξ|_{C}, where K := lim cl(L(t_{i})). Thus, since γ(t_{i}) → γ(t) and γ(t) ∈ L(t), it follows that L(t) ⊆ C ∩K. To prove the opposite inclusion, we may assume by Proposition 1.5 that every leaf of ξ|_{C} is the graph of a strictly increasing function (the other case is handled similarly). By Proposition 2.5 again, Π_{1}(K) = [a, b] with c ≤ a < b ≤ d, and there is a continuous function f : (a, b) ⟶ ℝ such that K ∩ ((a, b) × ℝ) = gr(f).

Assume for a contradiction that there is a leaf M of ξ|_{C} such that M ≠ L(t) and M ⊆ C ∩ K. Then L(t) and M are disjoint subsets of gr(f); say L(t) = gr(f_{t}), where f_{t} : (a(t), b(t)) ⟶ ℝ, and M = gr(g), where g : (a′, b′) ⟶ ℝ. We assume here that a′ < b′ ≤ a(t) < b(t); the other case is again handled similarly. By our assumption, c < a(t) and hence lim_{x→a(t)^{+}} f_{t}(x) ∈ {α(a(t)), β(a(t))}. We assume here that lim_{x→a(t)^{+}} f_{t}(x) = α(a(t)), the other case being handled similarly. Then by the Mean Value Theorem, for every ϵ > 0 there is an x ∈ (a(t), a(t) + ϵ) such that f′_{t}(x) > α′(x), that is, σ_{α}(x, f_{t}(x)) < 0. It follows from (V) that

(∗) the map σ_{α} has constant negative sign on (α, α_{0}). On the other hand, b′ < d, and we may assume that lim_{x→b^{′−}} g(x) = α(b′): otherwise, lim_{x→b^{′−}} g(x) = β(b′), and since lim_{x→a(t)} f(x) = lim_{x→a(t)^{+}} f_{t}(x) = α(a(t)), we can replace M by a leaf of ξ|_{C} that is contained in gr(f) and has the desired property. But lim_{x→b^{′−}} g(x) = α(b′) means (as above) that for every ϵ > 0 there is an x ∈ (b′ − ϵ, b′) such that g′(x) < α′(x), that is, σ_{α}(x, g(x)) > 0. This contradicts (∗), so the lemma is proved. □

Put F := F (γ((0, 1))); note that F is open by Lemma 2.3(1).

Corollary 3.6. C ∩ bd(F) = L(0) ∪ L(1); in particular, there are distinct j_{0}, j_{1} ∈ {1, 2} such that C \ cl(F) = U_{L(0),j_{0}} ∪ U_{L(1),j_{1}}.

Proof. Let z ∈ cl(F) ∩ C, and let z_{i} ∈ F be such that z_{i} → z. Let t_{i} ∈ (0, 1) be such that z_{i} ∈ L(t_{i}); passing to a subsequence if necessary, we may assume that t_{i} → t ∈ [0, 1]. Then z ∈ C ∩ lim cl(L(t_{i})), so z ∈ L(t) by Lemma 3.5. Since F is open by Lemma 2.3(1), it follows that C ∩bd(F) ⊆ L(0)∪L(1). On the other hand, by Lemma 2.3(2), there is a j ∈ {1, 2} such that L(t) ⊆ U_{L(0),j} for all t ∈ (0, 1] and L(t) ⊆ U_{1,j′} for all t ∈ [0, 1), where j′ ∈ {1, 2} \ {j}. Hence L(0) ∪ L(1) ⊆ C ∩ bd(F (Γ)), and the corollary is proved. □

Definition 3.7. Let τ : [0, 1] ⟶ U be continuous. We call τ piecewise C^{p}-monotone in ξ if there are t_{0} := 0 < t_{1} < t_{2} < ⋯ < t_{k} < t_{k+1} := 1 and ∗ ∈ {<, >} such that for all i = 0, …, k, the restriction τ|_{(t_{i},t_{i+1})} is C^{p}, and either ξ^{⊥}(τ(t)) · τ′(t) = 0 for all t ∈ (t_{i}, t_{i+1}) or ξ^{⊥}(τ(t)) · τ′(t) ∗ 0 for all t ∈ (t_{i}, t_{i+1}). In this situation, we also say that τ is ∗-piecewise C^{p}- monotone in ξ. We call such a τ tangent to ξ if each τ|_{(t_{i},t_{i+1})} is tangent to ξ.

Lemma 3.8. Let v, w ∈ C. Then there is a curve τ : [0, 1] ⟶ C that is piecewise C^{p}-monotone in ξ and satisfies τ(0) = v and τ(1) = w.

Proof. If L_{v} = L_{w}, then there is a C^{p}-curve τ : [0, 1] ⟶ L_{v} such that τ(0) = v and τ(1) = w, and we are done. So we assume from now on that L_{v} ≠ L_{w}. Let j_{vw} ∈ {1, 2} be such that w ∈ U_{L_{v},j_{vw}}, and put

∗_{vw} := \begin{cases}< & if j_{vw} = 1, \\ > & if j_{vw} = 2. \end{cases}

By o-minimality, there is a definable C^{p}-curve τ : [0, 1] ⟶ C such that

(I) τ(0) = v and τ(1) = w. Again by o-minimality, there are t_{0} := 0 < t_{1} < ⋯ < t_{k} < t_{k+1} := 1 such that for each i = 0, …, k,

(II) the map t ↦ ξ^{⊥}(τ(t)) · τ′(t) has constant sign on (t_{i}, t_{i+1}). By Khovanskii theory [12], we may also assume that for every i = 0, …, k,

(III) either τ((t_{i}, t_{i+1})) ∩ (L_{v} ∪ L_{w}) = ∅ or τ((t_{i}, t_{i+1})) ⊆ L_{v} ∪ L_{w}. We now proceed by induction on k, simultaneously for all v, w ∈ C and τ satisfying (I)–(III), to prove that τ can be changed into a curve that is ∗_{vw}- piecewise C^{p}-monotone in ξ. If k = 0, then τ is ∗_{vw}-piecewise C^{p}-monotone in ξ, so we are done. Therefore, we assume that k > 0 and that the claim holds for lower values of k.

Since τ(1) = w ∉ L_{v} and L_{v} is closed in C, there is a maximal t ∈ [0, 1) such that τ(t) ∈ L_{v}, and by our choice of t_{1}, …, t_{k}, we have t = t_{i} for some i ∈ {0, …, k}. If i > 1, we replace τ|_{[0,t_{i}]} by a C^{p} curve τ_{1} : [0, t_{i}] ⟶ L_{v} such that τ_{1}(0) = v and τ_{1}(t_{i}) = τ(t_{i}), and we reindex t_{i}, …, t_{k+1} as t_{1}, …, t_{k−i+2}.

Hence by the inductive hypothesis, we may assume that i ≤ 1 and τ([0, 1]) ⊆ L_{v} ∪ U_{L_{v},j_{vw}}. Put v′ := τ(t_{1}); we now distinguish two cases: Case 1: v′ ∈ L_{v}. Then ∗_{v′w} = ∗_{vw}, so by the inductive hypothesis (and rescaling), there is a curve τ_{1} : [t_{1}, 1] ⟶ C that is ∗_{vw}-piecewise C^{p}-monotone in ξ and satisfies τ_{1}(t_{1}) = v′ and τ_{1}(1) = w. Now replace τ|_{[t_{1},1]} by τ_{1}.

Case 2: v′ ∉ L_{v}. Then we must have ξ^{⊥}(τ(t)) · τ(t) ∗_{vw} 0 for all t ∈ (0, t_{1}). If v′ ∈ L_{w}, the lemma follows by a similar argument as in Case 1, so we assume that v′ ∉ L_{w}. We claim again that ∗_{v′w} = ∗_{vw} in this situation, from which the lemma then follows from the inductive hypothesis as in Case 1.

To see the claim, note that by Corollary 3.6, the complement of F (τ([0, t_{1}])) in C has two connected components U_{L_{v},j} and U_{L_{v′,j′}}, where j, j′ ∈ {1, 2} are distinct. By the above, j must be different from j_{vw}, so w ∈ U_{L_{v′,j′}}, that is, j′ = j_{v′w}, which implies j_{vw} = j_{v′w} as required. □

Lemma 3.9. Let τ : [0, 1] ⟶ C be piecewise C^{p}-monotone in ξ such that τ is not tangent to ξ. Then there is a C^{p} curve γ : [0, 1] ⟶ C such that γ is transverse to C, γ(0) = τ(0) and γ(1) = τ(1).

Proof. Let t_{0} := 0 < t_{1} < t_{2} < ⋯ < t_{k} < t_{k+1} := 1 be as in Definition 3.7. We work by induction on k; if k = 0, then by hypothesis τ is transverse to ξ, and we take γ := τ. So we assume that k > 0; for the inductive step, it suffices to consider the the case k = 1. The hypothesis on τ then implies that at least one of τ|_{(0,t_{1})} and τ|_{(t_{1},1)} is transverse to ξ; so we distinguish three cases: Case 1: both τ|_{(0,t_{1})} and τ|_{(t_{1},1)} are transverse to ξ. By Picard’s theorem, there are an open neighborhood W ⊆ C of τ(t_{1}) and a C^{p}-diffeomorphism f : ℝ^{2} ⟶ W such that f(0) = τ(t_{1}) and f^{∗}ξ = ∂/∂x, where f^{∗}ξ is the pullback of ξ via f. Then for some ϵ > 0, the continuous curve f^{−1} ∘ τ|_{(t_{1}−ϵ,t_{1}+ϵ)} is C^{p} and transverse to ∂/∂x on (t_{1}−ϵ, t_{1})∪(t_{1}, t_{1}+ϵ). Using standard smoothing arguments from analysis, we can now find a C^{p}-curve η : (t_{1} − ϵ, t_{1} + ϵ) ⟶ ℝ^{2} that is transverse to ∂/∂x and satisfies η(t) = f^{−1}(τ(t)) for all t ∈ (t_{1} − ϵ, t_{1} − ϵ/2) ∪ (t_{1} + ϵ/2, t_{1} + ϵ). Now define γ : [0, 1] ⟶ C by

γ(t) := \begin{cases}τ(t) & if 0 ≤ t < t_{1} − ϵ or t_{1} + ϵ < t ≤ 1, \\ f(η(t)) & if t_{1} − ϵ ≤ t ≤ t_{1} + ϵ. \end{cases}

Case 2: τ|_{(0,t_{1})} is transverse to ξ and τ|_{(t_{1},1)} is tangent to ξ. Since τ([t_{1}, 1]) is compact, there are (by Picard’s theorem again) s_{0} := t_{1} < s_{1} < ⋯ < s_{l} < s_{l+1} := 1, open neighborhoods W_{i} ⊆ U of τ(s_{i}) and C^{p}-diffeomorphisms f_{i} : ℝ^{2} ⟶ W_{i}, for i = 0, …, l + 1, such that τ([t_{1}, 1]) ⊆ W_{0} ∪ ⋯ ∪ W_{l+1}, f_{i}(0) = τ(s_{i}) and f_{i}^{∗}ξ = ∂/∂x for each i. We assume that l = 0, so that s_{0} = t_{1} and s_{1} = 1; the general case then follows by induction on l.

Let u ∈ (t_{1}, 1) be such that τ(u) ∈ W_{0} ∩ W_{1}. Working with f_{0} similarly as in Case 1, we can replace τ|_{[0,u]} by a C^{p}-curve η : [0, u] ⟶ C transverse to ξ such that η(0) = τ(0) and η(u) = τ(u). Define η(t) := τ(t) for t ∈ (u, 1]; repeating the procedure with η and f_{1} in place of τ and f_{0}, we obtain a C^{p}- curve γ : [0, 1] ⟶ C that is transverse to ξ and satisfies γ(0) = τ(0) and γ(1) = τ(1), as desired. Case 3: τ|_{(0,t_{1})} is tangent to ξ and τ|_{(t_{1},1)} is transverse to ξ. This case is similar to Case 2. □

Combining Lemmas 3.8 and 3.9, we obtain:

Corollary 3.10. Let u, v ∈ C be such that L_{u} ≠ L_{v}. Then there is a C^{p} curve γ : [0, 1] ⟶ C such that γ(0) = u, γ(1) = v and γ is transverse to ξ. □

Proof of Theorem 3.4. Let M, L ∈ L(C) be distinct and choose v ∈ M and w ∈ L. By Corollary 3.10, there is a C^{p}-curve γ : [0, 1] ⟶ C such that γ(0) = v, γ(1) = w and γ is transverse to ξ. Hence t ↦ ξ^{⊥}(γ(t)) · γ′(t) has constant nonzero sign on [0, 1]; this shows that ≪_{C} is irreflexive. Transitivity follows by a similar argument. □

4. Foliation orderings

Let ξ = a_{1} \frac{∂}{∂x} + a_{2} \frac{∂}{∂y} be a definable vector field of class C^{1} on ℝ^{2}. We fix a piecewise trivial decomposition C of ℝ^{2} for ξ; refining C if necessary, we may assume that C is a stratification. To simplify statements, we put

C_{reg} := {C ∈ C : C ∩ S(ξ) = ∅} .

For instance in Example 3.2, the piecewise trivial decomposition C is a stratification and C_{reg} = C \ {0}.

Remark 4.1. C being a stratification has the following consequence: for every 1-dimensional C ∈ C, there are exactly two distinct open D ∈ C such that C ∩ fr(D) ≠ ∅, and for each of these D we have C ⊆ fr(D).

Let V ⊆ ℝ^{2} \ S(ξ) be an integral manifold of ξ, that is, a 1-dimensional manifold tangent to ξ. Given u, v ∈ V, we define u <_{V}^{ξ} v if and only if there is a C^{1} path γ : [0, 1] ⟶ V such that γ(0) = u, γ(1) = v and ξ(γ(t)) · γ′(t) > 0 for all t ∈ [0, 1].

Lemma 4.2. Assume that V is connected and not a compact leaf. Then the relation <_{V}^{ξ} defines a dense linear ordering of V without endpoints.

Proof. Let u, v ∈ V be such that u ≠ v. Since V is connected, we get u <_{V}^{ξ} v or v <_{V}^{ξ} u. On the other hand, if there are C^{1}-paths γ, δ : [0, 1] ⟶ V such that γ(0) = δ(1) = u, γ(1) = δ(0) = v and ξ(γ(t)) · γ′(t) > 0 and ξ(δ(t)) · δ′(t) > 0 for all t ∈ [0, 1], then γ([0, 1]) ∪ δ([0, 1]) is a compact leaf of ξ contained in V; since V is connected, it follows that V is a compact leaf, a contradiction. □

We now fix a C ∈ C_{reg} such that dim(C) > 0.

Definition 4.3. The foliation of ξ induces an ordering <_{C}^{ξ} on C as follows:

• Suppose that C is open, and let u, v ∈ C. Then every leaf of ξ|_{C} is non-compact by Proposition 1.5. Thus, we define u <_{C}^{ξ} v if and only if L_{u} ≪_{C}^{ξ} L_{v} or L_{u} = L_{v} and u <_{L_{u}}^{ξ} v.

• Suppose that dim(C) = 1 and C is tangent to ξ. Then C is a connected, non-compact integral manifold of ξ, so we define <_{C}^{ξ} as before Lemma 4.2.

• Suppose that dim(C) = 1 and C is transverse to ξ. Let u, v ∈ C; we define u <_{C}^{ξ} v if and only if there is a C^{1}-curve γ : [0, 1] ⟶ C such that ξ^{⊥}(γ(t)) · γ′(t) > 0 for all t ∈ [0, 1].

As before, we omit the superscript ξ whenever it is clear from context.

A <_{C}-interval is a set A of the form (a, b) := {c ∈ C : a ∗_{1} c ∗_{2} b} with a, b ∈ C, or (a, ∞) := {c ∈ C : a ∗ c} with a ∈ C, or (−∞, b) := {c ∈ C : c ∗ c} with b ∈ C, where ∗, ∗_{1}, ∗_{2} ∈ {<_{C}, ≤_{C}}; we call A open if ∗ = ∗_{1} = ∗_{2} =<_{C}.

Lemma 4.4. The ordering <_{C} is a dense linear ordering on C without endpoints. Moreover, if dim(C) = 1, then every <_{C}-bounded subset of C has a least upper bound.

Proof. It is clear from the definition that C has no endpoints with respect to <_{C}. Density and linearity follow from Lemmas 2.3 and 4.2 if dim(C) = 1, and if C is open, they follow from Lemma 4.2 and Theorem 3.4.

For the second statement, assume that dim(C) = 1 and let α : (0, 1) ⟶ ℝ^{2} be C^{1} and injective such that C = α((0, 1)). If C is tangent to ξ, then the map t ↦ ξ(α(t)) · α′(t) has constant nonzero sign, and if C is transverse to ξ, then the map t ↦ ξ^{⊥}(α(t))·α′(t) has constant nonzero sign. Thus in both cases, the map α : ((0, 1), < ) ⟶ (C, <_{C}) is either order-preserving or order-reversing; the second statement follows. □

We assume for the remainder of this section that either C is open, or C is 1-dimensional and tangent to ξ.

Definition 4.5. For each leaf L of ξ|_{C}, it follows from Proposition 1.5 that fr(L) consists of exactly two points P_{L}^{>}, P_{L}^{<} ∈ fr(C) ∪ {∞}, where, for ∗ ∈ {>, <}, P_{L}^{∗} is the unique of these two points with the property that for every C^{1}-curve γ : [0, 1) ⟶ L satisfying γ(0) ∈ L and lim_{t→1} γ(t) = P_{L}^{∗}, we have ξ(γ(t)) · γ′(t) ∗ 0 for all t ∈ [0, 1). In this situation, we define the forward projection 𝔣_{C} : C ⟶ fr(C) ∪ {∞} and the backward projection 𝔟_{C} :

C ⟶ fr(C) ∪ {∞} as

𝔣_{C}(z) := P_{L_{z}}^{>} and 𝔟_{C}(z) := P_{L_{z}}^{<}, for all z ∈ C.

From now on we assume that C is open, and we let D ∈ C_{reg} be of dimension 1 and contained in fr(C) such that D is transverse to ξ.

Lemma 4.6. Either D ⊆ 𝔣_{C}(C) and D ∩ 𝔟_{C}(C) = ∅, or D ⊆ 𝔟_{C}(C) and D ∩ 𝔣_{C}(C) = ∅.

Proof. Let α : (0, 1) ⟶ ℝ^{2} be a definable C^{1}-map such that D = α((0, 1)) and ξ^{⊥}(α(t)) · α′(t) > 0 for all t ∈ (0, 1). Thus, either ξ(α(t)) points into C for all t, or ξ(α(t)) points out of C for all t. In the first case, we have 𝔣_{C}(C) ∩ D = ∅, and in the second case 𝔟_{C}(C) ∩ D = ∅. Moreover by Picard’ s Theorem, for every w ∈ D there is an integral manifold V ⊆ ℝ^{2} of ξ such that V ∩ D = {w}; hence, either w ∈ 𝔣_{C}(C) or w ∈ 𝔟_{C}(C). □

Lemma 4.7. The maps 𝔣_{C}|_{𝔣_{C}^{−1}(D)} and 𝔟_{C}|_{𝔟_{C}^{−1}(D)} are increasing.

Proof. We prove the lemma for 𝔣_{C}. Let u, v ∈ C with u <_{C} v be such that 𝔣_{C}(u), 𝔣_{C}(v) ∈ D; we may clearly assume that L_{u} ≪_{C} L_{v}, and hence (by Picard’s Theorem) that 𝔣_{C}(u) ≠ 𝔣_{C}(v).

We assume here that D = gr(α), where α : (a, b) ⟶ ℝ is a definable C^{1}- function; the case D = {a}×(b, c) is handled similarly. Let also β : (a, b) ⟶ ℝ be a definable C^{1}-function such that C = (α, β) or C = (β, α); we assume here the former, the latter being handled similarly. For s ∈ [0, 1], we put

α_{s}(t) := (1 − s)α(t) + sβ(t), a < t < b.

Then for every t ∈ (a, b), we have lim_{s→0} α_{s}(t) = α(t) and lim_{s→0} α′_{s}(t) = α′(t).

Let now a < a′ < b′ < b be such that 𝔣_{C}(u), 𝔣_{C}(v) ∈ gr α|_{(a′,b′)}. Since D is transverse to ξ, there is an ϵ > 0 such that gr α_{s}|_{(a′,b′)} is transverse to ξ for all s ∈ [0, ϵ). It follows from the previous paragraph that the map t ↦ σ_{α}(t, α(t)) has the same constant nonzero sign as the map t ↦ σ_{α_{s}}(t, α_{s}(t)), for all s ∈ (0, ϵ). Therefore by Lemma 2.3(2) and the definition of <_{D}, we have 𝔣_{C}(u) <_{D} 𝔣_{C}(v), as required. □

Corollary 4.8. Let I ⊆ C be a <_{C}-interval. Then each of 𝔣_{C}(I) ∩ D and 𝔟_{C}(I) ∩ D is either empty, a point or an open <_{D}-interval.

Proof. Assume that a, b ∈ 𝔣_{C}(I) ∩ D are such that a <_{D} b, and let c ∈ D be such that a <_{D} c <_{D} b; it suffices to show that c ∈ 𝔣_{C}(I). By Lemma 4.6, c ∈ 𝔣_{C}(C). Let u, v, w ∈ C be such that a = 𝔣_{C}(u), b = 𝔣_{C}(v), c = 𝔣_{C}(w) and u, v ∈ I. Then u <_{C} w <_{C} v by Lemma 4.7, as required. □

We fix a set E_{C} ⊆ C such that |E_{C} ∩ L| = 1 for every L ∈ L(C) and put <_{E_{C}}:=<_{C} |_{E_{C}}, and we denote by e_{L} the unique element of E ∩ L, for every L ∈ L(C).

Remark. The map L ↦ L∩E_{C} : (L(C), ≪_{C}) ⟶ (E_{C}, <_{E_{C}}) is an isomorphism of ordered structures.

Proposition 4.9. Let 𝔤 ∈ {𝔣, 𝔟}. If D ⊆ 𝔤_{C}(C), then D_{𝔤} := 𝔤_{C}^{−1}(D) ∩ E_{C} is an <_{E_{C}}-interval, and the map 𝔤_{C}|_{D_{𝔤}} : (D_{𝔤}, <_{E_{C}} |_{D_{𝔤}}) ⟶ (D, <_{D}) is an isomorphism of ordered structures.

Proof. The transversality of D to ξ implies that if u ∈ D and L_{1}, L_{2} ∈ L(C) are such that u = P_{L_{1}}^{>} = P_{L_{2}}^{>} or u = P_{L_{1}}^{<} = P_{L_{2}}^{<}, then L_{1} = L_{2}. Thus by Lemma 4.7, the map 𝔤_{C}|_{D_{𝔣}} is strictly increasing, so the lemma follows. □

5. Progression map

We continue working with ξ and C as in Section 4, and we adopt all corresponding notations. We let

(i) C_{open} be the collection of all open cells in C_{reg}; (ii) C_{tan} be the collection of all cells in C_{reg} that are of dimension 1 and

tangent to ξ; (iii) C_{trans} be the collection of all cells in C_{reg} that are of dimension 1 and

transverse to ξ; and (iv) C_{single} the collection of all p ∈ ℝ^{2} such that {p} ∈ C_{reg}. By Lemma 4.6 and since C is a stratification, there are, for each C ∈ C_{trans},

distinct and unique cells C^{𝔟}, C^{𝔣} ∈ C_{open} such that C∩cl(C^{𝔟}) ≠ ∅, C∩cl(C^{𝔣}) ≠ ∅ and

C ⊆ 𝔣_{C^{𝔟}}(C^{𝔟}) and C ⊆ 𝔟_{C^{𝔣}}(C^{𝔣}).

Similarly, there are, for each p ∈ C_{single}, distinct and unique cells p^{𝔟}, p^{𝔣} ∈ C_{open} ∪ C_{tan} such that p ∈ cl(p^{𝔟}), p ∈ cl(p^{𝔣}) and

p ∈ 𝔣_{p^{𝔟}}(p^{𝔟}) and p ∈ 𝔟_{p^{𝔣}}(p^{𝔣}).

(For p ∈ C_{single}, we use the fact that there is an open box B containing p such that the leaf of ξ|_{B} passing through p is a Rolle leaf.) For each C ∈ C_{tan}, we fix an arbitrary element e_{C} ∈ C; note that for each z ∈ C, C is the unique leaf L_{z} of ξ|_{C} containing z.

We now define 𝔣′, 𝔟′ : ℝ^{2} ⟶ ℝ^{2} ∪ {∞} by

𝔣′(z) := \begin{cases}𝔣_{C}(z) & if z ∈ C ∈ C_{open} ∪ C_{tan} and e_{L_{z}} ≤_{L_{z}} z, \\ e_{L_{z}} & if z ∈ C ∈ C_{open} ∪ C_{tan} and z <_{L_{z}} e_{L_{z}}, \\ (𝔟_{C^{𝔣}}|_{E_{C^{𝔣}}})^{−1}(z) & if z ∈ C ∈ C_{trans} ∪ C_{single}, \\ z & if z ∈ S(ξ) \end{cases}

and

𝔟′(z) := \begin{cases}𝔟_{C}(z) & if z ∈ C ∈ C_{open} ∪ C_{tan} and z ≤_{L_{z}} e_{L_{z}}, \\ e_{L_{z}} & if z ∈ C ∈ C_{open} ∪ C_{tan} and e_{L_{z}} <_{L_{z}} z, \\ (𝔣_{C^{𝔟}}|_{E_{C^{𝔟}}})^{−1}(z) & if z ∈ C ∈ C_{trans} ∪ C_{single}, \\ z & if z ∈ S(ξ). \end{cases}

Definition 5.1. We define 𝔣, 𝔟 : ℝ^{2} ∪ {∞} ⟶ ℝ^{2} ∪ {∞} by

𝔣(z) := \begin{cases}𝔣′(z) & if z ∈ ℝ^{2} and 𝔣′(z) ∉ S(ξ), \\ ∞ & otherwise \end{cases}

and

𝔟(z) := \begin{cases}𝔟′(z) & if z ∈ ℝ^{2} and 𝔟′(z) ∉ S(ξ), \\ ∞ & otherwise. \end{cases}

We call 𝔣 a progression map associated to ξ and 𝔟 a reverse progression map associated to ξ. We put

C_{1} = C_{trans} ∪ C_{single} ∪ ⋃ {E_{C} : C ∈ C_{open}} ∪ {{e_{C}} : C ∈ C_{tan}}

and let B := ⋃ C_{1}; note that 𝔣(ℝ^{2}) ⊆ B ∪ {∞} and 𝔟(ℝ^{2}) ⊆ B ∪ {∞}. Finally, we define 𝔣^{0} : ℝ^{2} ∪ {∞} ⟶ ℝ^{2} ∪ {∞} by 𝔣^{0}(x) := x, and for k > 0 we define 𝔣^{k} : ℝ^{2} ∪ {∞} ⟶ ℝ^{2} ∪ {∞} inductively on k by 𝔣^{k}(x) := 𝔣(𝔣^{k−1}(x)).

Proposition 5.2. Let X ∈ C_{1} and L be a compact leaf of ξ. Then |X ∩L| ≤ 1.

Proof. If X ∈ C_{single} or X = {e_{C}} for some C ∈ C_{tan}, the conclusion is trivial. By Lemma 1.3(2), L is a Rolle leaf of ξ; in particular, |X ∩L| ≤ 1 if X ∈ C_{trans}. So we may assume that X = E_{C} for some C ∈ C_{open}. Then there is at most one L′ ∈ L(C) contained in L: otherwise by Corollary 3.10, there is a C^{1}-curve γ : [0, 1] ⟶ C transverse to ξ such that γ(0), γ(1) ∈ L, a contradiction. It follows again that |X ∩ L| ≤ 1. □

Proposition 5.3. There is an N ∈ ℕ such that for every x ∈ B, the leaf of ξ through x is compact if and only if 𝔣^{N}(x) = x.

Proof. Let x ∈ B; if 𝔣^{k}(x) = x for some k > 0, then the leaf of ξ through x is compact. For the converse, we assume that the leaf L of ξ through x is compact. Since L is compact, we have L∩S(ξ) = ∅, that is, 𝔣^{k}(x) ∈ B for every k > 0. Thus with n := |C_{reg}|+1, there are a C ∈ C_{reg} and 0 ≤ k_{1} < k_{2} ≤ n such that 𝔣^{k_{1}}(x), 𝔣^{k_{2}}(x) ∈ C. It follows from Proposition 5.2 that 𝔣^{k_{1}}(x) = 𝔣^{k_{2}}(x), and hence that

x = 𝔟^{k_{1}} ∘ 𝔣^{k_{1}}(x) = 𝔟^{k_{1}} ∘ 𝔣^{k_{2}}(x) = 𝔣^{k_{2}−k_{1}}(x).

Since n is independent of x ∈ B, the number N := n! will do. □

6. Flow configuration theories

Inspired by the previous sections, we now define a first-order theory as described in the introduction. Our main goal, reached in Section 9, is to show that this theory admits quantifier elimination in a language suitable to our purposes.

Definition 6.1. A flow configuration is a tuple

Φ = (Φ_{open}, Φ_{tan}, Φ_{trans}, Φ_{single}, ϕ^{𝔟}, ϕ^{𝔣}, min, max, N_{Φ})

such that Φ_{open}, Φ_{tan}, Φ_{trans} and Φ_{single} are pairwise disjoint, finite sets,

ϕ^{𝔟}, ϕ^{𝔣} : Φ_{trans} ∪Φ_{single} ⟶ Φ_{open} ∪ Φ_{tan},
min, max : Φ_{open} ∪ Φ_{tan} ∪ Φ_{trans} ⟶ Φ_{single} ∪ {∞}

and N_{Φ} ∈ ℕ. In this situation, we shall write a^{𝔟} and a^{𝔣} instead of ϕ^{𝔟}(a) and ϕ^{𝔣}(a), for a ∈ Φ_{trans} ∪Φ_{single}.

Example 6.2. Let ξ be a vector field on ℝ^{2} of class C^{1} and definable in an o-minimal expansion of the real field, and let C be a piecewise trivial cell decomposition of ℝ^{2} that is also a stratification. We define C_{open}, C_{tan}, C_{trans}, C_{single} and ^{𝔟}, ^{𝔣} : C_{trans} ∪ C_{single} ⟶ C_{open} ∪ C_{tan} as in Section 5, and we let N ∈ ℕ be as in Proposition 5.3.

Let C ∈ C_{open} ∪ C_{tan} ∪ C_{trans}. If there is a point in C_{single} that is contained in the closure of every set {x ∈ C : x <_{C}^{ξ} a} with a ∈ C, we let min(C) be any such point; otherwise, we put min(C) := ∞. Similarly, if there is a point in C_{single} that is contained in the closure of every set {x ∈ C : a <_{C}^{ξ} x} with a ∈ C, we let max(C) be any such point; otherwise, we put max(C) := ∞. Then the tuple

Φ_{ξ} = Φ_{ξ}(C) := (C_{open}, C_{tan}, C_{trans}, C_{single}, ^{𝔟}, ^{𝔣}, min, max, N)

is a flow configuration associated to ξ.

For the remainder of this section, we fix a flow configuration Φ.

Definition 6.3. Let L(Φ) be the first-order language consisting of

(i) a unary predicate C and a binary predicate <_{C}, for each C ∈ Φ_{open} ∪ Φ_{tan} ∪ Φ_{trans};

(ii) a unary predicate E_{C} for each C ∈ Φ_{open} and a constant symbol e_{C} for

each C ∈ Φ_{tan}; (iii) a constant symbol s, and a constant symbol c for each c ∈ Φ_{single}; (iv) unary function symbols 𝔣 and 𝔟;

(v) constant symbols r_{C}^{𝔤} and s_{C}^{𝔤} for each C ∈ Φ_{trans} and 𝔤 ∈ {𝔣, 𝔟}.

Throughout the rest of this paper, for m ∈ ℕ we write 𝔣^{m} for the L(Φ)-word consisting of m repetitions of the symbol 𝔣, and similarly for 𝔟^{m}.

Example 6.4. Let ξ and C be as in Example 6.2; we adopt the notations used there. We associate to ξ a unique L(Φ_{ξ})-structure M_{ξ} = M_{ξ}(C) as follows:

(i) the universe M_{ξ} of M_{ξ} is ℝ^{2} \ S(ξ) ∪ {∞}; (ii) for each C ∈ C_{open} ∪ C_{tan} ∪ C_{trans}, the predicate C is interpreted by

the corresponding cell in C, and the predicate <_{C} is interpreted by the union of <_{C}^{ξ} with {(min(C), a) : a ∈ C}, and {(a, max(C)) : a ∈ C};

(iii) for each C ∈ C_{open}, the predicate E_{C} is interpreted by the set E_{C} described in Section 5, and for each C ∈ C_{tan}, the constant e_{C} is interpreted by the element e_{C} ∈ C picked in Section 5;

(iv) the constant s is interpreted as ∞, and for each c ∈ C_{single}, the constant

c is interpreted as the corresponding element of C_{single};

(v) the functions 𝔣 and 𝔟 are interpreted by the corresponding forward progression and reverse progression maps;

(vi) for each C ∈ C_{trans} and 𝔤 ∈ {𝔣, 𝔟}, the constants r_{C}^{𝔤} and s_{C}^{𝔤} are interpreted as the lower and upper endpoints, respectively, of the interval 𝔤(C) in E_{C^{𝔤}} ∪ {min(C^{𝔤}), max(C^{𝔤})}.

Definition 6.5. We put Φ_{0} := Φ_{open} ∪ Φ_{tan} ∪ Φ_{trans}; intending to capture the theory of the previous example, we let T (Φ) be the L(Φ)-theory consisting of the universal closures of the formulas in the axiom schemes (F1)–(F15) below.

(F1) The formulas

(a) ⋀_{c,d∈Φ_{single},c≠d} ¬c = d ∧ ⋀_{c∈Φ_{single},C∈Φ_{0}} ¬Cc,

(b) ⋀_{c∈Φ_{single}} ¬c = s ∧ ⋀_{C∈Φ_{0}} ¬Cs,

(c) x = s ∨ ⋁_{c∈Φ_{single}} x = c ∨ ⋁_{C∈Φ_{0}} (Cx ∧ ⋀_{D∈Φ_{0},D≠C} ¬Dx).

(F2) For each C ∈ Φ_{0} the sentences stating that <_{C} is a dense linear ordering of C, together with Cx → (x <_{C} max(C) ∧ min(C) <_{C} x).

Remark. We do not wish to state that <_{C} is a linear order on all of C ∪ {min(C), max(C)}, because it is possible that min(C) = max(C). The axioms (F2) suffice for our purpose, which is to be able to refer to C as the <_{C}-interval between min(C) and max(C).

(F3) The formula ⋀_{C∈Φ_{tan}} Ce_{C} ∧ ⋀_{C∈Φ_{open}} E_{C}x → Cx.

(F4) For each C ∈ Φ_{open} the sentences stating that the restriction of <_{C} to E_{C} is a dense linear ordering.

(F5) For each (𝔤, 𝔥) ∈ {(𝔣, 𝔟), (𝔟, 𝔣)} and ∗ ∈ {≤, ≥} the formulas (a) 𝔤s = s ∧ (¬x = s → ¬𝔤x = x),

(b) ⋀_{c∈Φ_{single}}(¬𝔤c = s → 𝔥𝔤c = c),

(c) ⋀_{C∈Φ_{open}} C𝔤x → E_{C}𝔤x ∧ ⋀_{C∈Φ_{tan}} C𝔤x → 𝔤x = e_{C},

(d) ⋀_{C∈Φ_{tan}}(Cx ∧ e_{C} ∗_{C} x ∗_{C} 𝔤e_{C}) → 𝔤x = 𝔤e_{C},

(e) ⋀_{C∈Φ_{tan}}(Cx ∧ e_{C} ∗_{C} x ∗_{C} 𝔥e_{C}) → 𝔤x = e_{C}.

(F6) For each C ∈ C_{open} and 𝔤 ∈ {𝔣, 𝔟} the formula

(E_{C}x ∧ E_{C}y ∧ 𝔤x = 𝔤y) → (𝔤x = s ∨ x = y).

(F7) For each c ∈ Φ_{single} and 𝔤 ∈ {𝔣, 𝔟}, the sentences 𝔤c = e_{c^{𝔤}} if c^{𝔤} ∈ Φ_{tan}

and E_{c^{𝔤}}𝔤c if c^{𝔤} ∈ Φ_{open}. (F8) For each C ∈ Φ_{trans} and (𝔤, 𝔥) ∈ {(𝔣, 𝔟), (𝔟, 𝔣)} the sentences stating

that 𝔤(C) is an interval I_{1} in E_{C^{𝔤}} and 𝔤|_{C} : C ⟶ I_{1} is an orderisomorphism.

(F9) For each C ∈ Φ_{open} and (𝔤, 𝔥) ∈ {(𝔣, 𝔟), (𝔟, 𝔣)} the formula

E_{C}x → (𝔤x = s ∨ ⋁_{D∈Φ_{trans}, C=D^{𝔥}} D𝔤x ∨ ⋁_{d∈Φ_{single}, C=d^{𝔥}} 𝔤x = d) .

We need more axioms describing the ordering <_{C} and the behavior of 𝔣 and 𝔟 on C, for C ∈ Φ_{open}. For example, if x ∈ C \ E_{C}, we want that x has either a unique predecessor or a unique successor in E_{C}. Also, for any y ∈ E_{C}, the set of points x for which y is either the predecessor or successor is infinite and densely ordered by <_{C}. For convenience, we let ϕ_{C}^{𝔣}(x, y) and ϕ_{C}^{𝔟}(x, y) be the following formulas:

ϕ_{C}^{𝔣}(x, y) is Cx ∧ ¬E_{C}x ∧ E_{C}y ∧ x <_{C} y ∧ ¬∃z(E_{C}z ∧ x <_{C} z <_{C} y),
ϕ_{C}^{𝔟}(x, y) is Cx ∧ ¬E_{C}x ∧ E_{C}y ∧ y <_{C} x ∧ ¬∃z(E_{C}z ∧ y <_{C} z <_{C} x).

(F10) For each C ∈ Φ_{open} the formulas (a) Cx ∧ ¬E_{C}x → ∃y(ϕ_{C}^{𝔣}(x, y) ∨ ϕ_{C}^{𝔟}(x, y)),

(b) ∃yϕ_{C}^{𝔣}(x, y) → ¬∃yϕ_{C}^{𝔟}(x, z),

(c) ∃yϕ_{C}^{𝔟}(x, y) → ¬∃yϕ_{C}^{𝔣}(x, y), and the formula scheme E_{C}y → ∃^{∞}xϕ_{C}^{𝔣}(x, y) ∧ ∃^{∞}xϕ_{C}^{𝔟}(x, y).

(F11) For each C ∈ Φ_{open} the sentences stating that for every y ∈ E_{C}, the restriction of <_{C} to the set C_{y} := {x : ϕ_{C}^{𝔟}(x, y) ∨ ϕ_{C}^{𝔣}(x, y) ∨ x = y} is a dense linear ordering, together with C_{y}x → (x <_{C} 𝔣y ∧ 𝔤y <_{C} x).

(F12) For each C ∈ Φ_{open} and (𝔤, 𝔥) ∈ {(𝔣, 𝔟), (𝔟, 𝔣)} the formulas (a) Cx ∧ ¬E_{C}x ∧ ∃yϕ_{C}^{𝔤}(x, y) → ∀z(ϕ_{C}^{𝔤}(x, z) → 𝔤x = z),

(b) Cx ∧ ¬E_{C}x ∧ ∃yϕ_{C}^{𝔥}(x, y) → ∀z(ϕ_{C}^{𝔥}(x, z) → 𝔤x = 𝔤z). (F13) For each C ∈ Φ_{trans} and (𝔤, 𝔥) ∈ {(𝔣, 𝔟), (𝔟, 𝔣)} the formulas

(a) E_{C^{𝔤}}r_{C}^{𝔤} ∨ r_{C}^{𝔤} = min(C^{𝔤}) ∨ r_{C}^{𝔤} = max(C^{𝔤}),

(b) E_{C^{𝔤}}s_{C}^{𝔤} ∨ s_{C}^{𝔤} = min(C^{𝔤}) ∨ s_{C}^{𝔤} = max(C^{𝔤}),

(c) r_{C}^{𝔤} ≤_{C^{𝔤}} s_{C}^{𝔤},

(d) E_{C^{𝔤}}x → (C𝔥x ↔ r_{C}^{𝔤} <_{C^{𝔤}} x <_{C^{𝔤}} s_{C}^{𝔤}). (F14) For each m, n ∈ ℕ, C ∈ Φ_{open}, D ∈ Φ_{trans} and 𝔤 ∈ {𝔣, 𝔟} the formulas

(a) E_{C}x ∧ E_{C}𝔤^{m}x ∧ 𝔤^{n}x = x → 𝔤^{m}x = x,

(b) Dx ∧ D𝔤^{m}x ∧ 𝔤^{n}x = x → 𝔤^{m}x = x. (F15) For each m ∈ ℕ and 𝔤 ∈ {𝔣, 𝔟} the formula 𝔤^{m}(x) = x → 𝔤^{N_{Φ}}(x) = x. This completes our list of axioms for T (Φ).

Our choice of axioms above and Sections 4 and 5 imply the following:

Proposition 6.6. Let ξ be a vector field on ℝ^{2} of class C^{1} and definable in an o-minimal expansion of the real field, and let M_{ξ} be an L(Φ_{ξ})-structure associated to ξ as in Example 6.4. Then M_{ξ} ⊧ T (Φ_{ξ}). □

Definition 6.7. We write

Φ_{1} := Φ_{trans} ∪ {E_{C} : C ∈ Φ_{open}} .

The following L(Φ)-formulas are of particular interest: for C ∈ Φ_{1}, we let Fix_{C}(x) be the formula Cx ∧ 𝔣^{N_{Φ}}x = x and Fix_{C}(x, y) be the formula

∃z((x ≤_{C} z ≤_{C} y ∨ y ≤_{C} z ≤_{C} x) ∧ Fix_{C}(z)).

Next, we let Bd_{C}(x) be the formula

Fix_{C}(x) ∧ ∀y∀z(y <_{C} x <_{C} z → ∃w(y <_{C} w <_{C} z ∧ ¬ Fix_{C}(w))),

and let Lim_{C}(x) be the formula

Fix_{C}(x) ∧ ∃y(Cy ∧ y ≠ x ∧ ¬ Fix_{C}(x, y)).

Example 6.8. Let ξ be a vector field on ℝ^{2} of class C^{1} and definable in an o-minimal expansion of the real field, and let M_{ξ} be an L(Φ_{ξ})-structure associated to ξ as in Example 6.4. Let also C ∈ C_{1} := C_{trans}∪{E_{F} : F ∈ C_{open}}. Then the set Fix_{C}(M) is the set of points in C that belong to a cycle of ξ, the set Bd_{C}(M) is the set of points in C that belong to a boundary cycle of ξ, and the set Lim_{C}(M) is the set of points in C that belong to a limit cycle of ξ. Note that if ξ is analytic, then the set Bd_{C}(M) is discrete by Poincaré’s Theorem [10] (see also [9, p. 217]); in particular, Bd_{C}(M) = Lim_{C}(M) in this case.

In general, by Proposition 5.3, the cardinality of Bd_{C}(M) is equal to the number of boundary cycles of ξ that intersect C. Since every cycle of ξ intersects the set ⋃ C_{tan} ∪ ⋃ C_{trans} ∪ ⋃ C_{single}, it follows that, with b(ξ) denoting the cardinality of the set of all boundary cycles of ξ, we have

| Bd_{C}(M)| ≤ b(ξ) ≤ |C_{tan}| + |C_{single}| + ∑_{D∈C_{trans}} | Bd_{D}(M)|.

7. Iterating the progression maps

We continue to work with a flow configuration Φ as in Definition 6.1. Throughout this section, we fix (𝔤, 𝔥) ∈ {(𝔣, 𝔟), (𝔟, 𝔣)}.

For the next lemma, we denote by Θ_{(𝔤,𝔥)} the universal closure of the conjunction of the formulas (⋀_{C∈Φ_{0}} ¬Cx) → 𝔤𝔥x = x,

(Cx ∧ E_{C}𝔥x) → 𝔤𝔥x = 𝔤x and (E_{C}x ∧ 𝔥x ≠ s) → 𝔤𝔥x = x

for each C ∈ Φ_{open},

(Cx ∧ 𝔥x = e_{C}) → 𝔤𝔥x = 𝔤x and (x = e_{C} ∧ 𝔥x ≠ s) → 𝔤𝔥x = x

for each C ∈ Φ_{tan}, and Cx → 𝔤𝔥x = x for each C ∈ Φ_{trans} ∪Φ_{single}.

Lemma 7.1. T (Φ) ⊢ Θ_{(𝔤,𝔥)}.

Proof. Let M ⊧ T (Φ), and let a ∈ M be such that a ∉ ⋃_{C∈Φ_{0}} C. Then by (F1), either a = c for some c ∈ Φ_{single}, or a = s. In the latter case, we have 𝔤(𝔥(a)) = 𝔥(𝔤(a)) = a by (F5), so we may assume that a = c for some c ∈ Φ_{single}. Then 𝔥(𝔤(a)) = 𝔤(𝔥(a)) = a by (F7)–(F9).

The proofs of the other conjuncts is similar, using also (F12); we leave the details to the reader. □

Corollary 7.2. Let ϕ be any quantifier-free L(Φ)-formula. Then ϕ is equivalent in T (Φ) to a quantifier-free formula ϕ′ such that no term occurring in ϕ′ contains both the symbols 𝔣 and 𝔟.

Proof. By induction on l := max{length(t) : t is a term occurring in ϕ}, using Lemma 7.1. □

For the remainder of this section, we fix an arbitrary model M of T (Φ). To simplify notation, we omit the superscript M below and write \overline{C} := C ∪ {min(C), max(C)} for C ∈ Φ_{1}.

Definition 7.3. Let C ∈ Φ_{1} and k ∈ ℕ. We define

G_{C}^{k} := {𝔤^{l}(z) : z is a constant, 0 ≤ l ≤ k and 𝔤^{l}(z) ∈ C},

and we let O_{C}^{k} be the collection of all possible order types of pairs (a, b) ∈ \overline{C}^{2} over G_{C}^{k}. In addition, for ζ_{0}, ζ_{1} ∈ \overline{C} and D ∈ Φ_{1}, we put

𝔤_{D}^{−k}(ζ_{0}, ζ_{1}) := {x ∈ D : ζ_{0} <_{C} 𝔤^{k}(x) <_{C} ζ_{1}}

and

H_{D}^{k}(ζ_{0}, ζ_{1}) := {𝔥^{l}(z) : z ∈ {ζ_{0}, ζ_{1}} or z is a constant,

0 ≤ l ≤ k and 𝔥^{l}(z) ∈ D}.

Note that G_{C}^{k} and H_{D}^{k}(ζ_{0}, ζ_{1}), and hence O_{C}^{k}, are finite sets whose cardinality is bounded by a number depending only on the language and k, but independent of M, C, D, ζ_{0} or ζ_{1}.

Proposition 7.4. Let C, D ∈ Φ_{1}, ζ_{0}, ζ_{1} ∈ \overline{C} and k ∈ ℕ.

(1) The set 𝔤_{D}^{−k}(ζ_{0}, ζ_{1}) is a union of points in H_{D}^{k}(ζ_{0}, ζ_{1}) and open intervals with endpoints in H_{D}^{k}(ζ_{0}, ζ_{1}).

(2) For each ϑ ∈ O_{C}^{k}, there is a conjunction σ_{ϑ}(x, y_{0}, y_{1}) of atomic formulas with free variables x, y_{0} and y_{1} such that whenever (ζ_{0}, ζ_{1}) have order type ϑ over G_{C}^{k}, the set 𝔤_{D}^{−k}(ζ_{0}, ζ_{1}) is defined by the formula σ_{ϑ}(x, ζ_{0}, ζ_{1}).

(3) 𝔤^{k} restricted to 𝔤_{D}^{−k}(ζ_{0}, ζ_{1}) is continuous.

Proof. Note that for every x ∈ 𝔤_{D}^{−k}(ζ_{0}, ζ_{1}), there is a sequence E = (E_{0}, …, E_{k}) of elements of Φ_{2} := Φ_{1} ∪ {{c} : c ∈ Φ_{single}} ∪ {{e_{C}} : C ∈ Φ_{tan}} such that E_{0} = D, E_{k} = C and 𝔤^{i}(x) ∈ E_{i} for i = 0, …, k. Thus, we fix a sequence E = (E_{0}, …, E_{k}) ∈ Φ_{2}^{k+1} with E_{k} = C, and we define the set

𝔤_{E}^{−k}(ζ_{0}, ζ_{1}) := {x ∈ M : 𝔤^{i}(x) ∈ E_{i} for i = 0, …, k, ζ_{0} <_{C} 𝔤^{k}(x) <_{C} ζ_{1}};

it suffices to prove the proposition with 𝔤_{E}^{−k}(ζ_{0}, ζ_{1}) and H_{E_{0}}^{k}(ζ_{0}, ζ_{1}) in place of 𝔤_{D}^{−k}(ζ_{0}, ζ_{1}) and H_{D}^{k}(ζ_{0}, ζ_{1}).

Next, we note that if E_{i} ∈ {{c} : c ∈ Φ_{single}} ∪ {{e_{C}} : C ∈ Φ_{tan}} for some i ∈ {1, …, k−1}, then a ∈ 𝔤_{E}^{−k}(ζ_{0}, ζ_{1}) if and only if 𝔤^{i}(a) is the unique constant in E_{i} and ζ_{0} <_{C} 𝔤^{k}(a) <_{C} ζ_{1}, so the proposition follows in this case.

We therefore assume from now on that E_{i} ∈ Φ_{1} for each i = 0, …, k, and in this case we prove the proposition with part (1) replaced by

(1)’ The set 𝔤_{E}^{−k}(ζ_{0}, ζ_{1}) is an open interval with endpoints in H_{E_{0}}^{k}(ζ_{0}, ζ_{1}). We proceed by induction on k. The case k = 0 is trivial, so we assume that k > 1. By Axiom (F8), the set 𝔤_{(E_{k−1},E_{k})}^{−1}(ζ_{0}, ζ_{1}) is an open interval whose endpoints η_{0}, η_{1} belong to the set H_{E_{k−1}}^{1}(ζ_{0}, ζ_{1}) and are determined by the order type of (ζ_{0}, ζ_{1}) over G_{E_{k}}^{1}. In fact, we claim that the order type of (η_{0}, η_{1}) over G_{E_{k−1}}^{k−1} is determined by the order type of (ζ_{0}, ζ_{1}) over G_{E_{k}}^{k}; together with the inductive hypothesis applied to 𝔤_{(E_{0},...,E_{k−1})}^{k−1}(η_{0}, η_{1}), the proposition then follows, because H_{E_{0}}^{k−1}(c, d) is contained in H_{E_{0}}^{k}(ζ_{0}, ζ_{1}) for all c, d ∈ H_{E_{k−1}}^{1}(ζ_{0}, ζ_{1}).

To see the claim, assume first that E_{k} = E_{C} for some C ∈ Φ_{open}. Then by Axiom (F8), the set {𝔤(z) : z ∈ G_{E_{k−1}}^{k−1}} is contained in G_{E_{k}}^{k} and the claim follows in this case. So we assume that E_{k} ∈ Φ_{trans}. Then by Axiom (F13), E_{k−1} = E_{C} for some C ∈ Φ_{open} and there are constants a and b such that

(η_{0}, η_{1}) ⊆ (a, b) = 𝔤^{−1}(E_{k}) = h(E_{k}) (as intervals).

Hence the order type of (η_{0}, η_{1}) over G_{E_{C}}^{k−1} is determined by the order type of (η_{0}, η_{1}) over the set G′ := {z ∈ G_{E_{C}}^{k−1} : a <_{C} z <_{C} b} . Then again by Axiom (F8), the set {𝔤(z) : z ∈ G′} is contained in G_{E_{k}}^{k} and the claim also follows in this case. □

Corollary 7.5. Let C ∈ Φ_{1} and put G := 𝔤_{C}^{−N}(min(C), max(C)).

(1) The set Bd_{C}(M) is a closed and nowhere dense subset of G.

(2) Assume that Φ = Φ_{ξ} and M ≡ M_{ξ} for some definable vector field ξ of class C^{1} on ℝ^{2}. Then for every c ∈ G \ Bd_{C}(M), there are a, b ∈ \overline{C} such that

a = sup \{x ∈ Bd_{C}(M) ∪ (\overline{C} \ G) : x <_{C} c\}

and

b = inf \{x ∈ Bd_{C}(M) ∪ (\overline{C} \ G) : c <_{C} x\} .

Proof. Part (1) follows from the continuity of 𝔤^{N}|_{G} and the definition of the set Bd_{C}(M). Part (2) follows from part (1) and the fact that C^{M_{ξ}} is complete. □

Finally, for each C ∈ Φ_{1} we let \overline{C}x abbreviate Cx ∨ x = min(C) ∨ x = max(C). We let G^{k} be the set of all L(Φ)-terms 𝔤^{j}c such that 0 ≤ j ≤ k and c is a constant symbol, and we let O^{k} be the set of all formulas of the form

(\overline{C}y_{0} ∧ \overline{C}y_{1}) ∧ ⋀_{\{τ,ρ\}⊆G^{k}∪\{y_{0},y_{1}\}}(τ ∗_{\{τ,ρ\}} ρ),

where C ∈ Φ_{1} and ∗_{{τ,ρ}} ∈ {<_{C}, >_{C}, =, ≠}. The cardinalities of G^{k} and O^{k} are bounded by a number depending only on k (and on L(Φ)). Moreover in M, each formula ϑ ∈ O^{k} determines an order type in O_{C}^{k}, for some C ∈ Φ_{1}; and conversely, every order type in O_{C}^{k} with C ∈ Φ_{1} is determined by some formula ϑ ∈ O^{k}. Thus we obtain the following from Proposition 7.4:

Corollary 7.6. Let k ∈ ℕ. Then there are l = l(k) ∈ ℕ and quantifier-free formulas ϑ_{1}^{k}(y_{0}, y_{1}), …, ϑ_{l}^{k}(y_{0}, y_{1}) with free variables y_{0} and y_{1} such that

(1) T (Φ) ⊢ ⋁_{i=1}^{l} ϑ_{i}^{k}(y_{0}, y_{1}) ↔ ⋁_{C∈Φ_{1}}(\overline{C}y_{0} ∧ \overline{C}y_{1});

(2) for every D ∈ Φ_{1} there are quantifier-free formulas σ_{i}^{D,k}(x, y_{0}, y_{1}) with free variables x, y_{0} and y_{1}, i = 1, …, l, such that if M ⊧ ϑ_{i}^{k}(ζ_{0}, ζ_{1}) for ζ_{0}, ζ_{1} ∈ M and some i, then the set 𝔤_{D}^{−k}(ζ_{0}, ζ_{1}) is defined by the formula σ_{i}^{D,k}(x, ζ_{0}, ζ_{1}). □

Remark 7.7. We obtain analogous statements to Proposition 7.4 and Corollary 7.6 if we replace the open interval (ζ_{0}, ζ_{1}) by a half-open or closed interval.

8. Dulac flow configurations

It is clear from Remark 6.8 that, for a vector field ξ on ℝ^{2} definable in R, the set of boundary cycles of ξ is represented in M_{ξ} by the definable sets Bd_{C}(M). The following example shows that the theory T (Φ) has hardly any implications for the nature of these sets.

Example 8.1. Consider the vector field ζ of Example 3.2, and let C be the piecewise trivial decomposition obtained there. We denote by Φ_{ζ} the flow configuration corresponding to this C, and write C_{0} := {(x, y) : x > 0, y = 0} ∈ C. We show here how to define, given any closed and nowhere dense subset F of C_{0}, a vector field ζ′ of class C^{∞} for which Φ_{ζ} is still a flow configuration and such that Bd_{C_{0}}(M_{ζ′}) = F.

First, given 0 < a < b < ∞, we let d_{(a,b)} : ℝ^{2} ⟶ ℝ be the function d_{(a,b)}(x, y) := (b^{2} − (x^{2} + y^{2}))((x^{2} + y^{2}) − a^{2}), and we let e_{(a,b)} : ℝ^{2} ⟶ ℝ be the C^{∞} function defined by e_{(a,b)}(x, y) := exp(−1/d_{(a,b)}(x, y)). We let ζ_{(a,b)} be the vector field of class C^{∞} on the annulus A_{(a,b)} := {(x, y) : d_{(a,b)}(x, y) > 0} defined by

ζ_{(a,b)} := − (y + e_{(a,b)}(x, y)x) \frac{∂}{∂x} + (x − e_{(a,b)}(x, y)y) \frac{∂}{∂y} .

Second, let F ⊆ C_{0} be an arbitrary closed and nowhere dense subset. Then C_{0} \ F is open in C_{0} and hence the union of countably many disjoint open intervals I_{0}, I_{1}, I_{2}, . . .. We let ζ′ be the vector field on ℝ^{2} of class C^{∞} defined by

ζ′(x, y) := \begin{cases}ζ_{I_{j}}(x, y) & if (x, y) ∈ A_{I_{j}} for some j ∈ ℕ, \\ ζ(x, y) & otherwise. \end{cases}

(Note that by Wilkie’s Theorem [13], ζ′ is definable in some o-minimal expansion of the real field if and only if F is finite.)

In view of the previous example, we now introduce a strengthening of the setting described in Section 6.

Definition 8.2. A Dulac flow configuration Ψ is a pair (Φ, ν) such that Φ is a flow configuration and ν ∈ ℕ.

Example 8.3. Let ξ be a definable vector field on ℝ^{2} of class C^{1}. Let Φ = Φ_{ξ} be a flow configuration associated to ξ as in Example 6.2 and let M_{ξ} be the associated L(Φ_{ξ})-structure described in Example 6.4. Assume that there is a ν ∈ ℕ such that for each C ∈ Φ_{1}, the set Bd_{C}(M_{ξ}) has cardinality at most ν. Then Ψ_{ξ} := (Φ_{ξ}, ν) is called a Dulac flow configuration associated to ξ.

For the remainder of this section, we fix a Dulac flow configuration Ψ = (Φ, ν).

Definition 8.4. The language L(Ψ) consists of the symbols of L(Φ) together with the following symbols for each C ∈ Φ_{1}:

(i) binary predicates R_{C} and S_{m,C}^{𝔣}, B_{m,C}^{𝔣}, S_{m,C}^{𝔟} and B_{m,C}^{𝔟} for each m ∈ ℕ; (ii) constant symbols γ_{C}^{1}, …, γ_{C}^{ν}.

We put Γ = Γ(Ψ) := {γ_{C}^{j} : C ∈ Φ_{1}, j = 1, …, ν}.

Example 8.5. Let ξ be a definable vector field on ℝ^{2} of class C^{1}, and let M_{ξ} be an L(Φ_{ξ})-structure associated to ξ as in Example 6.4. Assume that there is a ν ∈ ℕ such that for each C ∈ C_{trans} ∪ C_{open}, the set Bd_{C}(M_{ξ}) has cardinality at most ν, and let Ψ_{ξ} be a Dulac flow configuration associated to ξ as in Example 8.3. We expand M_{ξ} into an L(Ψ_{ξ})-structure M_{ξ}^{D} as follows: for each C ∈ Φ_{1},

(i) R_{C} is interpreted as the set

\{(x, y) ∈ \overline{C}^{2} : ∃z(x <_{C} z <_{C} y ∧ Fix_{C}(z)) ∨ (x = y ∧ Fix_{C}(x))\};

(ii) for m ∈ ℕ, 𝔤 ∈ {𝔣, 𝔟} and G ∈ {S_{m,C}^{𝔤}, B_{m,C}^{𝔤}}, we put

∗ := \begin{cases}<_{C} & if G is S_{m,C}^{𝔤}, \\ >_{C} & if G is B_{m,C}^{𝔤}, \end{cases}

and we interpret G as the union of the sets

\{(x, y) ∈ \overline{C}^{2} : ∃z(Cz ∧ x <_{C} z <_{C} y ∧ C𝔤^{m}(z) ∧ 𝔤^{m}(z) ∗ z)\}

and the set {(x, x) : Cx ∧ C𝔤^{m}(x) ∧ 𝔤^{m}(x) ∗ x}; (iii) if a_{1} <_{C} ⋯ <_{C} a_{m} are the points in C that lie on boundary cycles of

ξ, we interpret γ_{C}^{j} as a_{j} if 1 ≤ j ≤ m and as max(C) if m < j ≤ ν. This completes the description of M_{ξ}^{D}.

Definition 8.6. Inspired by the previous example, we let T (Ψ) be the L(Ψ)- theory consisting of T (Φ) and the universal closures of the formulas in the axiom schemes (D1)–(D6) below. (D1) For each C ∈ Φ_{1}, m ∈ ℕ and G ∈ {R_{C}, S_{m,C}^{𝔣}, B_{m,C}^{𝔣}, S_{m,C}^{𝔟}, B_{m,C}^{𝔟}}, the

formulas

(a) Gxy → (\overline{C}x ∧ \overline{C}y),

(b) Gxy → (x ≤_{C} y ∨ (x = min(C) ∧ y = max(C))). (D2) For each C ∈ Φ_{1} the formulas

(a) R_{C}xy ↔ ∃z(x <_{C} z <_{C} y ∧ Fix_{C}(z)), and

(b) R_{C}xx ↔ Fix_{C}(x). (D3) For each m ∈ ℕ, C ∈ Φ_{1} and 𝔤 ∈ {𝔣, 𝔟} the formulas (a) (S_{m,C}^{𝔤}xy) ↔ ∃z(x <_{C} z <_{C} y ∧ 𝔤^{m}(z) <_{C} z),

(b) (S_{m,C}^{𝔤}xx) ↔ (Cx ∧ 𝔤^{m}x <_{C} x),

(c) (B_{m,C}^{𝔤}xy) ↔ ∃z(x <_{C} z <_{C} y ∧ z <_{C} 𝔤^{m}(z)),

(d) (B_{m,C}^{𝔤}xx) ↔ (Cx ∧ x <_{C} 𝔤^{m}x). (D4) For each m ∈ ℕ, C ∈ Φ_{1}, 𝔤 ∈ {𝔣, 𝔟} and G ∈ {R_{C}, B_{m,C}^{𝔤}, S_{m,C}^{𝔤}} the

formula

(Gxy ∧ ∀z (x <_{C} z <_{C} y → \overline{C}𝔤^{m}z) ∧ ¬∃z (x <_{C} z <_{C} y ∧ Bd_{C}(z))) → ∀z(x <_{C} z <_{C} y → Gzz).

(D5)_{ν} For each C ∈ Φ_{1} the formulas (a) \overline{C}γ_{C}^{j} ∧ (Cγ_{C}^{j} → Fix_{C}(γ_{C}^{j})) for j = 0, …, ν,

(b) γ_{C}^{j} ≤_{C} γ_{C}^{j+1} ∧ (γ_{C}^{j} = γ_{C}^{j+1} → γ_{C}^{j} = max(C)) for j = 0, …, ν − 1. (D6)_{ν} For each C ∈ Φ_{1} the formula

(Cx ∧ Bd_{C}(x)) ↔ ⋁_{j=1}^{ν} (x = γ_{C}^{j} ∧ Cγ_{C}^{j}) .

This completes the description of the axioms.

Proposition 8.7. If ξ is a definable vector field on ℝ^{2} of class C^{1} with finitely many boundary cycles, then M_{ξ}^{D} ⊧ T (Ψ_{ξ}).

Proof. This is almost immediate from the definition of M_{ξ}^{D} and Proposition 6.6, except perhaps for Axiom (D4), which follows from Proposition 7.4 and the fact that every bounded subset of ℝ has an infimum. □

Remark 8.8. Let T (Φ)′ be the union of T (Φ) with Axioms (D1)–(D4) only. Since (D1)–(D3) just extend T (Φ) by definitions in the sense of Section 4.6 in Shoenfield [11], the argument in the proof of the previous proposition shows that any L(Φ_{ξ})-structure M_{ξ} as defined in Example 6.4 can be expanded to a model M′_{ξ} of T (Φ)′.

9. Quantifier elimination for T (Ψ)

We fix a Dulac flow configuration Ψ = (Φ, ν); our ultimate goal is to show that T (Ψ) eliminates quantifiers. Most of the work in this section goes towards showing that, in order to eliminate quantifiers, we need only consider formulas of the form ∃yϕ(x, y) where ϕ is of a special form.

Terminology. Let x = (x_{1}, …, x_{m}) be a tuple of variables and y and z single variables. To simplify terminology, we write “term” and “formula” for “L(Ψ)- term” and “L(Ψ)-formula”. For a formula ϕ, we write ϕ(x, y) to indicate that the free variables of ϕ are among x_{1}, …, x_{m} and y. A binary atomic formula is a formula of the form At_{1}t_{2}, where A is a binary relation symbol in L(Ψ) and t_{1} and t_{2} are terms.

For this section fix an arbitrary model M of T (Ψ); again, we omit the superscript M when interpreting predicates in M.

Definition 9.1. An order formula is a quantifier-free L(Φ) ∪ Γ-formula. A z-order formula is a quantifier-free formula ϕ such that every atomic subformula of ϕ containing z is an L(Φ) ∪ Γ-formula.

A z-order formula ϕ is minimal if the only subterm of ϕ containing z is z itself and every binary atomic subformula At_{1}t_{2} of ϕ is such that at most one of t_{1} and t_{2} contains z.

Our first goal is to show that we may, in order to prove quantifier elimination, restrict our attention to y-order formulas. This argument is based on the following lemma, which will also be of use later.

Lemma 9.2. Let G ∈ L(Ψ) \ L(Φ).

(1) The formula Gyy is equivalent in T (Ψ) to a minimal y-order formula ψ(y).

(2) The formula Gyz is equivalent in T (Ψ) to a formula ψ(y, z) that is both a minimal y-order formula and a minimal z-order formula.

Proof. Let C ∈ Φ_{1}, m ∈ ℕ and 𝔤 ∈ {𝔣, 𝔟} be such that G ∈ {R_{C}, S_{m,C}^{𝔤}, B_{m,C}^{𝔤}}. In this proof, we write < instead of <_{C}; if G is R_{C}, we assume m = N = N_{Φ}. By Corollary 7.6(1), any formula ϕ is equivalent in T (Ψ) to the conjunction of the formulas ϑ_{i} → ϕ, where i ∈ {1, …, l(m)} and ϑ_{i} is the formula ϑ_{i}^{m}(min(C), max(C)). Hence it suffices to prove the lemma with each ϑ_{i} → Gyy in place of Gyy and each ϑ_{i} → Gyz in place of Gyz; so we also fix an i below and write ϑ in place of ϑ_{i}. Now by Corollary 7.6(2), there are finitely many terms α_{j}^{0}, α_{j}^{1} for 1 ≤ j ≤ r, built up exclusively from constants, such that whenever M ⊧ ϑ the set {z ∈ C : 𝔤^{m}(z) ∈ C} is the union of the open intervals I_{j} = (α_{j}^{0}, α_{j}^{1}) and points α_{j}^{0} = α_{j}^{1}.

(1) We claim that the formula ϑ → Gyy is equivalent to ϑ → ψ^{G}, where ψ^{G} is of the form

Cy ∧ ( ⋁_{1≤j≤r}(α_{j}^{0} < y < α_{j}^{1} ∨ α_{j}^{0} = y = α_{j}^{1})) ∧ ( ⋁_{β∈Y} ψ_{β}^{G} ∨ ⋁_{β_{0},β_{1}∈Y} ψ_{β_{0},β_{1}}^{G})

with Y := Γ∪{α_{j}^{l} : l ∈ {0, 1} and 1 ≤ j ≤ r}, and for each β ∈ Y, the formula ψ_{β}^{G} is Cy ∧ ((y = β ∧ Gββ) ∨ y = t^{G}) with

t^{G} the term \begin{cases}y & if G is R_{C}, \\ 𝔥^{m} min(C) & if G is S_{m,C}^{𝔤}, \\ 𝔥^{m} max(C) & if G is B_{m,C}^{𝔤}, \end{cases}

and for each β_{0}, β_{1} ∈ Y, the formula ψ_{β_{0},β_{1}}^{G} is of the form

(Cβ_{0} ∨ β_{0} = min(C)) ∧ (Cβ_{1} ∨ β_{1} = max(C)) ∧ β_{0} < y < β_{1} ∧ η_{β_{0},β_{1}}^{G},

where

η_{β_{0},β_{1}}^{G} is \begin{cases}¬S_{N,C}^{𝔤}β_{0}β_{1} ∧ ¬B_{N,C}^{𝔤}β_{0}β_{1} & if G is R_{C}, \\ ¬B_{m,C}^{𝔤}β_{0}β_{1} ∧ ¬R_{C}β_{0}β_{1} & if G is S_{m,C}^{𝔤}, \\ ¬S_{m,C}^{𝔤}β_{0}β_{1} ∧ ¬R_{C}β_{0}β_{1} & if G is B_{m,C}^{𝔤}. \end{cases}

Note that ϑ → ψ^{G} is a minimal y-order formula; thus, the proof of part (1) is finished once we prove the claim.

We prove the claim for R_{C}; the other cases of G are similar and left to the reader. Suppose that M ⊧ ϑ and pick an a ∈ M such that M ⊧ R_{C}aa. Then M ⊧ α_{j}^{0} ≤ a ≤ α_{j}^{1} for some j ∈ {1, … r}. If a = β for some β ∈ Y, we are done, so we assume a ≠ β for all β ∈ Y. Then there are β_{0}, β_{1} ∈ Y such that M ⊧ β_{0} < a < β_{1} and M ⊧ ¬(β_{0} < β < β_{1}) for every β ∈ Y. Hence by Axiom (D4), M ⊧ R_{C}bb for every b ∈ (β_{0}, β_{1}), so M ⊧ ¬S_{m,C}^{𝔤}β_{0}β_{1} ∧ ¬B_{m,C}^{𝔤}β_{0}β_{1} as required. The converse of the claim is immediate.

(2) The formula ϑ → Gyz is in turn equivalent in T (Ψ) to

ϑ → (Gyz ∧ (y = min(C) ∨ y = max(C) ∨ Cy));

since the lemma is immediate for the formulas ϑ → (Gyz ∧ y = min(C)) and ϑ → (Gyz ∧ y = max(C)), we need only consider ϑ → (Gyz ∧ Cy). We claim that the latter is equivalent to ϑ → ψ^{G}, where ψ^{G} is of the form

Cy ∧ (Cz ∨ z = max(C)) ∧ y ≤ z ∧ ((y = z ∧ Gyy) ∨ (y < z ∧ η^{G})) ,

η^{G} is the formula

⋁_{β∈Y} (y = β ∧ Gβz) ∨ ⋁_{β∈Y} (y < β < z ∧ Gββ) ∨ ⋁_{β_{o},β_{1}∈Y, 1≤j≤r} η_{β_{0},β_{1},j}^{G}

and for each β_{0}, β_{1} ∈ Y and j ∈ {1, …, r}, the formula η_{β_{0},β_{1},j}^{G} is

β_{0} < y ∧ z < β_{1} ∧ α_{j}^{0} ≤ β_{0} ∧ β_{1} ≤ α_{j}^{1} ∧ Gβ_{0}β_{1} ∧ η_{β_{0},β_{1}}^{G}

with η_{β_{0},β_{1}}^{G} defined as for part (1).

We again prove the claim for R_{C}, leaving the other cases of G to the reader. Suppose that M ⊧ ϑ and M ⊧ R_{C}ab ∧ Cb and work inside M. Suppose that a ≠ β for all β ∈ Y and that M ⊧ ¬(a < β < b ∧ R_{C}ββ) for every β ∈ Y. Then 𝔣^{N}(d) = d for some d ∈ (a, b), and d ∈ (α_{j}^{0}, α_{j}^{1}) for some j. Moreover, there are β_{0}, β_{1} ∈ Y such that d ∈ (β_{0}, β_{1}) and β ∉ (β_{0}, β_{1}) for every β ∈ Y. Hence by Axiom (D4), we get M ⊧ ¬S_{N,C}^{𝔤}β_{0}β_{1} ∧¬B_{N,C}^{𝔤}β_{0}β_{1}, as required. The converse of the claim is straightforward.

By symmetry, a similar claim holds with ϑ → (Gyz ∧ Cz) in place of ϑ → (Gyz ∧Cy). Combining these two claims with part (1) now yields part(2). □

Corollary 9.3. Every quantifier-free formula ϕ(x, y) is equivalent in T (Ψ) to a y-order formula ψ(x, y).

Proof. It suffices to prove the proposition for all atomic formulas; the relevant atomic formulas are handled in Lemma 9.2. □

Our second goal of this section is to show that we only need consider, for quantifier elimination, y-order formulas in which the complexity of any term involving y is as low as possible. Minimal y-order formulas are examples of such y-order formulas; but we cannot always reduce to minimal y-order formulas.

Definition 9.4. Let t be a term. The z-height h_{z}(t) of t is defined as follows: (i) if z does not occur in t, then h_{z}(t) := 0; (ii) h_{z}(z) := 1; (iii) if t is 𝔣t′ or 𝔟t′ for some term t′ and z occurs in t′, then h_{z}(t) := h_{z}(t′)+1. Let At_{1}t_{2} be a binary atomic formula; the z-height h_{z}(At_{1}t_{2}) of At_{1}t_{2} is

defined as the pair (a, b) ∈ ℕ^{2}, where

a := \begin{cases}1 & if z occurs in both t_{1} and t_{2}, \\ 0 & otherwise, \end{cases}

and

b := \begin{cases}min\{h_{z}(t_{1}), h_{z}(t_{2})\} & if z occurs in both t_{1} and t_{2}, \\ max\{h_{z}(t_{1}), h_{z}(t_{2})\} & otherwise. \end{cases}

Let Bt be a unary atomic formula; the z-height h_{z}(Bt) of Bt is defined by h_{z}(Bt) := (0, h_{z}(t)) ∈ ℕ^{2}.

Let ϕ be a quantifier-free formula; the z-height h_{z}(ϕ) of ϕ is the maximum of the set {h_{z}(ψ) : ψ is an atomic subformula of ϕ} with respect to the lexicographic ordering of ℕ^{2}. We write h_{z}(ϕ) = (h_{z}^{1}(ϕ), h_{z}^{2}(ϕ)) below.

Finally, a term t is mixed if it contains both function symbols 𝔣 and 𝔟; otherwise t is called unmixed.

Example 9.5. Let ϕ be a z-order formula. Then h_{z}(ϕ) ≤ (0, 1) if and only if ϕ is minimal.

Lemma 9.6. Let ϕ(x, y) be a y-order formula. Then there is a y-order formula ψ(x, y) that contains no mixed terms such that ϕ and ψ are equivalent in T (Ψ) and h_{y}(ψ) ≤ h_{y}(ϕ).

Proof. Let ϕ′ be the L(Φ)-formula obtained from ϕ by replacing each constant γ_{C}^{j} by a new variable z_{C}^{j}, for C ∈ Φ_{1} and j = 1, …, ν. By Lemma 7.1, ϕ′ is equivalent in T (Φ) to a quantifier-free L(Φ)-formula ψ′ that is a disjunction of formulas of the form η ∧ξ, where ξ is obtained from ϕ′ by replacing each mixed subterm by an unmixed term of lower y-height, and where η is a conjunction of some of the premises of the implications occurring in Θ_{(𝔣,𝔟)} and in Θ_{(𝔟,𝔣)} with x there replaced by various unmixed subterms of ϕ′. Clearly h_{y}(ξ) ≤ h_{y}(ϕ′) for every such ξ; since h_{y}^{1}(η) = 0 for every such η, it follows that h_{y}(ψ′) ≤ h_{y}(ϕ′) if h_{y}^{1}(ϕ′) = 1. On the other hand, if h_{y}^{1}(ϕ′) = 0, then every subterm t of ϕ′ satisfies h_{y}(t) ≤ h_{y}^{2}(ϕ′); so h_{y}(η) ≤ h_{y}(ϕ′) for every such η. Therefore, we always have h_{y}(ψ′) ≤ h_{y}(ϕ′) = h_{y}(ϕ), and we let ψ be the y-order formula obtained from ψ′ by replacing each variable z_{C}^{j} again by γ_{C}^{j}. □

Below we let ι(y) denote the formula ⋀_{C∈Φ_{open}} Cy → E_{C}y and we put

T′ := T (Ψ) ∪ {ι(y)}.

Lemma 9.7. Let ϕ(x, y) be a y-order formula. Then there is a y-order formula ψ(x, y) such that ϕ is equivalent in T′ to ψ and h_{y}^{2}(ψ) ≤ 1.

Proof. By induction on h_{y}(ϕ); the case where h_{y}^{2}(ϕ) ≤ 1 is trivial, so we assume that h_{y}^{2}(ϕ) > 1 and we prove that

(∗) there exists an order formula ψ(x, y) such that ϕ is equivalent in T′ to

ψ and h_{y}(ψ) < h_{y}(ϕ). To do so, we fix arbitrary (𝔤, 𝔥) ∈ {(𝔣, 𝔟), (𝔟, 𝔣)}, a unary predicate P, a C ∈ Φ_{0} and terms t_{1} and t_{2}, and we assume that y occurs in t_{1}, and either y does not occur in t_{2} or h_{y}(t_{1}) < h_{y}(t_{2}). By the definition of h_{y}(ϕ) and Axiom (F5), it suffices to prove (∗) with each of the atomic formulas P 𝔤t_{1}, 𝔤t_{1} = t_{2}, 𝔤t_{1} <_{C} t_{2} and t_{2} <_{C} 𝔤t_{1} in place of ϕ.

Case 1: ϕ is P 𝔤t_{1}. By Axioms (F7)–(F9), the formula ϕ is equivalent in T′ to ψ, where ψ is the formula depending on P defined as follows:

• if P ∈ Φ_{open} or P is E_{F} for some F ∈ Φ_{open}, then ψ is

⋁_{D∈Φ_{trans}, P =D^{𝔥}} Dt_{1} ∨ ⋁_{d∈Φ_{single}, P =d^{𝔥}} t_{1} = d;

• if P ∈ Φ_{tan}, then ψ is the formula t_{1} = 𝔥e_{P};
• if P ∈ Φ_{trans}, then ψ is the formula E_{P^{𝔥}}t_{1}.

In each case of ψ above, we have h_{y}(ψ) < h_{y}(ϕ), as required.

Case 2: ϕ is 𝔤t_{1} = t_{2}. Then by Axioms (F5), (F7)–(F9) and (F13) the formula ϕ is equivalent in T′ to ψ, where ψ is the conjuction of the formulas

(i) t_{2} = s ∨ ⋁_{C∈Φ_{1}} Ct_{2} ∨ ⋁_{c∈Φ_{single}} t_{2} = c ∨ ⋁_{C∈Φ_{tan}} t_{2} = e_{C},

(ii) t_{2} = c → t_{1} = 𝔥c for each constant c different from s,

(iii) t_{2} = s → ((t_{1} = s)∨

⋁_{C∈Φ_{open}} (E_{C}t_{1} ∧ ⋀_{D∈S_{C}} ¬(r_{D}^{𝔥} <_{C} t_{1} <_{C} s_{D}^{𝔥}) ∧ ⋀_{c∈Φ_{single}}(¬t_{1} = 𝔥c))∨

⋁_{C∈Φ_{tan}}(𝔤e_{C} <_{C} t_{1} ≤_{C} e_{C} ∨ e_{C} ≤_{C} t_{1} <_{C} 𝔤e_{C}) ∧ 𝔤e_{C} = s))

with S_{C} := {D ∈ Φ_{trans} : D^{𝔥} = C}, (iv) Ct_{2} → t_{1} = 𝔥t_{2} for C ∈ Φ_{1}.

If y does not occur in t_{2}, then h_{y}(ψ) < h_{y}(ϕ); so we assume that y occurs in t_{2}. In this case, the only atomic subformula ξ of ψ with h_{y}^{1}(ξ) = 1 is t_{1} = 𝔥t_{2}, and h_{y}(t_{1} = 𝔥t_{2}) = (1, h_{y}(t_{1})) < (1, h_{y}(𝔤t_{1})) = h_{y}(ϕ) by hypothesis, so h_{y}(ψ) < h_{y}(ϕ) as well.

Case 3: ϕ is 𝔤t_{1} <_{C} t_{2}. There are various subcases depending on C.

• If C ∈ Φ_{trans}, we write D := C^{𝔥}; then by Axioms (F8) and (F13) the formula ϕ is equivalent in T′ to ψ, where ψ is the conjunction of the formulas

(Ct_{2} ∨ t_{2} = max(C)) ∧ ((E_{D}t_{1} ∧ r_{C}^{𝔥} <_{D} t_{1} <_{D} r_{C}^{𝔥}) ∨ t_{1} = 𝔥 min(C))

and

(E_{D}t_{1} ∧ r_{C}^{𝔥} <_{D} t_{1} <_{D} r_{C}^{𝔥}) → (t_{1} <_{D} 𝔥t_{2} ∨ t_{2} = max(C)).

• If C ∈ Φ_{open}, then by Axioms (F2), (F9), (F10), (F12) and (F13) the formula ϕ is equivalent in T′ to ψ, where ψ is the conjunction of the formulas

(i) ⋁_{D∈Φ_{trans}, D^{𝔤}=C} Dt_{1} ∨ ⋁_{d∈Φ_{single}, P =d^{𝔥}} t_{1} = d,

(ii) E_{C}t_{2} ∨ (Ct_{2} ∧ ¬E_{C}t_{2} ∧ E_{C}𝔤t_{2}) ∨ (Ct_{2} ∧ ¬E_{C}t_{2} ∧ E_{C}𝔥t_{2}) ∨ (t_{2} =

max(C)), (iii) (Dt_{1} ∧ E_{C}t_{2}) → ((r_{D}^{𝔤} <_{C} t_{2} <_{C} s_{D}^{𝔤} ∧ t_{1} <_{D} 𝔥t_{2}) ∨ (s_{D}^{𝔤} ≤_{C} t_{2})) for

each D ∈ Φ_{trans} with D^{𝔤} = C, (iv) (Dt_{1}∧¬E_{C}t_{2}∧E_{C}𝔤t_{2}) → ((r_{D}^{𝔤} <_{C} 𝔤t_{2} <_{C} s_{D}^{𝔤} ∧t_{1} <_{D} 𝔥t_{2})∨(s_{D}^{𝔤} ≤_{C}

𝔤t_{2})) for each D ∈ Φ_{trans} with D^{𝔤} = C,

(v) (Dt_{1}∧¬E_{C}t_{2}∧E_{C}𝔥t_{2}) → ((r_{D}^{𝔤} <_{C} 𝔥t_{2} <_{C} s_{D}^{𝔤}∧t_{1} ≤_{D} 𝔥𝔥t_{2})∨(s_{D}^{𝔤} ≤_{C} 𝔥t_{2})) for each D ∈ Φ_{trans} with D^{𝔤} = C,

(vi) t_{1} = d → 𝔤d <_{C} t_{2} for d ∈ Φ_{single} with P = d^{𝔥}.

• If C ∈ Φ_{tan}, then by Axioms (F2) and (F7) the formula ϕ is equivalent in T′ to ψ′, where ψ′ is

(Ct_{2} ∨ t_{2} = max(C)) ∧ ((t_{1} = 𝔥e_{C} ∧ e_{C} <_{C} t_{2}) ∨ 𝔤t_{1} = min(C)).

In this case we let ψ be the formula obtained from ψ′ by replacing the subformula 𝔤t_{1} = min(C) by the corresponding formula obtained in Case 2.

We leave it to the reader to verify that h_{y}(ψ) < h_{y}(ϕ) in each of these subcases.

Case 4: ϕ is t_{2} <_{C} 𝔤t_{1}. This case is similar to Case 3; we leave the details to the reader. □

Proposition 9.8. Let ϕ(x, y) be a quantifier-free formula. Then there is a minimal y-order formula ψ(x, y) such that ϕ is equivalent in T′ to ψ.

Proof. By Corollary 9.3 and Lemma 9.7, we may assume that ϕ is a y-order formula such that h_{y}^{2}(ϕ) ≤ 1. By Lemma 9.6, there is a y-order formula ψ′(x, y) such that ϕ is equivalent in T′ to ψ′, ψ′ contains no mixed terms and h_{y}(ψ) ≤ h_{y}(ϕ).

In particular, for every binary atomic subformula η of ψ′ in which both terms contain y, one of the terms is y itself and the other is either 𝔣^{m}y or 𝔟^{m}y for some m = m(η) ∈ ℕ. We now replace each such binary atomic subformula η of ψ′ with m(η) > 1 by the formula η′ defined as follows:

• if η is y = 𝔤^{m}y with 𝔤 ∈ {𝔣, 𝔟}, then η′ is the disjunction of the formulas y = c ∧ 𝔤^{m}c = c, for each constant symbol c, and C𝔤^{m}y ∧ R_{C}yy, for each C ∈ Φ_{1};

• if η is y <_{C} 𝔤^{m}y with 𝔤 ∈ {𝔣, 𝔟}, then η′ is B_{m,C}^{𝔤}yy;

• if η is 𝔤^{m}y <_{C} y with 𝔤 ∈ {𝔣, 𝔟}, then η′ is S_{m,C}^{𝔤}yy. We also replace each occurrence of y = y by s = s and each occurrence of y <_{C} y by s ≠ s, and we denote by ψ′′ be the resulting formula. Clearly h_{y}(ψ′′) ≤ h_{y}(ψ′), and every binary atomic subformula of ψ′′ in which both terms contain y is of the form Gyy for some G ∈ L(Ψ) \ L(Φ). Moreover by Axioms (D1)–(D4), (D5)_{ν} and (D6)_{ν}, the formula ψ′ is equivalent in T′ to ψ′′.

Next, we replace each subformula of ψ′′ of the form Gyy, where G ∈ L(Ψ) \ L(Φ), by the corresponding minimal y-order formula ψ(y) obtained in Lemma 9.2(1). If ψ′′′ is the resulting y-order formula, then ψ′′ is equivalent in T (Ψ) to ψ′′′ and h_{y}^{1}(ψ′′′) = 0.

Finally by Lemmas 9.7 and 9.6, there is a y-order formula ψ such that h_{y}(ψ) ≤ (0, 1), ψ contains no mixed terms and ψ is equivalent in T′ to ψ′′′. □

Finally, note that

T (Φ) ∪ {Cy} ⊧ ¬E_{C}y ↔ (C𝔣y ∨ C𝔟y)

for each C ∈ Φ_{open}, by Axioms (F5), (F10) and (F12). Hence, for each C ∈ Φ_{open} and each 𝔤 ∈ {𝔣, 𝔟}, we put T_{C,𝔤} := T (Ψ) ∪ {Cy ∧ C𝔤y}; by the previous proposition, it remains to reduce quantifier-free formulas in each T_{C,𝔤}. It turns out, however, that we cannot entirely reduce to minimal y-order formulas in these situations.

Instead, given 𝔤 ∈ {𝔣, 𝔟}, we call a formula ϕ 𝔤-almost minimal if ϕ is quantifier-free, the only subterms of ϕ containing z are z and 𝔤z and every binary atomic subformula At_{1}t_{2} of ϕ is such that at most one of t_{1} and t_{2} contains z.

Proposition 9.9. Let ϕ(x, y) be a quantifier-free formula, C ∈ Φ_{open} and 𝔤 ∈ {𝔣, 𝔟}. Then there is a 𝔤-almost minimal y-order formula ψ_{C,𝔤}(x, y) such that ϕ is equivalent in T_{C,𝔤} to ψ_{C,𝔤}.

Proof. By Corollary 9.3 and Lemma 9.6, we may assume that ϕ is a y-order formula containing no mixed terms. On the other hand, we have T ⊧ ι(𝔣y) and T ⊧ ι(𝔟y) by Axiom (F5). Let η(x, y) be an atomic subformula of ϕ; it suffices to show that there is a 𝔤-almost minimal y-order formula ξ_{η}(x, y) such that η and ξ_{η} are equivalent in T_{C,𝔤}. If h_{y}^{2}(η) = 0, there is nothing to do, so we assume h_{y}^{2}(η) > 0, and we distinguish two cases to define ξ_{η}.

Case 1: h_{y}^{2}(η) > 1. We first replace each occurrence of 𝔤y in η by a new variable z and each occurrence of 𝔥y in η by 𝔥z. Denote the resulting atomic formula by η′(x, z); by Axiom (F12), η′(x, 𝔤y) is equivalent in T_{C,𝔤} to η(x, y). By Proposition 9.8, the formula η′(x, z) is equivalent in T′ to a minimal z-order formula η′′(x, z). Since T (Ψ) ⊧ ι(𝔤y), it follows that η is equivalent in T_{C,𝔤} to the 𝔤-almost minimal y-order formula ξ_{η} given by η′′(x, 𝔤y).

Case 2: h_{y}^{2}(η) = 1. In this case, we take ξ_{η} equal to η if η contains a unary predicate symbol; so we assume that η is a binary atomic formula At_{1}t_{2}. If η is y = y, we take ξ_{η} to be s = s, and if η is y <_{D} y for some D ∈ Φ_{0}, we take ξ_{η} to be s ≠ s; so we also assume from now on that max{h_{y}^{2}(t_{1}), h_{y}^{2}(t_{2})} > 1. By Axiom (F5), the formulas y = 𝔤^{m}y, y = 𝔥^{m}y, y <_{D} 𝔤^{m}y, y <_{D} 𝔥^{m}y, 𝔤^{m}y <_{D} y and 𝔥^{m}y <_{D} y, for m > 0 and D ∈ Φ_{0} \ {C}, are all equivalent in T_{C,𝔤} to s ≠ s, so we are left with four subcases:

(i) if η is y <_{C} 𝔤^{m}y for some m > 0, then we let η′ be the formula (y <_{C} 𝔤y ∧ C𝔤^{m}y ∧ R_{C}𝔤y𝔤y) ∨ B_{m−1,C}^{𝔤}𝔤y𝔤y;

(ii) if η is y <_{C} 𝔥^{m}y for some m > 0, then we let η′ be the formula

(y <_{C} 𝔤y ∧ C𝔥^{m}y ∧ R_{C}𝔤y𝔤y) ∨ B_{m,C}^{𝔥}𝔤y𝔤y; (iii) if η is 𝔤^{m}y <_{C} y for some m > 0, then we let η′ be the formula

(𝔤y <_{C} y ∧ C𝔤^{m}y ∧ R_{C}𝔤y𝔤y) ∨ S_{m−1,C}^{𝔤}𝔤y𝔤y; (iv) if η is 𝔥^{m}y <_{C} y for some m > 0, then we let η′ be the formula

(𝔤y <_{C} y ∧ C𝔥^{m}y ∧ R_{C}𝔤y𝔤y) ∨ S_{m,C}^{𝔥}𝔤y𝔤y.

We claim that η and η′ are equivalent in T_{C,𝔤}. We prove this for Case (i); the other cases are similar and left to the reader. Let b ∈ M be such that M ⊧ Cb∧C𝔤b. Assume that M ⊧ b <_{C} 𝔤^{m}b∧¬B_{m−1,C}^{𝔤}𝔤b𝔤b. Then 𝔤^{m}b ∈ E_{C} and 𝔤^{m}b ≤_{C} 𝔤b by Axioms (F2) and (F5). Hence b <_{C} 𝔤b, so M ⊧ ϕ^{𝔣}(b, 𝔤b) by Axioms (F10) and (F12), which implies 𝔤^{m}b = 𝔤b as required. Conversely, assume first that M ⊧ b <_{C} 𝔤b ∧ C𝔤^{m}b ∧ R_{C}𝔤b𝔤b; then b <_{C} 𝔤^{m}b by Axioms (D2) and (F14). Now assume that M ⊧ B_{m−1,C}^{𝔤}𝔤b𝔤b; then 𝔤b <_{C} 𝔤^{m}b by Axiom (D3), and hence b <_{C} 𝔤^{m}b by Axioms (F10) and (F12).

Finally, by Proposition 9.8, the formulas B_{k,C}^{𝔤}zz, S_{k,C}^{𝔤}zz, C𝔤^{k}z ∧ R_{C}zz and C𝔥^{k}z ∧ R_{C}zz are each equivalent in T′ to minimal z-order formulas. It follows from the claim that we are left to dealing with Subcases (i)–(iv) for m = 1. But by Axioms (F5), (F10) and (F12) we have T_{C,𝔤} ⊧ ¬C𝔥y. Hence T_{C,𝔤} ⊧ ¬ϕ_{C}^{𝔥}(y, 𝔥y), so from Axioms (F10) and (F12) we get T_{C,𝔤} ⊧ ϕ_{C}^{𝔤}(y, 𝔤y). Therefore, y <_{C} 𝔤y is equivalent in T_{C,𝔤} to s = s if 𝔤 is 𝔣, and to ¬s = s if 𝔤 is 𝔟; the other subcases follow similarly. □

The previous two propositions allow us to reduce the problem of eliminating quantifiers in T (Ψ) to that of eliminating quantifiers in two simpler theories: for C ∈ Φ_{1} ∪ Φ_{tan} we let L_{C} be the language {<_{C}, min(C), max(C)} and T_{C} be the L_{C}-theory consisting of the universal closures of (A1) the sentences stating that <_{C} is a dense linear ordering on C, together

with the formula x = min(C)∨x = max(C)∨min(C) <_{C} x <_{C} max(C). For C ∈ Φ_{open} we let L_{C} be the language {<_{C}, π_{C}, E_{C}, min(C), max(C)}, where π_{C} a unary function symbol, and we let T_{C} be the L_{C}-theory consisting of the universal closures of (A1) as well as (B1) the formula E_{C}π_{C}x ∧ (E_{C}x → π_{C}x = x); (B2) the formula π_{C}x <_{C} x → ¬∃y(E_{C}y ∧ π_{C}x <_{C} y <_{C} x); (B3) the formula x <_{C} π_{C}x → ¬∃y(E_{C}y ∧ x <_{C} y <_{C} π_{C}x); (B4) the sentences stating that for every x ∈ E_{C}, the restriction of <_{C} to

the set {y : π_{C}y = x} is a dense linear ordering without endpoints. A routine application of a quantifier elimination test such as Theorem 3.1.4

in Marker [7] gives the following result; we leave the details to the reader.

Proposition 9.10. For each unary predicate symbol C of L(Φ), the theory T_{C} admits quantifier elimination in the language L_{C}. □

Theorem 9.11. The theory T (Ψ) admits quantifier elimination.

Proof. Let ϕ(x, y) be a quantifier-free formula; we show that ∃yϕ(x, y) is equivalent in T (Ψ) to a quantifier-free formula. First, note that ∃yϕ(x, y) is equivalent in T (Ψ) to the disjunction of the formulas

(1) ϕ(x, c) for each constant c;

(2) ∃y(Cy ∧ ϕ(x, y)) for each C ∈ Φ_{1} ∪ Φ_{tan};

(3) ∃y(Cy ∧ C𝔤y ∧ ϕ(x, y)) for each C ∈ Φ_{open} and each 𝔤 ∈ {𝔣, 𝔟}. We deal with each disjunct separately; since formulas of type (1) are trivial to handle, we deal with types (2) and (3).

Type (2): Let C ∈ Φ_{1} ∪ Φ_{tan}. Since T (Ψ) ⊧ Cy → ι(y), we may assume by Proposition 9.8 that ϕ is a minimal y-order formula. Without loss of generality, we may also assume that ϕ is a conjunction of atomic formulas, that y occurs in each of the atomic subformulas of ϕ and, by Axiom (F1), that ϕ contains only the relation symbols = and <_{C}. Let t_{1}, …, t_{k} be all maximal subterms of ϕ that do not contain y, and let ϕ′(z_{1}, …, z_{k}, y) be the formula obtained from ϕ by replacing each t_{i} by a new variable z_{i}. Then ϕ′ is a <_{C}-formula without parameters; by Proposition 9.10, there is a quantifier-free L_{C}-formula ψ′(z_{1}, …, z_{k}) such that ∃yϕ′ and ψ′ are equivalent in T_{C}. Let ψ(x) be the L(Ψ)-formula obtained from ψ′ by replacing each z_{i} by t_{i}; then ∃yϕ and ψ are equivalent in T (Ψ), as required.

Type (3): Let C ∈ Φ_{open} and 𝔤 ∈ {𝔣, 𝔟}; by Proposition 9.9, we may assume that ϕ is a 𝔤-almost minimal y-order formula. Without loss of generality, we may also assume that ϕ is a conjunction of atomic formulas, that y occurs in each of the atomic subformulas of ϕ and, by Axiom (F1), that ϕ contains only the relation symbols =, <_{C} and E_{C}. Let t_{1}, …, t_{k} be all maximal subterms of ϕ that do not contain y, and let ϕ′(z_{1}, …, z_{k}, y) be the formula obtained from ϕ by replacing each t_{i} by a new variable z_{i}. Note that ϕ′ contains no parameters. Arguing as for Type (2), it now suffices to find a quantifier-free formula ψ′(z_{1}, …, z_{k}) equivalent in T (Ψ) to ∃yϕ′(z_{1}, …, z_{k}, y).

To do so, we let π_{C} be a new unary function symbol and let T (Ψ)_{C} be the theory T (Ψ) together with the universal closure of the formula

y = π_{C}x ↔ ((Cx ∧ C𝔣x ∧ y = 𝔣x) ∨ (Cx ∧ C𝔟x ∧ y = 𝔟x) ∨ (E_{C}x ∧ y = x)) .

Since T (Ψ)_{C} is an extension by definitions of T (Ψ) in the sense of [11, Section 4.6], it suffices to find a quantifier-free L(Ψ)-formula ψ′(z_{1}, …, z_{k}) equivalent in T (Ψ)_{C} to ∃yϕ′(z_{1}, …, z_{k}, y).

Let ϕ′′ be the L_{C}-formula obtained from ϕ′ by replacing each occurrence of 𝔤y by πy; then ϕ′ and ϕ′′ are equivalent in T (Ψ)_{C}. Since T (Ψ)_{C} ⊧ T_{C}, there is by Proposition 9.10 a quantifier-free L_{C}-formula ψ′′(z_{1}, …, z_{k}) that is equivalent in T (Ψ)_{C} to ∃yϕ′′(z_{1}, …, z_{k}, y); without loss of generality, we may assume that the only subterms of ψ′′ are z_{i} and πz_{i} for i = 1, …, k.

Finally, we let ψ′ be the L(Ψ)-formula obtained from ψ′′ by replacing each atomic subformula η of ψ′′ by an L(Ψ)-formula η′ determined as follows:

(i) if η is E_{C}π_{C}z_{i}, we let η′ be Cz_{i} ∧ (E_{C}z_{i} ∨ C𝔣z_{i} ∨ C𝔟z_{i}); (ii) if η is π_{C}z_{i} ∗ z_{j} with ∗ ∈ {=, <_{C}, >_{C}}, we let η′ be

Cz_{i} ∧ Cz_{j} ∧ ( ⋁_{𝔤∈{𝔣^{0},𝔣,𝔟}} E_{C}𝔤z_{i} ∧ 𝔤z_{i} ∗ z_{j});

(iii) if η is π_{C}z_{i} <_{C} π_{C}z_{j} and ∗ ∈ {=, <_{C}}, we let η′ be

Cz_{i} ∧ Cz_{j} ∧ ( ⋁_{𝔤,𝔥∈{𝔣^{0},𝔣,𝔟}} E_{C}𝔤z_{i} ∧ E_{C}𝔥z_{j} ∧ 𝔤z_{i} ∗ 𝔥z_{j});

and if η is not of one of the forms (i)–(iii) above, we let η′ be η. This ψ′ is equivalent in T (Ψ)_{C} to ψ′′ and is of the required form. □

10. Consequences for the Model Theory of T (Ψ)

The quantifier elimination result established in the previous section allows us to show that the theory T (Ψ) is very well-behaved: it is a theory of finite rank in the sense developed by Onshuus [8].

We first rephrase the results from the previous section. For a flow configuration Φ, C ∈ Φ_{open}, M ⊧ T (Ψ) and x ∈ E_{C}^{M}, we put

C_{x}^{M} := {y ∈ C^{M} : y = x ∨ 𝔣y = x ∨ 𝔟y = x}

and \overline{C}_{x}^{M} := C_{x}^{M} ∪ \{𝔣(x), 𝔤(x)\}. The following corollary implies Theorem C:

Corollary 10.1. Let Ψ be a Dulac flow configuration and M ⊧ T (Ψ).

(1) For C ∈ Φ_{1} ∪ Φ_{tan}, every definable subset of C^{M} is a finite union of points and open <_{C}-intervals with endpoints in \overline{C}.

(2) For C ∈ Φ_{open} and x ∈ E_{C}^{M}, every definable subset of C_{x}^{M} is a finite union of points and open <_{C}-intervals with endpoints in \overline{C}_{x}^{M}.

Proof. This follows immediately from Theorem 9.11, Propositions 9.8 and 9.9 and Axioms (F2) and (F11). □

Below we use the terminology of [8].

Theorem 10.2. Let Ψ be a Dulac flow configuration and T be any completion of T (Ψ). Then T is rosy with U^{þ}(T) ≤ 2.

Proof. Let p(x) be a complete 1-type in T, M ⊧ T and a ∈ M such that M ⊧ p(a). If Cx ∈ p for some C ∈ Φ_{tan} ∪ Φ_{1}, then by Proposition 10.1(1) the type p is determined by the <_{C}-order type of x over the constants; hence U^{þ}(p) ≤ 1. If Cx ∧ ¬E_{C}x ∈ p for some C ∈ Φ_{open}, then by Proposition 10.1(2) the type p is determined by the <_{C}-order type o(x) of a over the constants and π_{C}(a), where π_{C} : C ⟶ E_{C} is given by

π_{C}(z) := \begin{cases}z & if z ∈ E_{C}^{M}, \\ 𝔣(z) & if 𝔣(z) ∈ E_{C}^{M}, \\ 𝔟(z) & if 𝔟(z) ∈ E_{C}^{M}. \end{cases}

Again by Proposition 10.1(1), the type of π_{C}(a) over the constants is determined by the <_{C}-order type of π_{C}(a) over the constants.

Since p either contains one of the above formulas or a formula x = c for some constant symbol c, it follows from the Coordinatization Theorem in [8, Theorem 2.2.2] that U^{þ}(T) ≤ 2. □

In fact, the U^{þ}-rank in the previous theorem is actually equal to 2:

Proposition 10.3. Let Φ be a flow configuration and M ⊧ T (Φ), and assume that Φ_{open} ≠ ∅. Then U^{þ}(M) ≥ 2.

Proof. Let C ∈ Φ_{open}. Replacing M by an elementary extension, we may assume that M is ℵ_{1}-saturated. Since E_{C} is a dense linear ordering without endpoints, there are infinitely many a ∈ E_{C} such that a ∉ acl(∅). For any two such a, b ∈ E_{C}, the fibers C_{a} and C_{b} are disjoint, infinite definable sets. Hence U^{þ}(M) ≥ 2. □

There is a certain converse to Theorem 10.2 based on Remark 8.8: we let Φ be a flow configuration and consider the theory T (Φ)^{+} obtained by adding the universal closures of the following formulas to T (Φ)′ for each C ∈ Φ_{trans}:

Cx → ∃y (\overline{C}y ∧ y = inf\{z : x <_{C} z ∧ Bd_{C}(z)\})

Cx → ∃y (\overline{C}y ∧ y = sup\{z : z <_{C} x ∧ Bd_{C}(z)\}) . (10.1)

Examples 10.4. (1) Let Ψ be a Dulac flow configuration. Then any model M of T (Ψ) satisfies (10.1).

(2) Let ξ be a definable vector field on ℝ^{2}, and let M_{ξ} be an L(Φ_{ξ})-structure associated to ξ as in Example 6.4. Then M_{ξ} satisfies (10.1) by Corollary 7.5, and by Remark 8.8 the structure M_{ξ} can be expanded to a model M_{ξ}^{+} of T (Φ_{ξ})^{+}.

Below, for each ν ∈ ℕ we abbreviate the formula stating that Bd_{C}(x) defines a set with at most ν elements by “| Bd_{C}(x)| ≤ ν”.

Proposition 10.5. Let Φ be a flow configuration and T be a completion of T (Φ)^{+}, and assume that U^{þ}(T) ≤ 2. Then there is a ν ∈ ℕ such that

(1) T ⊧ | Bd_{C}(x)| ≤ ν;

(2) every model M of T can be expanded to a model of T (Φ, ν).

Proof. (1) Assume that T |̸= | Bd_{C}(x)| ≤ ν for any ν ∈ ℕ. Then by model theoretic compactness, there are an M ⊧ T and a C ∈ Φ_{1} such that the set Bd_{C}(M) is infinite; we may assume that M is ℵ_{1}-saturated. Moreover by Axiom (F8), we may assume that C ∈ Φ_{trans}. Also, by Axiom (F8) and an argument as in the proof of Proposition 10.3, it suffices to find a d ∈ C^{M} such that U^{þ}(d) ≥ 2.

Since M is ℵ_{1}-saturated, there is an interval I ⊆ C^{M} such that I∩acl(∅) = ∅ and I∩Bd_{C}(M) is infinite. By (10.1) and since Bd_{C}(M) is nowhere dense, there is a c ∈ I\Bd_{C}(M) such that the elements a := sup {x ∈ I : x <_{C} c ∧ Bd_{C}(x)} and b := inf {x ∈ C : a <_{C} x ∧ Bd_{C}(x)} exist in I. Then a <_{C} b, a, b ∉ acl(∅), b ∈ dcl(a) and

M ⊧ a <_{C} b ∧ Bd_{C}(a) ∧ ¬∃x(Cx ∧ a <_{C} x <_{C} b ∧ Bd_{C}(x)).

It follows that the formula ϕ(x) := a <_{C} x <_{C} b strongly divides over ∅; hence U^{þ}(d) ≥ 2 for some d ∈ C^{M}, as required.

Part (2) follows from Proposition 8.7 and part (1). □

We can now prove our restatement of Dulac’s Problem:

Proof of Theorem B. (1) If ξ has finitely many boundary cycles, then by Proposition 8.7 the structure M_{ξ} can be expanded into a model M_{ξ}^{D} of T (Φ_{ξ}, ν) for some ν ∈ ℕ. Since (Φ_{ξ})_{open} ≠ ∅, it follows that 2 ≤ U^{þ}(M_{ξ}) ≤ U^{þ}(M_{ξ}^{D}) ≤ 2 by Proposition 10.3 and Theorem 10.2. Conversely, if U^{þ}(M_{ξ}) = 2 then by Proposition 10.5, the structure M_{ξ} can be expanded into a model of T (Φ_{ξ}, ν) for some ν ∈ ℕ, so by Example 6.7 the vector field ξ has finitely many boundary cycles.

Part (2) follows from part (1) and Poincaré’s Theorem [10] (see also [9, p. 217]). The “moreover” clause follows from part(1) and Theorem 10.2. □

11. Final questions and remarks

(1) In the situation of Theorem B, is it possible for M_{ξ} to be rosy of U^{þ}-rank strictly greater than 2?

(2) Can a restatement of Hilbert’s 16th Problem be obtained in the spirit

of Theorem B?

A naïve approach to this question is as follows: Let {ξ_{a} : a ∈ A} be a family of vector fields on ℝ^{2} definable in R. Since the arguments in Sections 1 through 5 are uniform in parameters, we may assume that there is a flow configuration Φ such that Φ_{ξ_{a}} = Φ for all a ∈ A. In this situation, one can readily reformulate the theory T (Φ) for the parametric situation; and if one also assumes the existence of a uniform bound ν ∈ ℕ on the number of boundary cycles of each ξ_{a}, such a reformulation extends to T (Φ, ν). We suspect that under the latter assumption, the corresponding theory is rosy of U^{þ}-rank 3; however, this does not appear to us to be a completely trivial generalization of the results in Section 10, and we plan to pursue it in a future project.

(3) The structure M_{ξ}^{D} in Example 8.5 does not define any algebraic operations (by Theorem 9.11). Assume here that S(ξ) = ∅; is it possible to expand M_{ξ}^{D} by some (or all) of the sets definable in the original o-minimal structure R without increasing the U^{þ}-rank? We know very little about this question. However, if (a) the x-axis, the projection from ℝ^{2} onto the x-axis, and both addition and multiplication are definable in an expansion M′ of M_{ξ}^{D}, and if (b) the expansion M′ still has U^{þ}-rank two, then M′ (and hence M_{ξ}^{D}) would be definable in an o-minimal structure. (The assumption that M′ has U^{þ}-rank two is necessary here.) Thus, question (3) is related to the following question:

(4) Is the structure M_{ξ}^{D} of Example 8.5 definable in some o-minimal expansion of the real field?

(5) Consider a Dulac flow configuration Ψ and M ⊧ T (Ψ). Corollary 10.1, Theorem 10.2 and their respective proofs may be loosely interpreted as indicating that M is built-up from sets D ⊆ M on which the induced structure is o-minimal. Is there a theory of structures built-up from sets with induced o-minimal structure, say in the spirit of Zilber’s results on the fine structure of uncountably categorical theories [14]?

References

[1] C. Camacho and A. Lins Neto, Geometric Theory of Foliations, Birkhäuser, Boston, 1985.

[2] F. Chazal, Structure locale et globale des feuilletages de Rolle, un théorème de fibration, Ann. Inst. Fourier (Grenoble), 48 (1998), pp. 553–592.

[3] J. Ecalle, Introduction aux fonctions analysables et preuve constructive de la conjecture de Dulac, Hermann, Paris, 1992.

[4] M. W. Hirsch, Differential Topology, Springer Verlag, 1976.

[5] Yu. S. Ilyashenko, Finiteness theorems for limit cycles, vol. 94 of Translations of Mathematical Monographs, American Mathematical Society, 1991.

[6] A. Khovanskii, Fewnomials, vol. 88 of Translations of Mathematical Monographs, American Mathematical Society, 1991.

[7] D. Marker, Model Theory: An Introduction, Springer-Verlag, 2002.

[8] A. Onshuus, þ-forking, algebraic independence and examples of rosy theories. preprint.

[9] L. Perko, Differential Equations and Dynamical Systems, Springer-Verlag, New York, 2001.

[10] H. Poincaré, Mémoire sur les courbes définies par une equation différentielle, J. Mathématiques, 7 (1881), pp. 375–422.

[11] J. Shoenfield, Mathematical Logic, A. K. Peters Ltd., 2001.

[12] P. Speissegger, The Pfaffian closure of an o-minimal structure, J. Reine Angew. Math., 508 (1999), pp. 189–211.

[13] A. Wilkie, Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function, J. Amer. Math. Soc., 9 (1996), pp. 1051–1094.

[14] B. Zilber, Uncountably categorical theories, vol. 117 of Translations of mathematical monographs, American Mathematical Society, 1993.

Department of Mathematics & Statistics, McMaster University, 1280 Main Street West, Hamilton, Ontario L8S 4K1, Canada

E-mail address: dolicha@math.mcmaster.ca
E-mail address: speisseg@math.mcmaster.ca