Proof We describe an algorithm for computing $\varphi _{T, \mathcal {A}}(\ell , \mathcal {S}, N)$ and $\mathcal {N}_{T, \mathcal {A}}(\ell , \mathcal {S}, N)$ . Fix some $\mathcal {L}, T, \mathcal {A}, \ell $ , and $\mathcal {S}$ .

We will describe an algorithm that, for a given positive integer s, computes first-order formulas $\psi _s$ and $q_s$ in $\mathcal {L}$ in the variables $\mathbf {x} = (x_1, \ldots , x_\ell )$ and a positive integer $\mathcal {N}_s$ such that, for every model M of T and every $\mathbf {a} \in T^\ell $ ,

• • $\psi _s(\mathbf {a})$ is true in M iff algorithm $\mathcal {A}$ with input $\mathcal {S}$ and oracle $\mathcal {O}_M(\mathbf {a})$ will perform at least s queries;

• • if $\psi _s(\mathbf {a})$ is true in M, then the result of the sth query will be $q_s(\mathbf {a})$ ; and

• • if algorithm $\mathcal {A}$ with input $\mathcal {S}$ and oracle $\mathcal {O}_M(\mathbf {a})$ performs at most s queries, then the number of steps performed does not exceed $\mathcal {N}_s$ .

Fix some $s \geqslant 1$ and assume that the algorithm have computed $\psi _1, \ldots , \psi _{s - 1}$ , $q_1, \ldots , q_{s - 1}$ , and $\mathcal {N}_{0}, \ldots , \mathcal {N}_{s - 2}$ . Assume that $\mathcal {A}$ with input $\mathcal {S}$ has performed $s - 1$ queries. Then, whether or not an sth query will be performed is determined by the results of the first $s - 1$ queries. Fix some $\mathbf {r} \in \{\mathrm {True}, \mathrm {False}\}^{s - 1}$ . It will represent possible results of the first $s - 1$ queries. Consider the following formula in $\mathcal {L}$ :

$$ \begin{align*} \psi_{\mathbf{r}}(\mathbf{x}) := \psi_{s - 1}(\mathbf{x}) \wedge \bigwedge\limits_{i = 1}^{s - 1} \left( q_i(\mathbf{x}) \iff r_i \right), \end{align*} $$

where we assume $\psi _0 = \mathrm {True}$ . The algorithm uses the algorithm for checking correctness of sentences in T to check whether the sentence $\exists \mathbf {x}\; \psi _{\mathbf {r}}(\mathbf {x})$ is false in T. If it is, then there is no oracle of the form $\mathcal {O}_M(\mathbf {a})$ such that $\mathcal {A}$ will perform at least $s - 1$ queries on it with the results being $r_1, \ldots , r_{s - 1}$ .

In the case of $\exists \mathbf {x}\; \psi _{\mathbf {r}}(\mathbf {x})$ is true in T, the algorithm will run $\mathcal {A}$ with input $\mathcal {S}$ and an oracle $\mathcal {O}_{\mathbf {r}}$ that works as follows. For the first $s - 1$ queries, $\mathcal {O}_{\mathbf {r}}$ will return $r_1, \ldots , r_{s - 1}$ . For all subsequent queries, it always returns True. The algorithm will stop the execution of $\mathcal {A}$ if $\mathcal {A}$ makes an sth query to the oracle, and denote the formula in the query by $q_{\mathbf {r}}$ .

Because $\exists \mathbf {x}\;\psi _{\mathbf {r}}(\mathbf {x})$ is true in T, $\mathcal {O}_{\mathbf {r}}$ gives the same responses to the first $s - 1$ queries as some oracle of the form $\mathcal {O}_M(\mathbf {a})$ . Because $\mathcal {A}$ must terminate in finite time for every such oracle, one of the following must happen:

1. (1) $\mathcal {A}$ will perform an sth query.

2. (2) $\mathcal {A}$ will terminate after performing only $s - 1$ queries.

In the former case, as described above, the algorithm will define a formula $q_{\mathbf {r}}$ to be the sth query. In the latter case, the algorithm will define $\mathcal {N}_{\mathbf {r}}$ to be the number of steps performed by $\mathcal {A}$ . Then, the algorithm computes

$$ \begin{gather*} \psi_s(\mathbf{x}) := \bigvee\limits_{q_{\mathbf{r}} \text{ is defined}} \psi_{\mathbf{r}}(\mathbf{x}),\quad q_s(\mathbf{x}) := \bigwedge\limits_{q_{\mathbf{r}}\text{ is defined}} (\psi_{\mathbf{r}}(\mathbf{x}) \implies q_{\mathbf{r}}(\mathbf{x})),\\ \mathcal{N}_{s - 1} := \max\left(\mathcal{N}_{s - 2}, \sum\limits_{\mathcal{N}_{\mathbf{r}} \text{ is defined}} \mathcal{N}_{\mathbf{r}}\right), \end{gather*} $$

where we assume $\mathcal {N}_{-1} = -\infty $ . If the set $\{\mathbf {r}\mid q_{\mathbf {r}} \text { is defined}\}$ is empty, the algorithm sets $\psi _s(\mathbf {x}) = \operatorname {False}$ and $q_s(\mathbf {x}) = \operatorname {True}$ . Finally, the algorithm returns $\varphi _{T, \mathcal {A}}(\ell , \mathcal {S}, N) := \lnot \psi _{N + 1}$ and $\mathcal {N}_{T, \mathcal {A}}(\ell , \mathcal {S}, N) := \mathcal {N}_N$ .▪

Proof Assume the contrary, that is, that $U_i \neq \varnothing $ for every $i \geqslant 1$ . We will show that $\bigcap \limits _{i = 1}^\infty U_i \neq \varnothing $ .

