[1] Introduction Consider a sufficiently saturated model of a complete theory T. A formula φ(x;y) is an equation (for a given partition of the free variables into x and y) if the family of finite intersections of instances φ(x,a) has the descending chain condition (DCC). The theory T is equational if every formula ψ(x;y) is equivalent modulo T to a Boolean combination of equations φ(x;y). Quantifier elimination implies that the theory of algebraically closed fields of some fixed characteristic is equational. Separably closed fields of positive characteristic have quantifier elimination after adding λ-functions to the ring language [@fD88]. The imperfection degree of a separably closed field K of positive characteristic p encodes the linear dimension of K over K^(p). If the imperfection degree is finite, restricting the λ-functions to a fixed p-basis yields again equationality. A similar manipulation yields elimination of imaginaries for separably closed field K of positive characteristic and finite imperfection degree, in terms of the field of definition of the corresponding defining ideal. However, there is not an explicit description of imaginaries for separably closed fields K of infinite imperfection degree, that is, when K has infinite linear dimension over the definable subfield K^(p). Another important (expansion of a) theory of fields having infinite linear dimension over a definable subfield is the theory of an algebraically closed field with a predicate for a distinguished algebraically closed proper subfield. Any two such pairs are elementarily equivalent if and only if they have the same characteristic. They are exactly the models of the theory of Poizat’s belles paires [@Po83] of algebraically closed fields. Determining whether a particular theory is equational is not obvious. So far, the only known natural example of a stable non-equational theory is the free non-abelian finitely generated group [@zS13; @MS17]. In this paper, we will prove the equationality of several theories of fields: the theory of belles paires of algebraically closed fields of some fixed characteristic, as well as the theory of separably closed fields of arbitrary imperfection degree We also give a new proof of the equationality of the theory of differentially closed fields in positive characteristic, which was established by Srour [@gS88]. In Section 9 we include an alternative proof for belles paires of characteristic 0, by showing that definable sets are Boolean combination of certain definable sets, which are Kolchin-closed in the corresponding expansion DCF₀. A similar approach appeared already in [@aG16] using different methods. We generalise this approach to arbitrary characteristic in Section 10. Equations and indiscernible sequences Most of the results in this section come from [@PiSr84; @Ju00; @mJdL01]. We refer the avid reader to [@aO11] for a gentle introduction to equationality. We work inside a sufficiently saturated model 𝕌 of a complete theory T. A formula φ(x;y), with respect to a given partition of the free variables into x and y, is an equation if the family of finite intersections of instances φ(x,b) has the descending chain condition (DCC). If φ(x;y) is an equation, then so are φ⁻¹(y;x) = φ(x,y) and φ(f(x);y), whenever f is a ∅-definable map. Finite conjunctions and disjunctions of equations are again equations. By an abuse of notation, given an incomplete theory, we will say that a formula is an equation if it is an equation in every completion of the theory. The theory T is equational if every formula ψ(x;y) is equivalent modulo T to a Boolean combination of equations φ(x;y). Typical examples of equational theories are the theory of an equivalence relation with infinite many infinite classes, the theory of R-modules. Example 1. In any field K, for every polynomial p(X,Y) with integer coefficients, the equation p(x;y) ≐ 0 is an equation in the model-theoretic sense. Proof. This follows immediately from Hilbert’s Basis Theorem, which implies that the Zariski topology on K^(n) is noetherian, i.e. the system of all algebraic sets $$\Bigl\{a\in K^n\Bigm|\bigwedge_{i=1}^m q_i(a)=0\Bigr\},$$ where q_(i) ∈ K[X₁,…,X_(n)], has the DCC. There is a simpler proof, without using Hilbert’s Basis Theorem: Observe first that p(x;y) ≐ 0 is an equation, if p is linear in x, since then p(x;a) ≐ 0 defines a subspace of K^(n). Now, every polynomial has the form q(M₁,…,M_(m);y), where $q(u_1,\dotsc,u_m;y)$ is linear in the u_(i), for some monomials M₁, …, M_(m) in x. ◻ Quantifier elimination for the incomplete) theory ACF of algebraically closed fields and the above example yield that ACF is equational. Equationality is preserved under unnaming parameters and bi-interpretability [@Ju00]. It is unknown whether equationality holds if every formula φ(x;y), with x a single variable, is a boolean combination of equations. By compactness, a formula φ(x;y) is an equation if there is no indiscernible sequence (a_(i),b_(i))_(i ∈ ℕ) such that φ(a_(i),b_(j)) holds for i < j, but  ⊭ φ(a_(i),b_(i)). Thus, equationality implies stability [@PiSr84]. In stable theories, non-forking provides a natural notion of independence. Working inside a sufficiently saturated model, we say that two sets A and B are independent over a common subset C, denoted by $A\mathop{\mathpalette\Ind{}}_C B$, if, for every finite tuple a in A, the type tp (a/B) does not fork over C. Non-forking extensions of a type over an elementary substructure M to any set B ⊃ M are both heir and definable over M. Definition 2. A type q over B is an heir of its restriction q ↾ M to the elementary substructure M if, whenever the formula φ(x,m,b) belongs to q, with m in M and b in B, then there is some m′ in M such that φ(x,m,m′) belongs to q ↾ M. A type q over B is definable over M if, for each formula φ(x,y), there is a formula θ(y) with parameters in M such that for every b in B, φ(x,b) ∈ q if and only if  ⊨ θ(b). Observe that if q is definable over M, for any formula φ(x,y), any two such formulae θ(y) are equivalent modulo M, so call it the φ-definition of q. If φ is an equation, the φ-definition of a type q over B is particularly simple. The intersection $$\bigcap\limits_{\varphi(x,b)\in q} \varphi(\mathbb U,b)$$ is a definable set given by a formula ψ(x) over B contained in q. If suffices to set θ(y) = ∀x(ψ(x)→φ(x,y)). By the above characterisation, a formula φ(x;y) is an equation if and only if every instance φ(a,y) is indiscernibly closed definable sets [@mJdL01 Theorem 3.16]. A definable set is indiscernibly closed if, whenever (b_(i))_(i ≤ ω) is an indiscernible sequence such that b_(i) lies in X for i < ω, then so does b_(ω). Extending the indiscernible sequence so that it becomes a Morley sequence over an initial segment, we conclude the following: Lemma 3. In a complete stable theory T, a definable set φ(a,y) is indiscernibly closed if, for every elementary substructure M and every Morley sequence (b_(i))_(i ≤ ω) over M such that $$a\mathop{\mathpalette\Ind{}}_M b_i \text{ with } \models \varphi(a,b_i) \text{ for } i <\omega,$$ then b_(ω) realises φ(a,y) as well. We may take the sequence of length κ + 1, for every infinite cardinal κ, and assume that $a\mathop{\mathpalette\Ind{}}_M \{b_i\}_{i<\kappa}$. In [@gS88 Theorem 2.5], Srour stated a different criterion for the equationality of a formula. Let us provide a version of his result. Given a formula φ(x,y) and a type p over B, denote p_(φ)⁺ = {φ(x,b) ∣ φ(x,b) ∈ p}. Lemma 4. Given a formula φ(x;y) in a stable theory T, the following are equivalent: 1. [L:Srour_eq] The formula φ(x;y) is an equation. 2. [L:Srour_fteset] Given a tuple a of length |x| and a subset B, there is a finite subset B₀ of B such that tp_(φ)⁺(a/B₀) ⊢ tp_(φ)⁺(a/B). 3. [L:Srour_ind] There is a regular cardinal κ > |T| such that, for any tuple a of length |x| and any elementary substructures M ⊂ N with $a\mathop{\mathpalette\Ind{}}_M N$ and |N| = κ, there is a subset B₀ of N with |B₀| < κ such that tp (a/MB₀) ⊢ tp_(φ)⁺(a/N). Proof. For $(\ref{L:Srour_eq})\Longrightarrow (\ref{L:Srour_fteset})$, we observe that the intersection ⋂ {φ(𝕌,b) ∣ φ(x,b) ∈ tp_(φ)⁺(a/B)} is a finite intersection with parameters in a finite subset B₀ of B. The implication $(\ref{L:Srour_fteset})\Longrightarrow (\ref{L:Srour_ind})$ is immediate. For $(\ref{L:Srour_ind})\Longrightarrow (\ref{L:Srour_eq})$, it suffices to show that the set φ(a,y) is indiscernibly closed, for every tuple a of length |x|. By Lemma Lemma 3, let M be an elementary substructure and (b_(i))_(i ≤ κ) a Morley sequence over M such that $$a\mathop{\mathpalette\Ind{}}_M (b_i)_{i<\kappa} \text{ and } \models \varphi(a,b_i) \text{ for } i <\kappa.$$ We construct a continuous chain of elementary substructures (N_(i))_(i < κ), each of cardinality at most κ containing M, such that: - the sequence (b_(j))_(i ≤ j ≤ κ) remains indiscernible over N_(i); - b_( < i) is contained in N_(i); - $a\mathop{\mathpalette\Ind{}}_M N_i\cup (b_j)_{i\leq j<\kappa} .$ Set N₀ = M. For i < κ limit ordinal, set $$N_i=\bigcup\limits_{j 0. The corresponding notion of K^(p)-special is separability: A non-zero polynomial f(T) over a subfield K is separable if every root (in the algebraic closure of K) has multiplicity 1, or equivalently, if f and its formal derivative $\frac{\partial f}{\partial T}$ are coprime. Whenever f is irreducible, the latter is equivalent to $\frac{\partial f}{\partial T}\neq 0$. In particular, every non-constant polynomial in characteristic 0 is separable. In positive characteristic p, an irreducible polynomial f is separable if and only if f is not a polynomial in T^(p). An algebraic extension K ⊂ L is separable if the minimal polynomial over K of every element in L is separable. Algebraic field extensions in characteristic 0 are always separable. In positive characteristic p, the finite extension is separable if and only if the fields K and L^(p) are linearly disjoint over K^(p). This explains the following definition: Definition 9. An arbitrary (possibly not algebraic) field extension F ⊂ K is separable if, either the characteristic is 0 or, in case the characteristic is p > 0, the fields F and K^(p) are linearly disjoint over F^(p). A field K is perfect if either it has characteristic 0 or if K = K^(p), for p = char(K). Any field extension of a perfect field is separable. Given a field K, we define its imperfection degree (in ℕ ∪ {∞}), as 0 if the characteristic of K is 0, or ∞, in case of positive characteristic p if [K:K^(p)] is infinite. Otherwise [K:K^(p)] = p^(e) for e the degree of imperfection. Thus, a field is perfect if and only if its imperfection degree is 0 Another example of fields equipped with a definable subfields are differential fields. A differential field consists of a field K together with a distinguished additive morphism δ satisfying Leibniz’ rule δ(xy) = xδ(y) + yδ(x). Analogously to Zariski-closed sets for pure field, one defines Kolchin-closed sets in differential fields as zero sets of systems of differential-polynomials equations, that is, polynomial equations on the different iterates of the variables under the derivation. For a tuple x = (x₁,…,x_(n)) in K, denote by δ(x) the tuple (δ(x₁),…,δ(x_(n))). Lemma 10. In any differential field (K,δ), an algebraic differential equation p(x,δx,δ²x…;y,δy,δ²y,…) ≐ 0 is an equation in the model-theoretic sense. Proof. In characteristic zero this follows from Ritt-Raudenbush’s Theorem, which states that the Kolchin topology is noetherian. In arbitrary characteristic, it suffices to observe, as in Example Example 1, that p(x,δx,…;y,δy,…) can be written as q(M₁,…;y,δy,…) where $q(u_1,\dotsc;y_0,y_1,\ldots)$ is linear in the u_(i)’s, for some differential monomials M_(j)’s in x. ◻ In particular, the theory DCF₀ of differentially closed fields of characteristic 0 is equational, since it has quantifier elimination [@cW98]. In a differential field (K,δ), the set of constants C_(K) = {x ∈ K ∣ δ(x) = 0} is a definable subfield, which contains K^(p) if p = char(K) > 0. If K is algebraically closed, then so is C_(K). Fact 11. The elements a₁, …, a_(k) of the differential field (K,δ) are linearly dependent over C_(K) = {x ∈ K ∣ δ(x) = 0} if and only if their Wronskian W (a₁,…,a_(k)) is 0, where $$\mathop{\mathrm{W}}(a_1,\ldots, a_k)=\det\begin{pmatrix} a_1 & a_2 & \ldots & a_k \\ \delta(a_1) & \delta(a_2) & \ldots & \delta(a_k) \\ \vdots & & \vdots & \\ \delta^{k-1}(a_1) & \delta^{k-1}(a_2) & \ldots & \delta^{k-1}(a_k) \end{pmatrix}.$$ Whether the above matrix has determinant 0 does not dependon the differential field where we compute it. In particular, every differential subfield L of K is C_(K)-special. Perfect fields of positive characteristic cannot have non-trivial derivations. In characteristic zero though, any field K which is notalgebraic over the prime field has a non-trivial derivation δ. Analogously to perfectness, we say that the differential field (K,δ) is differentially perfect if either K has characteristic 0 or, in case p = char(K) > 0, if every constant has a p^(th)-root, that is, if C_(K) = K^(p). Notice that the following well-known result generalises the equivalent situation for perfect fields and separable extensions. Remark 12. Let (K,δ) be a differential field and F a differentially perfect differential subfield of K. The extension F ⊂ K is separable. Proof. We need only prove it when the characteristic of K is p > 0. By Fact Fact 11, the fields F and C_(K) are linearly disjoint over C_(F) = F^(p). Since K^(p) ⊂ C_(K), this implies that F and K^(p) are linearly disjoint over F^(p). ◻ In section 8, we will consider a third theory of fields equipped with a definable subfield: belles paires of algebraically closed fields. In order to show that the corresponding theory is equational, we require some basic notions from linear algebra ( [@jD74 Résultats d’Algèbre]). Fix some subfield E of 𝕌. Let V be a vector subspace of E^(n) with basis {v₁, …, v_(k)}. Observe that $$V=\bigl\{v\in E^n\,\bigm|\, v\wedge (v_1\wedge\cdots\wedge v_k)=0 \text{ in } \@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^{k+1} E^n\bigr\}.$$ The vector v₁ ∧ ⋯ ∧ v_(k) depends only on V, up to scalar multiplication, and determines V completely. The Plücker coordinates Pk (V) of V are the homogeneous coordinates of v₁ ∧ ⋯ ∧ v_(k) with respect to the canonical basis of $\@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^{k} E^n$. The k^(th)-Grassmannian Gr_(k)(E^(n)) of E^(n) is the collection of Plücker coordinates of all k-dimensional subspaces of E^(n). Clearly Gr_(k)(E^(n)) is contained in ℙ^(r − 1)(E), for $r={n \choose k}$. The k^(th)-Grassmannian is Zariski-closed. Indeed, given an element ζ of $\@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^k E^n$, there is a smallest vector subspace V_(ζ) of E^(n) such that ζ belongs to $\@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^k V_\zeta$. The vector space V_(ζ) is the collection of inner products e⌟ ζ, for e in $\@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^{k-1} (E^n)^*$. Recall that the inner product ⌟  is a bilinear map $$\operatorname{\lrcorner}: \@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^{k-1} (E^n)^* \times \@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^{k} (E^n) \to E.$$ A non-trivial element ζ of $\@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^k E^n$ determines a k-dimensional subspace of E^(n) if and only if ζ ∧ (e⌟ζ) = 0, for every e in $\@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^{k-1} (E^n)^*$. Letting e run over a fixed basis of $\@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^{k-1} (E^n)^*$, we see that the k^(th)-Grassmannian is the zero-set of a finite collection of homogeneous polynomials. Let us conclude this section with an observation regarding projections of certain varieties. Remark 13. Though the theory of algebraically closed fields has elimination of quantifiers, the projection of a Zariski-closed set need not be again closed. For example, the closed set V = {(x,z) ∈ E × E ∣ x ⋅ z = 1} projects onto the open set {x ∈ E | x ≠ 0}. An algebraic variety Z is complete if, for all varieties X, the projection X × Z → X is a Zariski-closed map. Projective varieties are complete. Model Theory of separably closed fields Recall that a field K is separably closed if it has no proper algebraic separable extension, or equivalently, if every non-constant separable polynomial over K has a root in K. For each fixed degree, this can be expressed in the language of rings. Thus, the class of separably closed fields is axiomatisable. Separably closed fields of characteristic zero are algebraically closed. For a prime p, let SCF_(p) denote the theory of separably closed fields of characteristic p and SCF_(p, e) the theory of separably closed fields of characteristic p and imperfection degree e. Note that SCF_(p, 0) is the theory ACF_(p) of algebraically closed fields of characteristic p. Fact 14. (cf. [@fD88 Proposition 27]) The theory SCF_(p, e) is complete and stable, but not superstable for e > 0. Given a model K and a separable field extension k ⊂ K, the type of k in K is completely determined by its quantifier-free type. In particular, the theory has quantifier elimination in the language ℒ_(λ) = ℒ_(rings) ∪ {λ_(n)^(i) ∣ 1 ≤ i ≤ n < ω}, where the value λ_(n)^(i)(a₀,…,a_(n)) is defined as follows in K. If there is a unique sequence $\zeta_1,\dotsc,\zeta_n\in K$ with $a_0 = \zeta_1^p \, a_1+\dotsb+\zeta_n^p\,a_n$, we set λ_(n)^(i)(a₀,…,a_(n)) = ζ_(i). Otherwise, we set λ_(n)^(i)(a₀,…,a_(n)) = 0 and call it undefined, Note that λ_(n)^(i)(a₀,…,a_(n)) is defined if and only if $$K\models \neg \mathop{\mathrm{\text{$p$}\hspace{0.12em}-Dep}}_n(a_1,\ldots,a_n) \land \mathop{\mathrm{\text{$p$}\hspace{0.12em}-Dep}}_{n+1}(a_0,a_1,\ldots,a_n),$$ where $\mathop{\mathrm{\text{$p$}\hspace{0.12em}-Dep}}_n(a_1,\ldots,a_n)$ means that $a_1,\dotsc,a_n$ are K^(p)-linearly dependent. In particular, the value λ_(n)^(i)(a₀,…,a_(n)) is undefined for n > p^(e). For a subfield k of a model K of SCF_(p), the field extension k ⊂ K is separable if and only if k is closed under λ-functions. Notation 1. For elements a₀, …, a_(n) of K, the notation $\overline{\lambda}(a_0, a_1,\ldots,a_n)\!\downarrow$ is an abbreviation for $\neg \mathop{\mathrm{\text{$p$}\hspace{0.12em}-Dep}}_n(a_1,\ldots,a_n) \land \mathop{\mathrm{\text{$p$}\hspace{0.12em}-Dep}}_{n+1}(a_0,a_1,\ldots,a_n)$. Remark 15. If the imperfection degree e is finite, we can fix a p-basis $\mathbf{b}=(b_1,\dotsc,b_e)$ of K, that is, a tuple such that the collection of monomials $$\mathbf{\bar b}=(b_1^{\nu_1}\dotsb b_e^{\nu_e}\,\mid\, 0\leq \nu_1,\dotsc,\nu_e 0 is equational. Proof. Proposition Proposition 19 yields, that modulo SCF_(p) every formula is a Boolean combination of sentences (i.e. formulas without free variables) and λ-tame formulas. Sentences are equations by definition, λ-tame formulas are equations by Theorem Theorem 21. ◻ Lemma Lemma 6 and Theorem Theorem 21 yield a partial elimination of imaginaries for SCF_(p, e). Corollary 23. The theory SCF_(p, e) of separably closed fields of characteristic p > 0 and imperfection degree e has weak elimination of imaginaries, after adding canonical parameters for all instances of λ-tame formulae. Question 1. Is there an explicit description of the canonical parameters of instances of λ-tame formulae, similar to the geometric sorts introduced in [@aP07]? Model Theory of differentially closed fields in positive characteristic The model theory of existentially closed differential fields in positive characteristic has been thoroughly studied by Wood [@cW73; @cW76]. In contrast to the characteristic 0 case, the corresponding theory is no longer ω-stable nor superstable: its universe is a separably closed field of infinite imperfection degree (see Section 4). A differential field (K,δ) is differentially closed if it is existentially closed in the class of differential fields. That is, whenever a quantifier-free ℒ_(δ) = ℒ_(rings) ∪ {δ}-formula φ(x₁,…,x_(n)), with parameters in K, has a realisation in a differential field extension (L,δ_(L)) of (K,δ), then there is a realisation of φ(x₁,…,x_(n)) in K. A differential polynomial p(x) is a polynomial in x and its higher order derivatives $\delta(x),\delta^2(x),\dotsc$ The order of p is the order of the highest occurring derivative. Fact 24. The class of differentially closed fields of positive characteristic p can be axiomatised by the complete theory DCF_(p) with following axioms: - The universe is a differentially perfect differential field of characteristic p. - Given two differential polynomials g(x) ≠ 0 and f(x) in one variable with ord (g) < ord (f) = n such that the separant $s_f=\frac{\partial f}{\partial (\delta^nx)}$ of f is not identically 0, there exists an element a with g(a) ≠ 0 and f(a) = 0. The type of a differentially perfect differential subfield is determined by its quantifier-free type. The theory DCF_(p) is stable but not superstable, and has quantifier-elimination in the language ℒ_(δ, s) = ℒ_(δ) ∪ {s}, where s is the following unary function: $$s(a)= \begin{cases} b, \text{ with } a=b^p \text{ in case } \delta(a)=0. \\ 0, \text{ otherwise.} \end{cases}$$ Note that every non-constant separable polynomial is a differential polynomial of order 0 whose separant is non-trivial (since δ⁰(x) = x). In particular, every model K of DCF_(p) is a separably closed field. Furthermore, the imperfection degree of K is infinite: Choose for every n in ℕ an element a_(n) in K with δ^(n)(a_(n)) = 0 but δ^(n − 1)(a_(n)) ≠ 0. It is easy to see that the family {a_(n)}_(n ∈ ℕ) is linearly independent over K^(p). Remark 25. The quotient field of any ℒ_(δ, s)-substructure of a model of DCF_(p) is differentially perfect. Proof. Let $\frac{a}{b}$ be an element in the quotient field with derivative 0. The element $ab^{p-1}=\frac{a}{b} b^p$ is also a constant, so ab^(p − 1) = s(ab^(p − 1))^(p). Hence $$\frac{a}{b} = \Bigl(\frac{s(ab^{p-1})}{b}\Bigr)^p.$$  ◻ From now on, we work inside a sufficiently saturated model K of DCF_(p). Corollary 26. Consider two subfields A and B of K containing an elementary substructure M of K. Whenever $$A\mathop{\mathpalette\Ind{}}^{\mathsf{DCF}_p}_M B,$$ the fields K^(p) ⋅ A and K^(p) ⋅ B are linearly disjoint over K^(p) ⋅ M. Proof. The quotient field A′ of the ℒ_(δ, s)-structure generated by A is K^(p)-special, by the Remarks Remark 12 and Remark 25. The result now follows from Lemma Lemma 8, as in the proof of Corollary Corollary 16. ◻ We will now present a relative quantifier elimination, by isolating the formulae which will be our candidates for the equationality of DCF_(p). Definition 27. Let x be a tuple of variables. A formula φ(x) in the language ℒ_(δ) is δ-tame if there are differential polynomials q₁, …, q_(m), with q_(i) in the differential ring ℤ{X, T₁, …, T_(i − 1)}, and a system of differential equations Σ in ℤ{X, T₁, …, T_(n)} such that $$\varphi(x )\;\;=\;\;\exists\, z_1\ldots \exists z_n \Bigl( \bigwedge_{j=1}^{n} z_j^p\doteq q_j(x,z_1,\ldots, z_{j-1}) \land\; \Sigma(x,z_1,\ldots, z_n)\Bigr).$$ Proposition 28. Every formula in DCF_(p) is a Boolean combination of δ-tame formulae. Proof. The proof is a direct adaptation of the proof of Proposition Proposition 19. We need only show that the equation t(x) ≐ 0 is a Boolean combination of δ-tame formulae, for every ℒ_(δ, s)-term t(x). Proceed by induction on the number of occurrences of s in t. Suppose that t(x) = r(x,s(q(x))), for some ℒ_(δ, s)-term r and a polynomial q, By induction, the equation r(x,z) ≐ 0 is equivalent to a Boolean combination $BK(\psi_1(x,z),\dotsc)$ of δ-tame formulae. Thus t(x) ≐ 0 ist equivalent to $$\bigl(\neg\delta(q(x))\doteq0\;\land\;r(x,0)\doteq0\bigr)\;\,\lor\;\, \bigl(\delta(q(x))\doteq0\;\land\; BK(\exists z\,z^p\doteq q(x)\,\land\,\psi_1(x,z),\dotsc)\bigr),$$ which is, by induction, a Boolean combination of δ-tame formulae. ◻ We conclude this section with a homogenisation result for δ-tame formulae, as in Proposition Proposition 20. Proposition 29. Given a δ-tame formula φ(x₁,…,x_(n)) and natural numbers k₁, …, k_(n), there is a δ-tame formula φ′(x₀,…,x_(n)) such that $$\mathsf{DCF}_p\vdash\forall x_0 \ldots \forall x_n \Bigl( \varphi'(x_0,\ldots, x_n)\longleftrightarrow \Bigl( \varphi\Bigl(\frac{x_1}{x_0^{k_1}},\ldots, \frac{x_n}{x_0^{k_n}}\Bigr) \lor x_0 \doteq 0 \Bigr) \Bigr) .$$ Proof. We prove it by induction on the number of existential quantifiers iny φ. If φ is a system Σ of differential equations, rewrite $$\Sigma(\frac{x_1}{x_0^{k_1}},\ldots, \frac{x_n}{x_0^{k_n}}) \Longleftrightarrow \frac{\Sigma'(x_0,\ldots, x_n)}{x^N_0} ,$$ for some natural number N and a system of differential equations Σ′(x₀,…,x_(n)). Set φ′(x₀,…,x_(n)) = x₀ ⋅ Σ′(x₀,…,x_(n)). For a general δ-tame formula, write φ(x₁,…,x_(n)) = ∃z (z^(p)≐q(x₁,…,x_(n))∧ψ(x₁,…,x_(n),z)), for some polynomial q and a δ-tame formula ψ with one existential quantifier less. There is a polynomial q′(x₀,…,x_(n)) such that $$q(\frac{x_1}{x_0^{k_1}},\ldots, \frac{x_n}{x_0^{k_n}})=\frac{q'(x_0,\ldots,x_n)}{x_0^{pN-1}},$$ for some natural number N. By induction, there is a δ-tame formula ψ′(x₀,…,x_(n),z) such that $$\mathsf{DCF}_p\vdash\forall x_0 \ldots \forall x_n \forall z \Bigl( \psi'(x_0,\ldots, x_n, z)\longleftrightarrow \Bigl( \psi\Bigl(\frac{x_1}{x_0^{k_1}},\ldots, \frac{x_n}{x_0^{k_n}}, \frac{z}{x^N_0}\Bigr) \lor x_0 \doteq 0 \Bigr) \Bigr) .$$ Set now φ′(x₀,…,x_(n)) = ∃z(z^(p)≐x₀⋅q′(x₁,…,x_(n))∧ψ′(x₀,x₁,…,x_(n),z)).  ◻ Equationality of DCF_(p) We have now all the ingredients to show that the theory DCF_(p) of existentially closed differential fields of positive characteristic p is equational. Working inside a sufficiently saturated model K of DCF_(p), given a δ-tame formula in a fied partition of the variables x and y, one can show, similar to the proof of Theorem Theorem 21, that the set φ(a,y) is indiscernibly closed. However, we will provide a proof, which resonates with Srour’s approach [@gS88], using Lemma Lemma 4. We would like to express our gratitude to Zoé Chatzidakis and Carol Wood for pointing out Srour’s result. Theorem 30 (Srour [@gS88]). In any partition of the variables, the δ-tame formula φ(x;y) is an equation. Srour proved this for the equivalent notion of S-formulae, cf. Definition Definition 33 and Lemma Lemma 34. Proof. We prove it by induction on the number n of existential quantifiers. For n = 0, the formula φ(x;y) is a system of differential equations, which is clearly an equation, by Lemma Lemma 10. For n > 0, write φ(x,y) as $$\exists z \Bigl( z^p\doteq q(x,y)\; \land\; \psi(x,y,z) \Bigr),$$ where ψ(x,y,z) is a δ-tame formula with n − 1 existential quantifiers. Claim 2. Suppose that every differential monomial in x occurs in q(x,y) as a p^(th)-power. Then φ(x;y) is an equation. Proof of Claim. It suffices to prove that φ(x,b) is equivalent to a δ-tame formula ψ′(x,b,b′) with n − 1 existential quantifiers, for some tuple b′. Choose a K^(p)-basis $1=b_0,\dotsc,b_N$ of the differential monomials in b occurring in q(x,b) and write $q(x,b)=\sum_{i=0}^Nq_i(x,b')^p\cdot b_i$. Then φ(x,b) is equivalent (in DCF_(p)) to $$\exists z \Bigl( z\doteq q_0(x,b')\;\land\; \bigwedge\limits_{i=1}^N q_i(x,b')\doteq 0 \land\; \psi(x,b,z) \Bigr),$$ which is equivalent to $$\psi'(x,b,b')=\Bigr(\bigwedge\limits_{i=1}^N q_i(x,b')\doteq 0 \;\land\; \psi(x,b,q_0(x,b')) \Bigr).$$ Claim In order to show that φ(x;y) is an equation, we will apply Remark Remark 5. Consider a tuple a of length |x|, and two elementary substructures M ⊂ N with $a\mathop{\mathpalette\Ind{}}_M N$. Choose now a K^(p) ⋅ M-basis $a_0,\dotsc,a_M$ of the differential monomials in a which occur in q(a,y) and write $$q(a,y)=\sum\limits_{i=0}^N q_i(a'^p,m,y)\cdot a_i,$$ for tuples a′ in K and m in M, and differential polynomials q_(i)(x′,y′,y) with integer coefficients and linear in x′ and y′. Observe that we may assume that $a'\mathop{\mathpalette\Ind{}}_{Ma} N$, which implies $aa'\mathop{\mathpalette\Ind{}}_M N$. By Corollary Corollary 26, the elements $a_0,\dotsc,a_M$ remain linearly independent over K^(p) ⋅ N. Thus, for all b in N, K ⊨ φ(a,b) ↔ ψ′(a,a′,m,b), where $$\psi'(x,x',y',y)\;\;=\;\;\exists z \Bigl( z^p\doteq q_0(x'^p,y',y) \land\; \bigwedge\limits_{i=1}^N q_i(x'^p,y',y)\doteq 0 \land\; \psi(x, y, z) \Bigr).$$ By the previous claim, the δ-tame formula ψ′(x,x′;y′,y) is an equation, so tp (a,a′/M) ⊢ tp_(ψ′)⁺(a,a′/N). In order to show that tp (a/M) ⊢ tp_(φ)⁺(a/N), consider a realisation ã of tp (a/M) and an instance φ(x,b) in tp_(φ)⁺(a/N). There is a tuple ã′ such that aa′≡_(M)ãã′. Since K ⊨ ψ′(a,a′,m,b), we have K ⊨ ψ′(ã,ã′,m,b). Observe that there are $\tilde a_0,\dotsc,\tilde a_N$ whith $q(\tilde a,y)=\sum\limits_{i=0}^N q_i(\tilde a'^p,m,y)\cdot \tilde a_i$, so we have in particular that q(ã,b) = q₀(ã′,m,b), whence K ⊨ φ(ã,b), as desired. ◻ Together with Proposition Proposition 28, we conclude the following result: Corollary 31. The theory DCF_(p) of existentially closed differential fields is equational. Similar to Corollary Corollary 23, there is a partial elimination of imaginaries for DCF_(p), by Lemma Lemma 6 and Theorem Theorem 30. Unfortunately, we do not have either an explicit description of the canonical parameters of instances of δ-tame formulae. Corollary 32. The theory DCF_(p) of differentially closed fields of positive characteristic p has weak elimination of imaginaries, after adding canonical parameters for all instances of δ-tame formulae. Digression: On Srour’s proof of the equationality of DCF_(p) Definition 33 (Srour [@gS88]). An S-Formula φ is a conjunction of ℒ_(δ, s)-equations such that, for every subterm s(r) of a term occurring in φ, the equation δ(r) ≐ 0 belongs to φ. Srour’s proof first shows that every formula is equivalent in DCF_(p)to a Boolean combination of S-formulae. This follows from Proposition Proposition 28, as the next Lemma shows. Lemma 34. Every tame δ-formula is equivalent to an S-formula, and conversely. Proof. For every ℒ_(δ, s)-formula ψ(x,z) and every polynomial q(x), observe that $$\mathsf{DCF}_p\;\vdash\;\; \exists z\,\Bigl(z^p\doteq q(x)\land\psi\bigl(x,z\bigr)\Bigr)\;\longleftrightarrow\;\Bigl(\delta(q)\doteq 0\land\psi\bigl(x,s(q(x))\bigr)\Bigr).$$  ◻ In order to show that S-formulae φ(x;y) are equations, Srour uses the fact that, whenever A and B are elementary submodels of a model K of DCF_(p) which are linearly disjoint over their intersection M, then for every a ∈ A and any S-formula φ(x;y), tp (a/M) ⊢ tp_(φ)⁺(a/B). In order to do so, he observes that S-formulae are preserved under differential ring homomorphisms, as well as a striking result of Shelah (see the the proof of [@sS16 Theorem 9]): the ring generated by A and B is differentially perfect, that is, it is closed under s. We would like to present a slightly simpler proof of Shelah’s result. Lemma 35. (Shelah’s Lemma [@sS16 Theorem 9]) Let M be a common differential subfield of the the two differential fields A and B and R = A⊗_(M)B. If M is existentially closed in B, then the ring of constants of R is generated by C_(A) and C_(B). In particular, in characteristic p, the ring R is differentially perfect, whenever both A and B are. Proof. Claim . The differential field A is existentially closed in R. In particular R is an integral domain. Proof of Claim . Suppose R ⊨ ρ(a,r), for some quantifier-free δ-formula ρ(x,y), and tuples a in A and r in R. Rewriting ρ, we may assume that r = b and a occurs linearly in ρ and is an enumeration of a basis of A over M. In particular, there is a quantifier-free formula ρ′(y) such that for all b ∈ B $$R\models \forall y \Bigl (\rho(a,b)\longleftrightarrow \rho'(b) \Bigr).$$ Since M is existentially closed in B, and the validity of quantifier-free formulae is preserved under substructures, we conclude that there is some a′ in M satisfying ρ′(y) and thus ρ(a,a′) holds in R, and hence in A. Claim  Let K be the quotient field of R. Claim . [Cl:prep] The ring of constants of the ring R′ generated by A and C_(B) is generated by C_(A) and C_(B). Proof of Claim . Let (a_(i)) be a basis of A over C_(A), with a₀ = 1. Every x in R′ can be written as ∑_(i)a_(i) ⋅ c_(i), for some c_(i) in the ring generated by C_(A) and C_(B). By Fact Fact 11, the a_(i)’s are independent over C_(K). If x is a constant in R′ ⊂ K, then x = c₀. Claim  Fix now a basis (a_(i))_(i ∈ I) of A over M and let x = ∑_(i ∈ I)a_(i) ⋅ b_(i) be a constant in R. Claim . All δ(b_(j)) are in the M-span of {b_(i) ∣ i ∈ I}. Proof of Claim . Write δ(a_(j)) = ∑_(i ∈ I)m_(j, i)a_(i) for m_(j, i) ∈ M. Since 0 = δ(x), we have 0 = ∑_(i)a_(i) ⋅ δ(b_(i)) + ∑_(j)(∑_(i)m_(j, i)a_(i)) ⋅ b_(j) = ∑_(i)a_(i) ⋅ δ(b_(i)) + ∑_(i)a_(i) ⋅ (∑_(j)m_(i, j)b_(j)), whence δ(b_(i)) =  − ∑_(j)m_(j, i)b_(i). Claim  Claim . All b_(i)’s lie in the ring generated by M and C_(B). Proof of Claim . Let b ∈ B^(n) be the column vector of the non-zero elements of {b_(i) ∣ i ∈ I}. By the last claim, there is an n × n-matrix H with coefficients in M with δ(b) = H ⋅ b. Let u¹, …, u^(m) be a maximal linearly independent system of solutions of δ(y) = H ⋅ y in M^(n). Consider the n × m-matrix U with columns u¹, …, u^(m). Since M is existentially closed in B, the column vectors u¹, …u^(m), b must be linearly dependent, so b = U ⋅ z for some vector z in B^(m). It follows that H ⋅ b = δ(b) = δ(U) ⋅ z + U ⋅ δ(z) = H ⋅ U ⋅ z + U ⋅ δ(z) = H ⋅ b + U ⋅ δ(z), whence δ(z) = 0. Claim  In particular, the constant x lies in the ring R′ from Claim [Cl:prep], so x is in the ring generated by C_(A) and C_(B). ◻ Interlude: An alternative proof of the equationality of SCF_(p, ∞) As a by-product of Theorem Theorem 30, we obtain a different proof of the equationality of SCF_(p, ∞): We will show that every λ-tame formula is an equation, since it is equivalent in a particular model of SCF_(p, ∞), namely a differentially closed field of characteristic p, to a δ-tame formula. A similar method will appear again in Corollary Corollary 55. Proposition 36. Every λ-tame formula is equivalent in DCF_(p) to a δ-tame formula. Proof. Work inside a model (K,δ) of DCF_(p). The proof goes by induction on the degree of the λ-tame formula φ(x). If φ is a polynomial equation, there is nothing to prove. Since the result follows for conjunctions, we need only consider the particular case when φ is of the form: $$\varphi(x)=\mathop{\mathrm{\text{$p$}\hspace{0.12em}-Dep}}_n(q_1,\dotsc, q_n)\;\lor\; (\overline{\lambda}(q_0,\dotsc,q_n)\!\downarrow\land\, \psi(x, \overline{\lambda}(q_0, \ldots, q_n))),$$ for some λ-tame formula ψ(x,z₁,…,z_(n)) of strictly smaller degree and polynomials q₀, …, q_(n) in ℤ[x]. Let W (x) = W (q₁,…,q_(n)) be the Wronskian of q₁, …, q_(n), that is, the determinant of the matrix $$A(x)=\begin{pmatrix} q_1 & q_2 & \ldots & q_n \\ \delta(q_1) & \delta(q_2) & \ldots & \delta(q_n) \\ \vdots & & \vdots & \\ \delta^{n-1}(q_1) & \delta^{n-1}(q_2) & \ldots & \delta^{n-1}(q_n) \end{pmatrix}.$$ and B(x) be the adjoint matrix of A(x). Set $$D(x)= \begin{pmatrix} q_0 \\ \delta(q_0)\\ \vdots\\ \delta^{n-1}(q_0) \end{pmatrix}.$$ Since K is differentially perfect, the elements q₁(x), …, q_(n)(x) are linearly independent over K^(p) if and only if W (x) ≠ 0. In that case, the functions $\overline{\lambda}(q_0,\dotsc,q_n)$ are defined if and only if every coordinate of the vector W (x)⁻¹  ⋅ B(x) ⋅ D(x) is a constant, in which case we have $$\overline\lambda(q_0,\dotsc,q_n)^p={\mathop{\mathrm{W}}(x)} ^{-1}\!\cdot B(x)\cdot D(x),$$ or equivalently, $$(\mathop{\mathrm{W}}(x)\cdot \overline\lambda(q_0,\dotsc,q_n))^p= \mathop{\mathrm{W}}(x)^{p-1}\!\cdot B(x)\cdot D(x)$$ By induction, the formula ψ(x,z₁,…,z_(n)) is equivalent to a δ-tame formula ψ_(δ). Homogenising with respecto to $z_0, z_1,\dotsc, z_n$, as in Proposition Proposition 29, there is a δ-tame formula ψ′_(δ)(x,z₀,z₁,…,z_(n)) equivalent to $$\psi_\delta(x,\frac{z_1}{z_0},\ldots, \frac{z_n}{z_0} )\lor z_0\doteq 0$$ Therefore, if z = (z₁,⋯,z_(n)), then $$K\models \Bigl(\varphi(x) \longleftrightarrow \exists z\; \bigl(z^p\doteq \mathop{\mathrm{W}}(x)^{p-1}\cdot B(x)\cdot D(x)\;\land\;\psi'_\delta(x,\mathop{\mathrm{W}}(x),z)\bigr) \Bigr).$$ The right-hand side is a δ-tame formula, as desired. ◻ By Propositions Proposition 19 and Proposition 36, and Theorem Theorem 30, we obtain a different proof of Corollary Corollary 22: Corollary 37. The theory SCF_(p, ∞) of separably closed fields of characteristic p > 0 and infinite imperfection degree is equational. Model Theory of Pairs The last theory of fields we will consider in this work is the (incomplete) theory ACFP of proper pairs of algebraically closed fields. Most of the results mentioned here appear in [@jK64; @Po83; @BPV03]. Work inside a sufficiently saturated model (K,E) of ACFP in the language ℒ_(P) = ℒ_(rings) ∪ {P}, where E = P(K) is the proper subfield. We will use the index P to refer to the expansion ACFP. A subfield A of K is tame if A is algebraically independent from E over E_(A) = E ∩ A, that is, $$A\mathop{\mathpalette\Ind{}}^\mathsf{ACF}_{E_A} E.$$ Tameness was called P-independence in [@BPV03], but in order to avoid a possible confusion, we have decided to use a different terminology. Fact 38. The completions of the theory ACFP of proper pairs of algebraically closed fields are obtained once the characteristic is fixed. Each of these completions is ω-stable of Morley rank ω. The ℒ_(P)-type of a tame subfield of K is uniquely determined by its ℒ_(P)-quantifier-free type. Every subfield of E is automatically tame, so the induced structure on E agrees with the field structure. The subfield E is a pure algebraically closed field and has Morley rank 1. If A is a tame subfield, then its ℒ_(P)-definable closure coincides with the inseparable closure of A and its ℒ_(P)-algebraic closure is the field algebraic closure acl (A) of A, and E_(acl_(P)(A)) = acl (E_(A)). Based on the above fact, Delon [@fD12] considered the following expansion of the language ℒ_(P): ℒ_(D) = ℒ_(P) ∪ {Dep_(n), λ_(n)^(i)}_(1 ≤ i ≤ n ∈ ℕ), where the relation Dep_(n) is defined as follows: K ⊨ Dep_(n)(a₁,…,a_(n)) ⇔ a₁, …, a_(n) are E-linearly independent, and the λ-functions take values in E and are defined by the equation $$a_0 = \sum\limits_{i=1}^n \lambda_n^i(a_0, a_1\ldots,a_n) \, a_i,$$ if K ⊨ Dep_(n)(a₁,…,a_(n)) ∧ ¬Dep_(n + 1)(a₀,a₁,…,a_(n)), and are 0 otherwise. Clearly, a field A is closed under the λ-functions if and only if it is linearly disjoint from E over E_(A), that is, if it is P-special, as in Definition Definition 7. Note that the fraction field of an ℒ_(D)-substructure is again closed under λ-functions and thus it is tame. The theory ACFP has therefore quantifier elimination [@fD12] in the language ℒ_(D). Note that the formula P(x) is equivalent to Dep₂(1,x). Likewise, the predicate Dep_(n) is is equivalent to λ_(n)¹(a₁,a₁…,a_(n)) = 1. Since the definable closure of a set is P-special, we conclude the following result by Lemma Lemma 8. Corollary 39. Given two subfields A and B of K containing an ℒ_(p)-elementary substructure M of K such that $A\mathop{\mathpalette\Ind{}}^P_M B$, then the fields E ⋅ A and E ⋅ B are linearly disjoint over E ⋅ M. Our candidates for the equations in the theory ACFP will be called tame formulae. Definition 40. Let x be a tuple of variables. A formula φ(x) in the language ℒ_(P) is tame if there are polynomials q₁, …, q_(m) in ℤ[X,Z], homogeneous in the variables Z, such that φ(x)  =  ∃ ζ ∈ P^(r)(¬ζ ≐ 0 ∧ ⋀_(j ≤ m)q_(j)(x,ζ) ≐ 0). Lemma 41. Let q₁, …, q_(m) ∈ ℤ[X,Y,Z] be polynomials, homogeneous in the variables Y and Z separately. The ℒ_(P)-formula $$\exists\, \upsilon \in P^r\; \exists \zeta \in P^s\Bigl(\neg\upsilon\doteq 0\; \land\; \neg\zeta\doteq 0\;\land\;\bigwedge_{k\leq m} q_k(x,\upsilon,\zeta)\doteq 0 \Bigr)$$ is equivalent in ACFP to a tame formula. Proof. With the notation $\xi_{\ast,j}=\xi_{1,j},\dotsc,\xi_{r,j}$ and $\xi_{i,\ast}=\xi_{i,1},\dotsc,\xi_{i,s}$, the previous formula is equivalent in ACFP to the tame formula $$\exists (\xi_{1,1},\dotsc,\xi_{rs})\in P^{r,s}\setminus 0 \bigwedge_{i,j,k=1}^{r,s,m}q_k(x,\xi_{*,j},\xi_{i,*})\doteq0.$$  ◻ Corollary 42. The collection of tame formulae is closed under conjunctions and disjunctions. In order to prove that tame formulae determine the type in ACFP, we need a short observation regarding the E-annihilator of a (possibly infinite) tuple. Fix some enumeration $\left(M_i(x_1,\dotsc,x_s)\right)_{i=1,2,\ldots}$ of all monomials in s variables. Given a tuple a of length s, denote $$\operatorname{Ann}_n(a) =\biggl\{(\lambda_1,\ldots,\lambda_n) \in \mathit{E}^n\; \biggm | \;\sum\limits_{i=1}^n \lambda_i\cdot M_i(a) =0\biggr \}.$$ Notation 2. If we denote by x ⋅ y the scalar multiplication of two tuples x and y of length n, that is $$x\cdot y= \sum\limits_{i=1}^n x_i\cdot y_i,$$ then Ann_(n)(a) = {λ ∈ E^(n) ∣ λ ⋅ (M₁(a),…,M_(n)(a)) = 0}. Lemma 43. Two tuples a and b of K have the same type if and only if ldim_(E)Ann_(n)(a) = ldim_(E)Ann_(n)(b) and the type tp (Pk(Ann_(n)(a))) equals tp (Pk(Ann_(n)(a))) (in the pure field language), for every n in ℕ. Proof. We need only prove the right-to-left implication. Since Pk (Ann_(i)(a)) is determined by Pk (Ann_(n)(a)), for i ≤ n, we obtain an automorphism of E mapping Pk (Ann_(n)(a)) to Pk (Ann_(n)(b)) for all n. This automorphism maps Ann_(n)(a) to Ann_(n)(b) for all n and hence extends to an isomorphism of the rings E[a] and E[b]. It clearly extends to a field isomorphism of the tame subfields E(a) and E(b) of K, which in turn can be extended to an automorphism of (K,E). So a and b have the same ACFP-type, as required. ◻ Proposition 44. Two tuples a and b of K have the same ACFP-type if and only if they satisfy the same tame formulae. Proof. Let q₁(Z), …, q_(m)(Z) be homogeneous polynomials over ℤ. By Lemma Lemma 43, it suffices to show that   Ann_(n)(x) has a k-dimensional subspace V such that ⋀_(j ≤ m)q_(j)(Pk(V)) = 0 is expressible by a tame formula. Indeed, it suffices to guarantee that there is an element ζ in Gr_(k)(E^(n)) such that (e⌟ζ) ⋅ (M₁(x),…,M_(n)(x)) = 0 for all e from a a fixed basis of $\@ifnextchar^\@extp{\mathop{\bigwedge\nolimits^{\!\,}}}^{k-1} (E^n)^*$, and ⋀_(j ≤ m)q_(j)(ζ) = 0. In particular, the tuple ζ is not trivial, so we conclude that the above is a tame formula. ◻ By compactness, we conclude the following: Corollary 45. In the (incomplete) theory ACFP of proper pairs of algebraically closed fields, every formula is a Boolean combination of tame formulae. Equationality of belles paires of algebraically closed fields In order to show that the stable theory ACFP of proper pairs of algebraically closed fields is equational, we need only consider tame formulae with respect to some partition of the variables, by Corollary Corollary 45. As before, work inside a sufficiently saturated model (K,E) of ACFP in the language ℒ_(P) = ℒ_(rings) ∪ {P}, where E = P(K) is the proper subfield. Consider the following special case as an auxiliary result. Lemma 46. Let φ(x;y) be a tame formula. The formula φ(x;y) ∧ x ∈ P is an equation. Proof. Let b be a tuple in K of length |y|, and suppose that the formula φ(x,b) has the form φ(x,b)  =  ∃ ζ ∈ P^(r)(¬ζ ≐ 0 ∧ ⋀_(j ≤ m)q_(j)(x,b,ζ) ≐ 0). for some polynomials q₁, …, q_(m) with integer coefficients and homogeneous in ζ. Express each of the monomials in b appearing in the above equation as a linear combination of a basis of K over E. We see that there are polynomials r₁, …, r_(s) with coefficients in E, homogeneous in ζ, such that the formula φ(x,b) ∧ x ∈ P is equivalent to ∃ ζ ∈ P^(r) (¬ζ ≐ 0 ∧ ⋀_(j ≤ s)r_(j)(x,ζ) ≐ 0). Working inside the algebraically closed subfield E, the expression inside the brackets is a projective variety, which is hence complete. By Remark Remark 13, its projection is again Zariski-closed, as desired. ◻ Proposition 47. Let φ(x;y) be a tame formula. The formula φ(x;y) is an equation. Proof. We need only show that every instance φ(a,y) of a tame formula is indiscernibly closed. By Lemma Lemma 3, it suffices to consider a Morley sequence (b_(i))_(i ≤ ω) over an elementary substructure M of (K,E) with $$a\mathop{\mathpalette\Ind{}}^P_M b_i \text{ with } \models \varphi(a,b_i) \text{ for } i <\omega.$$ Suppose that the formula φ(a,y) has the form φ(a,y)  =  ∃ ζ ∈ P^(r)(¬ζ ≐ 0 ∧ ⋀_(j ≤ m)q_(j)(a,y,ζ) ≐ 0), for polynomials q₁, …, q_(n) with integer coefficients and homogeneous in ζ. By Corollary Corollary 39, the fields E ⋅ M(a) and E ⋅ M(b_(i)) are linearly disjoint over E(M) for every i < ω. A basis (c_(ν)) of E ⋅ M(a) over E ⋅ M remains thus linearly independent over E ⋅ M(b_(i)). By appropriately writing each monomial in a in terms of the basis (c_(ν)), and after multiplication with a common denominator, we have that φ(a,y)  =  ∃ ζ ∈ P^(r)(¬ζ ≐ 0 ∧ ⋀_(ν)r_(ν)(e,m,y,ζ) ⋅ c_(ν) ≐ 0), where e a tuple from E and m is a tuple from M, and the polynomials r_(ν)(X,Y′,Y,Z) are homogeneous in Z. Hence, linearly disjointness implies that K⊨  ∃ ζ ∈ P^(r)(¬ζ ≐ 0 ∧ ⋀_(ν)r_(ν)(e,m,b_(i),ζ) ≐ 0) for i < ω. By Lemma Lemma 46, the formula φ′(e,y′,y) = ∃ ζ ∈ P^(r)(¬ζ ≐ 0 ∧ ⋀_(ν)r_(ν)(e,y′,y,ζ) ≐ 0) is indiscernibly closed. Since the sequence (m,b_(i))_(i ≤ ω) is indiscernible, we have K ⊨ φ′(e,m,b_(ω)), so K ⊨ φ(a,b_(ω)), as desired. ◻ Corollary Corollary 45 and Proposition Proposition 47 yield now the equationality of ACFP. Theorem 48. The theory of proper pairs of algebraically closed fields of a fixed characteristic is equational. Encore! An alternative proof of equationality for pairs in characteristic 0 We will exhibit an alternative proof to the equationality of the theory T_(p) of belles paires of algebraically closed fields in characteristic 0, by means of differential algebra, based on an idea of Günaydın [@aG16]. Definition 49. Consider an arbitrary field K with a subfield E. A subspace of the vector space K^(n) is E-defined if it is generated by vectors from E^(n). Since the intersection of two E-defined subspaces is again E-defined, every subset A of K is contained in a smallest E-defined subspace A^(E), which we call the E-hull of A. Notation 3. We write v^(E) to denote {v}^(E). Clearly A^(E) is the sum of all v^(E) for v in A. The E-hull v^(E) can be computed as follows: Fix a basis (c_(ν)∣ν∈N) of K over E and write v = ∑_(ν ∈ N)c_(ν)e_(ν) for vectors e_(ν) ∈ E^(n). Then {e_(ν) ∣ ν ∈ N} is a generating set of v^(E). Similarly, every subset A of the ring of polynomials $K[X_1,\dotsc,X_n]$ has an E-hull A^(E), that is, the smallest E-defined subspace of $K[X_1,\dotsc,X_n]$. Lemma 50. Let I be an ideal of $K[X_1,\dotsc,X_n]$. Then I^(E) is the smallest ideal containing I and generated by elements of $E[X_1,\dotsc,X_n]$. Proof. An ideal J generated by the polynomials f_(i) in $E[X_1,\dotsc,X_n]$ is generated, as a vector space, by the products X_(j)f_(i). Conversely, for each variable X_(j), the vector space {f ∣ X_(j)f ∈ I^(E)} is E-defined and contains I. Thus it contains I^(E), so I^(E) is an ideal. ◻ If the ideal I is generated by polynomials f_(i), then the union of all f_(i)^(E) generates the ideal I^(E). Note also that, if I is homogeneous, i.e. it is the sum of all I_(d) = {f ∈ I ∣ h homogeneous of degree d}, then so is I^(E), with (I^(E))_(d) = (I_(d))^(E). From now on, consider a sufficiently saturated algebraically closed differential field (K,δ), equipped with a non-trivial derivation δ. Denote its field of constants C_(K) by E. For example, we may choose (K,δ) to be a saturated model of DCF₀, the elementary theory of differential closed fields of characteristic zero. Observe that the pair (K,E) is a model of the theory ACFP₀ of proper extensions of algebraically closed fields in characteristic 0. In order to show that this theory is equational, it suffices to show, by Proposition Proposition 44, that every instance of a tame formula determines a Kolchin-closed set in (K,δ). We first need some auxiliary lemmata on the differential ideal associated to a system of polynomial equations. Lemma 51. Let v be a vector in K^(n). Then the E-hull of v is generated by v, δ(v), …, δ^(n − 1)(v). Proof. Any E-defined subspace is clearly closed under δ. Thus, we need only show the the subspace V generated by v, δ(v), …, δ^(n − 1)(v) is E-defined. Let k ≤ n be minimal such that v can be written as $$v = a_1 e_1+\dotsb+a_ke_k$$ for some elements a_(i) in K and vectors e_(i) in E^(n). Thus, the e_(i)’s are linearly independent and generate v^(E). Hence V ⊂ v^(E). If the dimension of V is strictly smaller than k, then v, δ(v), …, δ^(k − 1)(v) are linearly dependent over K. The rows of the matrix $$\begin{pmatrix} a_1 & a_2 & \ldots & a_k \\ \delta(a_1) & \delta(a_2) & \ldots & \delta(a_k) \\ \vdots & & \vdots & \\ \delta^{k-1}(a_1) & \delta^{k-1}(a_2) & \ldots & \delta^{k-1}(a_k) \end{pmatrix}$$ are thus linearly dependent over K. It follows from Fact Fact 11 that a₁, …, a_(k) are linearly dependent over E. So there are ξ_(i) in E, not all zero, such that $\xi_1a_1+\dotsb+\xi_ka_k=0$. The vector space $$\Bigl\{ \sum_{i=1}^kb_ie_i \Bigm| \sum_{i=1}^k\xi_ib_i=0\Bigr\},$$ which contains v, has a basis from E^(n) and dimension strictly smaller than k, contradicting the choice of the e_(i)’s. ◻ In order to apply the previous result, consider the derivation D on the polynomial ring K[X₁,…,X_(n)] obtained by differentiating the coefficients of a polynomial in K (and setting D(X_(i)) = 0, for 1 ≤ i ≤ n). We say that an ideal I of K[X₁,…,X_(n)] is differential if it is closed under D. Corollary 52. An ideal of K[X] is differential if and only if it can be generated by elements from E[X]. Corollary 53. Given homogeneous polynomials h₀, …, h_(m) in K[X] of a fixed degree d, there exists an integer k in ℕ (bounded only in terms of d and the length of X) such that the ideal generated by $\{D^{j}(h_i)\}_{\substack{i\leq m \\ j < k}}$ is a differential and homogeneous ideal. We now have all the ingredients in order to show that tame formulae are equations. Proposition 54. Let φ(x,y) be a tame formula. The definable set φ(x,b) is Kolchin-closed set in (K,δ). Proof. Suppose that φ(x,b)  =  ∃ ζ ∈ P^(r)(¬ζ ≐ 0 ∧ ⋀_(i ≤ m)q_(i)(x,ζ) ≐ 0), for polynomials q_(j)(X,Z) over K homogeneous in Z of some fixed degree d. Let k be as in Corollary Corollary 53. For a tuple a in K of length |x|, write D^(j)(q_(i)(a,Z)) = q_(i, j)(a,…,δ^(j)(a),Z), for polynomials q_(i, j)(X₀,…,X_(k),Z) over K, homogeneous in Z. By Corollary Corollary 53, the ideal I(a,Z) generated by $$\{q_{i,j}(a,\dots,\delta^j(a), Z)\}_{\substack{i< m \\ j