We show that a collection of formulas $\{x \in U_i\}_{i = 1}^\infty $ is finitely satisfiable. Indeed, let $S \subset \mathbb {Z}_{> 0}$ be a finite set and $N = \max S$ . Then, $\bigcap _{i \in S} U_i = U_N \neq \varnothing $ . Due to compactness, the countable collection $\{x \in U_i\}_{i = 1}^\infty $ is satisfiable in some elementary extension of M. Because M is $\aleph _0$ -saturated, this collection is satisfiable in M. Therefore, $\bigcap \limits _{i = 1}^\infty U_i \neq \varnothing $ .▪

Proof We will describe an algorithm for computing $\operatorname {\mathrm {Steps}}_{T, \mathcal {A}}(\ell , r)$ . We fix T, $\mathcal {A}$ , $\ell $ , and r. We will consider $\mathcal {S}$ of length at most r and describe how to compute a bound for the number of steps given that the input is $\mathcal {S}$ . Taking the maximum over all $\mathcal {S}$ of length at most r (there are finitely many of them), we obtain $\operatorname {\mathrm {Steps}}_{\mathcal {A}, T}(\ell , r)$ .

The algorithm will compute $\varphi _i := \varphi _{T, \mathcal {A}}(\ell , \mathcal {S}, i)$ for $i = 1, 2, \ldots $ using the algorithm from Lemma 4.3. For each $\varphi _i$ , the algorithm will check whether the formula is equivalent to $\mathrm {True}$ in T using the decidability of T.

If this is true, the algorithm stops and returns $\mathcal {N}_{T, \mathcal {A}}(\ell , \mathcal {S}, i)$ (see Lemma 4.3). It remains to show that the described procedure terminates in finitely many steps. Let M be an $\aleph _0$ -saturated model of T (it exists, for example, due to [Reference Marker19, Theorem 4.3.12]). For every $i = 1, 2, \ldots $ , we introduce a definable set

$$ \begin{align*} U_i := \{\mathbf{a} \in M^\ell \mid \varphi_i(\mathbf{a}) = \mathrm{False}\}. \end{align*} $$

Notice that $U_i = \varnothing $ if and only if $(\varphi _i \iff \mathrm {True})$ in T. Then, the definition of $\varphi _i$ ’s implies that $U_1 \supset U_2 \supset \cdots $ . Assume that $\bigcap _{i = 1}^\infty U_i$ is not empty and choose an element $\mathbf {a}$ in it. Then, $\mathcal {A}$ will not terminate in finitely many steps with input $\mathcal {S}$ and oracle $\mathcal {O}_M(\mathbf {a})$ . Thus, $\bigcap _{i = 1}^\infty U_i = \varnothing $ . Lemma 4.4 implies that there exists N such that $U_N = \varnothing $ . Then, our algorithm will terminate after checking whether $\varphi _N$ is equivalent to True.▪

Notation 5.1 Let m be a positive integer.

• • The language of partial differential rings with m commuting derivation is denoted by $ \mathcal {L}_{m} := \{+, -, \cdot , 0, 1, \partial _1, \ldots , \partial _m\}$ . We add a separate functional symbol for subtraction for convenience.

• • The theory of partial differentially closed fields with m commuting derivations of characteristic zero is denoted by $\operatorname {DCF}_{m}$ . Recall that $\operatorname {DCF}_m$ is complete [Reference McGrail21, Corollary 3.1.9] and, with this, is decidable by [Reference Marker19, Lemma 2.2.8] and [Reference McGrail21, Lemma 3.1.2, p. 890].

Notation 5.2 Let $m, n$ , and h be positive integers and k a differential field with a set of m commuting derivations $\Delta =\{\partial _1, \ldots , \partial _m\}$ .

• • $\operatorname {\mathrm {Pol}}_k(m, n, h)$ denotes the space of all differential polynomials over k in n variables of order at most h and degree at most h.

• • The dimension of $\operatorname {\mathrm {Pol}}_k(m, n, h)$ (which does not depend on k) will be denoted by $\operatorname {\mathrm {PolDim}}(m, n, h)$ .

Notation 5.3 Let m, $\ell $ , and n be positive integers.

• • Let $\mathcal {L}_m(x_1, \ldots , x_\ell )\{y_1, \ldots , y_n\}_\Delta $ denote the ring of differential polynomials in differential variables $y_1, \ldots , y_n$ with respect to m derivations with the coefficients being terms in the language $\mathcal {L}_m$ in $x_1, \ldots , x_\ell $ (that is, elements of $\mathbb {Z}\{x_1, \ldots , x_\ell \}_\Delta )$ .

  This is a computable differential ring with m commuting derivations. In what follows, we will assume that the algorithms use dense representation to store these polynomials (that is, store all the coefficients up to certain order and certain degree).

• • Let k be a differential field with m derivations and $\mathbf {a} \in k^\ell $ . Then, for $T \in \mathcal {L}_m(x_1, \ldots , x_\ell )\{y_1, \ldots , y_n\}_\Delta $ , we define $T(\mathbf {a}) \in k\{y_1, \ldots , y_n\}_\Delta $ to be the result of evaluating the coefficients of T at $\mathbf {a}$ .

Notation 5.5 For a $\Delta $ -field k and $f \in k\{z_1,\ldots ,z_n\}_\Delta \backslash k$ and differential ranking $>$ ,

• • $\operatorname {\mathrm {lead}}(f)$ is the element of Z of the highest rank appearing in f.

• • The leading coefficient of f considered as a polynomial in $\operatorname {\mathrm {lead}}(f)$ is denoted by $\operatorname {\mathrm {in}}(f)$ and called the initial of f.

• • The separant of f is $\frac {\partial f}{\partial \operatorname {\mathrm {lead}}(f)}$ .

• • The rank of f is $\operatorname {\mathrm {rank}}(f) = \operatorname {\mathrm {lead}}(f)^{\deg _{\operatorname {\mathrm {lead}}(f)}f}$ . The ranks are compared first with respect to $\operatorname {\mathrm {lead}}$ , and in the case of equality with respect to $\deg $ .

• • For $S \subset k\{z_1,\ldots ,z_n\}_\Delta \backslash k$ , the set of initials and separants of S is denoted by $H_S$ .

Proof In order to prove the completeness and decidability, we will prove that there is an algorithm for quantifier elimination in $\operatorname {\mathrm {DCF}}_m\oplus \operatorname {\mathrm {RCF}}$ based on the existence of such algorithms for $\operatorname {\mathrm {DCF}}_m$ (follows from decidability; see Notation 5.1 and quantifier elimination [Reference McGrail21, Theorem 3.1.7]) and $\operatorname {\mathrm {RCF}}$ . It is sufficient to perform quantifier elimination for a formula of the form

$$ \begin{align*} \exists x \in S\colon L_1\wedge \cdots \wedge L_N, \end{align*} $$

where S is one of the sorts (corresponding to $\operatorname {\mathrm {DCF}}_m$ or $\operatorname {\mathrm {RCF}}$ ) and $L_1, \ldots , L_N$ are literals. (See [Reference Marker19, Lemma 3.1.5].) By reordering $L_1, \ldots , L_N$ if necessary, we will further assume that there exists $N_0$ such that $L_1, \ldots , L_{N_0}$ are in the signature of the sort S and $L_{N_0 + 1}, \ldots , L_N$ are in the signature of the other sort. Then,

$$ \begin{align*} \left(\exists x \in S\colon L_1\wedge \cdots\wedge L_N\right) \iff \left(\exists x \in S \colon L_1\wedge \cdots \wedge L_{N_0}\right) \wedge \left( L_{N_0 + 1}\wedge \cdots \wedge L_{N}\right), \end{align*} $$

and, for $\exists x \in S \colon L_1\wedge \cdots \wedge L_{N_0}$ , the algorithm for the corresponding sort S can compute an equivalent quantifier-free formula.

The resulting theory is decidable, because the correctness of each sentence can be checked by performing quantifier elimination after which the formula will become just true/false.▪

Proof [Reference Boulier, Lazard, Ollivier and Petitot3, Theorem 9] states that the only operations performed by the Rosenfeld–Gröbner algorithm with the elements of the ground differential field are arithmetic operations, differentiation, and zero testing. Algorithm $\mathcal {RG}_{m}$ is constructed to work exactly in the same way as the Rosenfeld–Gröbner algorithm with the only difference that the elements of the ground differential field will be represented as $L(\mathbf {a})$ , where $L \in \mathcal {L}_m(x_1, \ldots , x_\ell )\{y_1, \ldots , y_n\}_\Delta $ . The arithmetic operations and differentiations can be performed with L, zero testing can be performed using the k-component of the oracle, and the queries to the ranking can be performed using the $\mathbb {R}$ -component of the oracle, so $\mathcal {RG}$ will be able to perform the same computations as the Rosenfeld–Gröbner algorithm.

Due to [Reference Boulier, Lazard, Ollivier and Petitot3, Theorem 5], the Rosenfeld–Gröbner algorithm is guaranteed to terminate on every input. Hence, the same is true for $\mathcal {RG}_{m}$ .▪

Proof We fix integers m, n, and $\ell $ and compute the total algorithm $\mathcal {RG}_{m}$ over $\operatorname {\mathrm {DCF}}_{m} \oplus \operatorname {\mathrm {RCF}}$ from Proposition 5.9. Let $\mathbf {a}$ be the set of all the coefficients of A and S. Then, $|\mathbf {a}| \leqslant N := 2\ell \operatorname {\mathrm {PolDim}}(m, n, n)$ . The sets A and S can be presented as evaluations of subsets $\widetilde {A}, \widetilde {S} \subset \mathcal {L}_m(x_1, \ldots , x_N)\{y_1, \ldots , y_n\}_\Delta $ at $\mathbf {a}$ such that the orders and degrees of $\widetilde {A}, \widetilde {S}$ in $y_1, \ldots , y_n$ do not exceed n and every coefficient is a single variable $x_i$ . Let the ranking be defined as $\operatorname {\mathrm {RK}}(\mathbf {b}, \mathcal {S})$ (see Remark 5.6), where $\mathbf {b}$ is a tuple of $m(m + 1)n$ real numbers and $\mathcal {S}$ is a binary string of length at most $(n^2 + n) \log _2 \max (n, m)$ . Then, the tuple $(\widetilde {A}, \widetilde {S}, \mathcal {S})$ can be encoded as a binary string of the length bounded by a computable function $S(m, n, N)$ .

We run $\mathcal {RG}_{m}$ with the input $\mathcal {I} = (\widetilde {A}, \widetilde {S}, \mathcal {S})$ and oracle $\mathcal {O}(\mathbf {a}, \mathbf {b})$ . Theorem 4.5 implies that the number of steps and, consequently, the bit size of all the intermediate results (see Remark 4.6) will not exceed $\operatorname {\mathrm {Steps}}_{\mathcal {RG}_{m}, \operatorname {\mathrm {DCF}}_m \oplus \operatorname {\mathrm {RCF}}}(N, S(m, n, N))$ .

Because each component takes at least one bit, a polynomial of degree d or order d has at least d coefficients (due to the dense representation of the polynomials; see Notation 5.2) requiring at least one bit each, the number of components, the degrees, and orders do not exceed the bit size of the intermediate results. Therefore, we can set $\operatorname {RG}(m, n, \ell ) = \operatorname {\mathrm {Steps}}_{\mathcal {RG}_{m}, \operatorname {\mathrm {DCF}}_{m} \oplus \operatorname {\mathrm {RCF}}}(N, S(m, n, N))$ .▪

Proof Theorem 5.10 implies that there exists a representation

$$ \begin{align*} \sqrt{\langle A\rangle^{(\infty)} \colon S^\infty} = (\langle C_1\rangle^{(\infty)} \colon H_{C_1}) \cap\cdots\cap (\langle C_N\rangle^{(\infty)} \colon H_{C_N}), \end{align*} $$

where $H_{C_i}$ is the product of the initials and separants of $C_i$ , and $C_i$ is the characteristic presentation [Reference Boulier, Lazard, Ollivier and Petitot3, Definition 8] of $\langle C_i\rangle ^{(\infty )} \colon H_{C_i}^\infty $ for every $1 \leqslant i \leqslant N$ . As noted in [Reference Boulier, Lazard, Ollivier and Petitot3, p. 108] a characteristic set of $\langle C_i\rangle ^{(\infty )} \colon H_{C_i}^\infty $ can be obtained from $C_i$ by performing reductions until it will become autoreduced. Because differential reduction is a part of the Rosenfeld–Gröbner algorithm, it can also be performed by a total algorithm over $\operatorname {\mathrm {DCF}}_m \oplus \operatorname {\mathrm {RCF}}$ . Therefore, as in the proof of Theorem 5.10, Lemma 4.5 implies that $\langle C_i\rangle ^{(\infty )} \colon H_{C_i}^\infty $ has a characteristic set with degrees and order bounded by a computable function of the degrees and orders of $C_i$ . The latter are bounded by a computable function $\operatorname {RG}$ due to Theorem 5.10. Composing these two bounds, we obtain a desired function $\operatorname {CharSet}(m, n, \ell )$ .▪

Proof Let H be the product of the initials and separants of C. Theorem 4 of [Reference Boulier, Lazard, Ollivier and Petitot3] implies that the number of prime components of $\langle C\rangle ^{(\infty )} \colon H^\infty $ is equal to the number of prime components of the algebraic ideal $(\langle C\rangle ^{(\infty )} \colon H^\infty ) \cap R_n$ , where $R_n$ is the ring of differential polynomials of order at most n. Because the degrees of elements of C are bounded by n, the Bézout inequality implies that there is a computable bound D for the degree of the radical ideal $I \cap R_n$ (defined, e.g., as the degree of the corresponding affine variety [Reference Heintz12, p. 246]) in terms of m and n, so this gives a bound for the number of components.

Let $P_1, \ldots , P_\ell $ be the prime components of I. For every $1 \leqslant i \leqslant \ell $ , $P_i \cap R_n$ is a prime algebraic ideal, and its zero set can be defined by equations of degree at most $\deg (P_i\cap R_n)$ due to [Reference Heintz12, Proposition 3]. Therefore, for each $2 \leqslant i \leqslant \ell $ , we can choose a polynomial in $(P_1 \setminus P_i) \cap R_n$ of degree at most $\deg (P_i \cap R_n)$ . Their product Q has degree at most $\deg (I\cap R_n) \leqslant D$ . Observe that

$$ \begin{align*} P_1 = P_1 \colon Q^\infty \subset I \colon Q^\infty = (P_1 \colon Q^\infty) \cap \cdots \cap (P_\ell \colon Q^\infty) = P_1. \end{align*} $$

Thus, applying Corollary 5.11 to a pair $(C, HQ)$ and using that $|C| \leqslant \operatorname {\mathrm {PolDim}}(m, n)$ , we show that $P_1$ has a characteristic set with orders and degrees bounded by $\operatorname {CharSet}(m, D + n, \operatorname {\mathrm {PolDim}}(m, n))$ .▪

Proof Consider any differential ranking. By replacing F with the basis of its linear span, we will further assume that $|F| \leqslant \operatorname {\mathrm {PolDim}}(m, n, h)$ (see Notation 5.2). Corollary 5.11 implies that $\sqrt {\langle F \rangle ^{(\infty )}}$ can be represented as an intersection of at most N characterizable ideals with characteristic sets $C_1, \ldots , C_N$ of order and degree at most N, where

$$ \begin{align*} N := \operatorname{CharSet}(m, \max\{n,h\}, \operatorname{\mathrm{PolDim}}(m, n, h)). \end{align*} $$

Lemma 5.12 applied to each of $C_1, \ldots , C_N$ implies that the number of components of the variety defined by $F = 0$ does not exceed $N\cdot \operatorname {PrimeComp}(m, N)$ , and each of them has a characteristic set with orders and degrees not exceeding $\operatorname {PrimeComp}(m, N)$ .▪

Notation 6.3 For a numeric polynomial $\omega (t) = \sum \limits _{i = 0}^{m} a_i \binom {t + i}{i}$ , we set

$$ \begin{align*} |\omega| := \sum\limits_{i = 0}^{m} |a_i|. \end{align*} $$

Proof By performing a linear change of variables, we reduce the problem to the case in which $\pi $ is the projection to the first $\ell $ coordinates. Consider a ranking such that:

• • $y_{\ell + i}$ is greater than every derivative of $y_{j}$ for every $i> 0$ and $1 \leqslant j \leqslant \ell $ ; and

• • the restriction of the ranking on $y_1, \ldots , y_\ell $ is an orderly ranking (that is, a ranking such that $\operatorname {\mathrm {ord}}\theta _1> \operatorname {\mathrm {ord}}\theta _2 $ implies, for all i and j, $\theta _1 y_i> \theta _2 y_j$ ).

Theorem 5.13 implies that $X_0$ has a characteristic set $\mathcal {C}$ with respect to this ranking with the order bounded by a computable function of N. Because a characteristic set of Y can be obtained from $\mathcal {C}$ by selecting the polynomials only in the first $\ell $ variables, there is a characteristic set of Y with respect to the orderly ranking with the order bounded by a computable function of N. Then, [Reference León Sánchez15, Proposition 3.1] and [Reference León Sánchez15, Fact 2.1] imply that $|\omega _Y|$ is bounded by a computable function of N.▪

Proof By replacing $g(n)$ with $n + \max \limits _{0 \leqslant s \leqslant n} g(s)$ , we can further assume that $g(n)$ is increasing and $g(n) \geqslant n$ . Definition 2.4.9 and Lemma 2.4.12 of [Reference Mikhalev, Levin, Pankratiev and Kondratieva22] define a computable order-preserving map c from the set of all Kolchin polynomials $\mathcal {K}$ to $\mathbb {Z}_{\geqslant 0}^{m + 1}$ (considered with respect to the lexicographic ordering). For $v = (v_0, \ldots , v_m) \in \mathbb {Z}_{\geqslant 0}^{m + 1}$ , we define $|v| = v_0 + \cdots + v_m$ . For every function $g\colon \mathbb {Z}_{\geqslant 0} \to \mathbb {Z}_{\geqslant 0}$ , we define

$$ \begin{align*} \widetilde{g}(n) := \max\limits_{\omega \in \mathcal{K},\; |\omega| \leqslant g(n)} |c(\omega)|. \end{align*} $$

Note that if $g(n)$ was computable, then $\widetilde {g}(n)$ is also computable.

The sequence $\omega _0> \omega _1 > \cdots $ gives rise to a sequence $c(\omega _0)>_{\operatorname {lex}} c(\omega _1) >_{\operatorname {lex}} \cdots $ in $\mathbb {Z}_{\geqslant 0}^{m + 1}$ with $|c(\omega _i)| \leqslant \widetilde {g}(i)$ for every i. Main Lemma of [Reference McAloon20] implies that there is an algorithm to compute the maximal length of such a sequence, so there is an algorithm to compute a bound on $\ell $ from g.▪

Proof The proof follows [Reference Li, Ovchinnikov, Pogudin and Scanlon18, Lemma 6.1] mutatis mutandis as follows. We will show that there exists a $\Delta $ - $\sigma ^\ast $ -field $K_0$ containing k. The proof of [Reference Levin17, Proposition 2.1.7] implies that one can build an ascending chain of $\sigma $ -fields

(6.2) $$ \begin{align} k_0 \subset k_1 \subset k_2 \subset \cdots \end{align} $$

such that, for every $i \in \mathbb {N}$ , there exists an isomorphism $\varphi _i\colon k \to k_i$ of $\sigma $ -fields, $\sigma (k_{i + 1}) = k_i$ , and $\varphi _i = \sigma \circ \varphi _{i + 1}$ , for every $i \in \mathbb {N}$ . We transfer the $\Delta $ - $\sigma $ -structure from k to $k_i$ ’s via $\varphi _i$ ’s. Then, $\varphi _i = \sigma \circ \varphi _{i + 1}$ implies that the restriction of $\Delta $ on $k_{i + 1}$ to $k_i$ coincides with the action of $\Delta $ on $k_i$ . We set $K_0 := \bigcup \limits _{i \in \mathbb {N}} k_i$ . Because the action of $\Delta $ and $\sigma $ is consistent with the ascending chain (6.2), $K_0$ is a $\Delta $ - $\sigma $ -extension of $k_0 \cong k$ . It is shown in [Reference Levin17, Proposition 2.1.7] that the action of $\sigma $ on $K_0$ is surjective. Corollary 2.4 of [Reference Léon Sánchez14] implies that $K_0$ can be embedded in a differentially closed $\Delta $ - $\sigma ^\ast $ -field K.▪

Notation 6.9 Within Sections 6.2 and 6.3, we fix a ground $\Delta $ - $\sigma $ field k and a differentially closed $\Delta $ - $\sigma ^\ast $ -field K given by Lemma 6.8 applied to k. All varieties in Sections 6.2 and 6.3 are considered over K.

Proof As in [Reference Li, Ovchinnikov, Pogudin and Scanlon18, Lemma 6.5].▪

Proof We prove it as in [Reference Li, Ovchinnikov, Pogudin and Scanlon18, Lemma 6.7], as follows. To prove the existence of a partial solution of $(X,\pi _1,\pi _2)$ with the desired property, it suffices to prove the following claim.

We will prove the claim by induction on $\ell $ . For $\ell =1$ , take $U=Y_1$ . Because each point in $Y_1$ is a partial solution of $(X,\pi _1,\pi _2)$ of length 1, the claim holds for $\ell =1$ . Now, suppose we have proved the claim for $\ell -1$ . So, there exists a nonempty open subset $U_0\subseteq Y_{\ell -1}$ satisfying the desired property. Because $Y_{\ell -1}$ is irreducible, $U_0$ is dense in $Y_{\ell -1}.$ So, $\pi _2(U_0)$ is dense in $\overline {\pi _2(Y_{\ell -1})}^{\operatorname {\mathrm {Kol}}}=\overline {\pi _1(Y_{\ell })}^{\operatorname {\mathrm {Kol}}}$ . Because $U_0$ is $\Delta $ -constructible (that is, solution set of a quantifier-free formula with parameters in K or, equivalently, a finite union of $\Delta $ -closed and $\Delta $ -open sets), $\pi _2(U_0)$ is $\Delta $ -constructible too. So, $\pi _2(U_0)$ contains a nonempty open subset of $\overline {\pi _1(Y_{\ell })}^{\operatorname {\mathrm {Kol}}}$ .

Because $\pi _1(Y_{\ell })$ is $\Delta $ -constructible and dense in $\overline {\pi _1(Y_{\ell })}^{\operatorname {\mathrm {Kol}}}$ , $\pi _2(U_0)\cap \pi _1(Y_{\ell })\neq \varnothing $ is $\Delta $ -constructible and dense in $\overline {\pi _1(Y_{\ell })}^{\operatorname {\mathrm {Kol}}}$ . Let $U_1$ be a nonempty open subset of $\overline {\pi _1(Y_{\ell })}^{\operatorname {\mathrm {Kol}}}$ contained in $\pi _2(U_0)\cap \pi _1(Y_{\ell })$ and

$$ \begin{align*}U_2=\pi_1^{-1}(U_1)\cap Y_{\ell}.\end{align*} $$

Then, $U_2$ is a nonempty open subset of $Y_{\ell }$ . We will show that, for each $p_\ell \in U_2$ , there exists $p_{i}\in Y_i$ , for $i=1,\ldots ,\ell -1$ , such that $p_1,\ldots ,p_{\ell }$ is a partial solution of $(X,\pi _1,\pi _2).$

Because $\pi _1(p_\ell )\in U_1\subset \pi _2(U_0)$ , there exists $p_{\ell -1}\in U_0$ such that $\pi _1(p_\ell )=\pi _2(p_{\ell -1}).$ Because $p_{\ell -1}\in U_0$ , by the inductive hypothesis, there exists $p_{i}\in Y_i$ , for $i=1,\ldots ,\ell -1$ , such that $p_1,\ldots ,p_{\ell -1}$ is a partial solution of $(X,\pi _1,\pi _2)$ of length $\ell -1$ . So, $p_1,\ldots ,p_{\ell }$ is a partial solution of $(X,\pi _1,\pi _2)$ of length $\ell $ .▪

Proof The proof follows [Reference Li, Ovchinnikov, Pogudin and Scanlon18, Lemma 6.8]. The first assertion is straightforward. We will prove the second assertion by induction on $\ell $ . For $\ell = 1$ , $\mathbf {W}_1= X$ , and we can set $W = Y_1$ .

Let $\ell> 1$ . Apply the inductive hypothesis to the train $(Y_1, \ldots , Y_{\ell - 1})$ and obtain an irreducible subvariety $Y' \subset \mathbf {W}_{\ell -1} \subset \mathbf {X}_{\ell - 1}$ . Then, there is a natural embedding of $Y' \times Y_\ell $ into $\mathbf {X}_\ell $ . Denote $(Y' \times Y_\ell ) \cap \mathbf {W}_\ell $ by $\widetilde Y$ . Because $Y'\subset \mathbf {W}_{\ell -1}$ ,

$$ \begin{align*} \widetilde Y = \{ p \in Y' \times Y_\ell \:|\: \pi_2\left( \varphi_{\ell, \ell - 1}(p) \right) = \pi_1\left( \varphi_{\ell, \ell}(p) \right) \}. \end{align*} $$

Let

(6.3) $$ \begin{align} Z := \overline{\pi_2\left( \varphi_{\ell - 1, \ell - 1}(Y') \right)} = \overline{\pi_1(Y_\ell)}. \end{align} $$

Then, we have a $(k, \Delta )$ -isomorphism

$$ \begin{align*} R_{Y'}\otimes_{R_Z}R_{Y_\ell} \to R_{\widetilde{Y}} \end{align*} $$

under the $(k,\Delta )$ -algebra homomorphisms $i_1:R_Z \to R_{Y'}$ and $i_2:R_Z \to R_{Y_\ell }$ induced by $\pi _2\circ \varphi _{\ell - 1, \ell - 1} $ and $\pi _1$ , respectively. Equality (6.3) implies that $i_1$ and $i_2$ are injective. Denote the fields of fractions of $R_{Y'}$ , $R_{Y_\ell }$ , and $R_Z$ by E, F, and L, respectively. Let $\mathfrak {p}$ be any prime differential ideal in $E \otimes _L F$ ,

$$ \begin{align*}R := (E \otimes_L F) / \mathfrak{p},\end{align*} $$

and $\pi \colon E \otimes _L F \to R$ be the canonical homomorphism. Consider the natural homomorphism $i \colon R_{Y'}\otimes _{R_Z}R_{Y_\ell } \to E \otimes _L F$ . Because $1 \in i(R_{Y'}\otimes _{R_Z}R_{Y_\ell })$ , the composition $\pi \circ i$ is a nonzero homomorphism. Because $i_1$ and $i_2$ are injective, the natural homomorphisms $i_{Y'} \colon R_{Y'} \to R_{Y'}\otimes _{R_Z}R_{Y_\ell }$ and $i_{Y_\ell } \colon R_{Y_\ell } \to R_{Y'}\otimes _{R_Z}R_{Y_\ell }$ are injective as well. We will show that the compositions

$$ \begin{align*}\pi\circ i \circ i_{Y'} \colon R_{Y'} \to R\quad \text{and}\quad \pi\circ i \circ i_{Y_\ell} \colon R_{Y_\ell} \to R\end{align*} $$

are injective. Introducing the natural embeddings $i_E \colon E \to E\otimes _L F$ and $j_{Y'} \colon R_{Y'} \to E$ , we can rewrite

$$ \begin{align*} \pi\circ i \circ i_{Y'} = \pi \circ i_E \circ j_{Y'}. \end{align*} $$

The homomorphisms $i_E$ and $j_{Y'}$ are injective. The restriction of $\pi $ to $i_E(E)$ is also injective, because E is a field. Hence, the whole composition $\pi \circ i_E \circ j_{Y'}$ is injective. The argument for $\pi \circ i \circ i_{Y_\ell }$ is analogous. Let

$$ \begin{align*}S :=\big(R_{Y'}\otimes_{R_Z}R_{Y_\ell}\big)\big/ \bigl(\mathfrak{p}\cap \big(R_{Y'}\otimes_{R_Z}R_{Y_\ell}\big)\bigr),\end{align*} $$

which is a domain, and the homomorphisms $\pi \circ i \circ i_{Y'}: R_{Y'}\to S$ and $\pi \circ i \circ i_{Y_\ell } : R_{Y_\ell }\to S$ are injective. Let $F \subset k\{\textbf {W}_\ell \}$ be such that $S = k\{\textbf {W}_\ell \}/\sqrt {\langle F\rangle }^{(\infty )}$ . We now let W be the $\Delta $ -subvariety of $\textbf {W}_\ell $ defined by $F =0 $ . For every i, $1 \leqslant i < \ell $ , the homomorphism

$$ \begin{align*}\varphi_{\ell, i}^\sharp = (\pi\circ i \circ i_{Y'})\circ\varphi_{\ell - 1, i}^\sharp : R_{Y_i}\to R_{Y'}\to S \end{align*} $$

is injective as a composition of two injective homomorphisms. Hence, the restriction $\varphi _{\ell , i} \colon W \to Y_i$ is dominant.▪

Proof By Lemma 6.15, the number of maximal trains of length $\ell $ in X is equal to the number of irreducible components of $\textbf {W}_\ell $ . By Theorem 5.13, this number does not exceed $\operatorname {\mathrm {Components}}(m,\ell n)$ .▪

Proof Denote the number of components in X by N, and assume that there is a train $(Y_1, \ldots , Y_{N + 1})$ with the Kolchin polynomial at least $\omega _X$ . Then, each of $Y_1, \sigma ^{-1}(Y_2), \ldots , \sigma ^{-N}(Y_{N + 1})$ must be a component of X, so there exist $1 \leqslant i < j \leqslant N + 1$ such that $Y_j = \sigma ^{j-i}Y_i$ . Thus, there exists an infinite train $(Y_1,\ldots ,Y_i,Y_{i+1},\ldots , Y_{j-1}, \sigma ^{j - i }(Y_i), \sigma ^{j - i}(Y_{i + 1}), \ldots )$ in X. This contradicts to $B(X, 0) < \infty $ .▪

Proof The proof follows [Reference Li, Ovchinnikov, Pogudin and Scanlon18, Lemma 6.20]. Let $B_1 := B(X, \omega _1)$ , and let T be the number of maximal trains of length $B_1$ in X. We set $B_2 := B_1 + T$ . Lemma 6.16 implies that T is bounded by $\operatorname {\mathrm {Components}}(m,nB_1)$ . Consider the fibered product $\mathbf {W}_{B_1}(X, \pi _1, \pi _2)$ , and, for each irreducible component W in it, denote the corresponding train by $Y_W$ . We set (assuming $\max \varnothing = 0$ )

$$ \begin{align*} \omega_2 := \max \bigl\{ \omega_{Y_W} \mid \omega_{Y_W} < \omega_1, W\text{ is a component of }\mathbf{W}_{B_1} \bigr\}. \end{align*} $$

We will show that $B(X, \omega _2) \leqslant B_1 + T$ . Assume that there is a maximal train $(Y_1, \ldots , Y_{B_2})$ in X with the Kolchin polynomial at least $\omega _2$ . Introduce $T + 1$ trains $Z^{(1)},\ldots ,Z^{(T + 1)}$ of length $B_1$ in $X,\sigma (X),\ldots ,\sigma ^{T}(X)$ , respectively, such that, for each j,

$$ \begin{align*} Z^{(j)}=\big( Z^{(j)}_1,\ldots,Z^{(j)}_{T}\big) := (Y_j, \ldots, Y_{j + B_1 - 1}). \end{align*} $$

Then, for each j, consider a maximal train $\tilde {Z}^{(j)}$ of length $B_1$ containing $Z^{(j)}$ . So, $\sigma ^{-j+1}(\tilde {Z}^{(j)})$ is a maximal train of length $B_1$ in X. There are two cases to consider:

(Case 1) $$ \begin{align} \big\{\omega_{Y_W}(t)\:\big|\: \omega_{Y_W}(t)<\omega_1(t),\; W \text{ is a component of } \mathbf{W}_{B_1}\big\}=\varnothing. \end{align} $$

In this case, $\tilde {Z}^{(1)}$ is a train in X with Kolchin polynomial at least $\omega _1$ . This contradicts the definition of $B(X, \omega _1)$ .

(Case 2) $$ \begin{align} \big\{\omega_{Y_W}(t)\:\big|\:\omega_{Y_W}(t)<\omega_1(t),\; W \text{ is a component of } \mathbf{W}_{B_1} \big\}\neq\varnothing. \end{align} $$

By the definition of $B(X, \omega _1)$ , for every j, $\omega _{\sigma ^{-j+1}(\tilde {Z}^{(j)})}(t) < \omega _1(t)$ . This implies that, for each j,

$$ \begin{align*} \omega_{\sigma^{-j+1}(\tilde{Z}^{(j)})}(t)=\omega_{2}(t). \end{align*} $$

Because there are only T maximal trains in X of length $B_1$ , there exist $a < b$ such that

$$ \begin{align*} \sigma^{-a+1}(\tilde{Z}^{(a)})=\sigma^{-b+1}(\tilde{Z}^{(b)}) =: Z. \end{align*} $$

Because $\omega _{Z} = \omega _{2}$ , there exists $\ell $ such that $\omega _{Z_\ell } = \omega _2$ . Because

$$ \begin{align*} \omega_{\sigma^{-a+1}({Z}^{(a)}_\ell)} = \omega_{2} \quad \text{ and }\quad \sigma^{-a+1}({Z}^{(a)}_\ell) \subseteq Z_\ell, \end{align*} $$

we have $ \sigma ^{-a+1}({Z}^{(a)}_\ell ) = Z_\ell $ . Similarly, we can show $ \sigma ^{-b+1}({Z}^{(b)}_\ell ) = Z_\ell $ . Hence,

$$ \begin{align*} \sigma^{-a+1}(Y_{a + \ell - 1}) = \sigma^{-a+1}({Z}^{(a)}_\ell) = \sigma^{-b+1}({Z}^{(b)}_\ell) = \sigma^{-b+1}(Y_{b+\ell - 1}). \end{align*} $$

Thus, we have $ Y_{b+\ell -1}=\sigma ^{b-a}(Y_{a+\ell -1}) $ . This contradicts the fact that $B(X, 0) < \infty $ .

It remains to show that $|\omega _2|$ is bounded by a computable function of n and $B_1$ . Let W be a component of $\mathbf {W}_{B_1}$ such that $\omega _{Y_W} = \omega _2$ . Let $Y_W = (Y_{W, 1}, \ldots , Y_{W, B_1})$ . There exists $1 \leqslant i \leqslant B_1$ such that $\omega _{Y_i} = \omega _2$ . Because $Y_i$ is the Kolchin closure of a linear projection of a component of $\mathbf {W}_{B_1}$ and $\mathbf {W}_{B_1}$ is bounded by $B_1n$ , Lemma 6.6 implies that $|\omega _2|$ is bounded by a computable function of n and $B_1$ .

Taking $\operatorname {\mathrm {Iter}}(n, D)$ to be the maximum of the computable bounds for $B(X, \omega _2)$ and $|\omega _2|$ , we conclude the proof.▪

Proof We recursively define the following function $G(n)$ on nonnegative integers:

$$ \begin{align*} &G(0) := \max\bigl(\operatorname{\mathrm{Components}}(n,n) + 1, \operatorname{\mathrm{KolchinProj}}(n) \bigr),\\ &G(j + 1) := \operatorname{\mathrm{Iter}}(n, G(j)),\ \ j\geqslant 0. \end{align*} $$

Consider a variety X bounded by n such that there is no infinite train in X, that is, $B(X, 0) < \infty $ . Lemma 6.18 implies that $B(X, \omega _X) - 1$ does not exceed the number of components of X. Hence, Theorem 5.13 implies that $B(X, \omega _X) \leqslant \operatorname {\mathrm {Components}}(n,n) + 1$ . Lemma 6.6 implies that $|\omega _X| \leqslant \operatorname {\mathrm {KolchinProj}}(n)$ . Repeatedly applying Lemma 6.19, we obtain a sequence of numeric polynomials

$$ \begin{align*} \omega_0 := \omega_X> \omega_1 > \omega_2 > \cdots \end{align*} $$

such that, for every $1 \leqslant i \leqslant L$ , we have $B(X, \omega _i) \leqslant G(i)$ and $|\omega _i| \leqslant G(i)$ . Because the Kolchin polynomials are well ordered, there exists L such that $\omega _L = 0$ . Proposition 6.7 implies that $L \leqslant \operatorname {\mathrm {Len}}_G$ . Hence, $B(X, 0) \leqslant G(\operatorname {\mathrm {Len}}_G)$ , where the right-hand side is a computable function of n. Set $A(n):=G(\operatorname {\mathrm {Len}}_G)$ , then $B(n,0)\leqslant A(n)$ .▪

Proof The proof is as in [Reference Li, Ovchinnikov, Pogudin and Scanlon18, Corollary 6.21], as follows. Let $X\subset \mathbb A^H$ be the $\Delta $ -variety defined by $F=0$ regarded as a system of $\Delta $ -equations in $\boldsymbol {y}, \sigma (\boldsymbol {y}),\ldots , \sigma ^h(\boldsymbol {y})$ , where $H=n(h+1)$ . By Lemmas 6.12 and 6.14, $F = 0$ has a partial solution of length D (resp. $F = 0$ has a solution in $K^{\mathbb Z}$ ) if and only if there exists a train of length D in X (resp. there exists an infinite train in X). By Proposition 6.21, if there exists a train of length $D := A(\max \{r,m,s\})$ in X, then there exists a infinite train in X. So, the assertion holds.▪

Proof The proof closely follows [Reference Li, Ovchinnikov, Pogudin and Scanlon18, Theorem 6.22]. The “ $\impliedby $ ” implication is straightforward. We will prove the “ $\implies $ ” implication. For this, let $A :=A(\max \{r, m, s\})$ from Corollary 6.22, and let B be a computable bound obtained from [Reference Gustavson, Kondratieva and Ovchinnikov10, Theorem 3.4] with

$$ \begin{align*}m\leftarrow m, \ \ n\leftarrow r(A + s + 1),\ \ h\leftarrow s,\ \ \text{and}\ \ D \leftarrow s.\end{align*} $$

By assumption,

(6.4) $$ \begin{align}1 \in \big\langle \sigma^i(F)\mid i\in \mathbb{Z}_{\geqslant 0} \big\rangle^{(\infty)}\cdot k(\boldsymbol{x}_\infty)[\boldsymbol{y}_\infty]. \end{align} $$

Suppose that

(6.5) $$ \begin{align}\langle \sigma^i(F)\mid i\in [0, A] \big\rangle^{(B)}\cap k[\boldsymbol{x}_{B+t}]=\{0\}. \end{align} $$

If

$$ \begin{align*}1 \in \big\langle \sigma^i(F)\mid i\in [0, A] \big\rangle^{({B})}\cdot k(\boldsymbol{x}_{B+t})[\boldsymbol{y}_{\infty,A + s}],\end{align*} $$

then there would exist $c_{i, j}\in k(\boldsymbol {x}_{B+t})[\boldsymbol {y}_{\infty ,A + s}]$ such that

(6.6) $$ \begin{align} 1 = \sum\limits_{\theta\in\Theta_{\Delta}(B)} \sum\limits_{j = 0}^A \sum\limits_{f\in F} c_{i, j}\theta(\sigma^j(f)). \end{align} $$

Multiplying equation (6.6) by the common denominator in the variables $\boldsymbol {x}_{B+t}$ , we obtain a contradiction with (6.5). Hence, by [Reference Gustavson, Kondratieva and Ovchinnikov10, Theorem 3.4],

$$ \begin{align*}1 \notin \big\langle \sigma^i(F)\mid i\in [0, A] \big\rangle^{(\infty)}\cdot k(\boldsymbol{x}_{B+t})[\boldsymbol{y}_{\infty, A + s}].\end{align*} $$

By Lemma 6.8, there exists a differentially closed $\Delta $ - $\sigma ^*$ -field extension $L \supset k(\boldsymbol {x}_{\infty })\supset k(\boldsymbol {x}_{B+t})$ . Then, differential Nullstellensatz implies that the system of differential equations

$$ \begin{align*} \{\sigma^i(F)=0\mid i\in [0, A]\} \end{align*} $$

in the unknowns $\boldsymbol {y}_{\infty , A + s}$ has a solution in L. Then, the system $F = 0$ has a partial solution of length $A + 1$ in L. Now, from (6.4), we see that the system $F=0$ has no solutions in $L^{\mathbb {Z}}$ . Together with the existence of a partial solution of length $A + 1$ , this contradicts to Corollary 6.22.▪