Fields Institute Communications Volume 00, 0000

On the Decidability of the Existential Theory of 𝔽_{p}[[t]]

Jan Denef

Department of Mathematics Catholic University of Leuven Celestijnenlaan 200B B-3001 Leuven (Belgium)

                             Jan.Denef@wis.kuleuven.ac.be

http://www.wis.kuleuven.ac.be/wis/algebra/denef.html

Hans Schoutens

Department of Mathematics Ohio State University Columbus, OH 43210 (USA)

                            schoutens@math.ohio-state.edu

http://www.math.ohio-state.edu/˜ schoutens

Abstract. We show how Resolution of Singularities in characteristic p implies the decidability of the existential theory of 𝔽_{p}[[t]] in the language of discrete valuation rings, where t is a single variable and 𝔽_{p} the pelement field.

1 Introduction

The aim of this paper is to study the ring 𝔽_{p}[[t]], where t is a single variable and 𝔽_{p} the p-element field. Note that this is an equicharacteristic complete, whence Henselian, discrete valuation ring with maximal ideal generated by t and residue field 𝔽_{p}. Hence, from an algebraic point of view this is a very well understood ring. However, from a model-theoretic point of view, it is poorly understood. This is in spite of the analogies, made evident by the work [3] of Ax en Kochen, between 𝔽_{p}[[t]] and the ring of p-adic integers. For instance, a complete recursive axiom system for the theory of 𝔽_{p}[[t]] is still unknown. For many purposes, it is an equivalent problem to understand the theory of the field 𝔽_{p}((t)) as a valued field (where the valuation is the t-adic one). Indeed, in general, if (K, v) denotes a valued field, with which we mean a field K with a valuation v on it, and if R denotes its valuation ring, then R is obviously definable in K (in the language of valued fields), and, conversely, for a, b ∈ R, we have that v(a) ≤ v(b) if, and only if, there exists c ∈ R with b = ca.

\begin{matrix}c \\ ◯ \end{matrix}0000 American Mathematical Society

1991 Mathematics Subject Classification. 13L05, 12L05.

In [14] it is pointed out that the following ”obvious” candidate for an axiom system for the field K = 𝔽_{p}((t)) with its natural valuation v, derived by analogy from the axiom system for the p-adics, is not complete.

• The valued field (K, v) is Henselian and defectless.

• The characteristic of K is p.

• The value group of v is a ℤ-group.

• The residue field is 𝔽_{p}.

Note that the condition that K be defectless is superfluous for fields of characteristic zero, but in positive characteristic Henselian discretely valued fields with defect exist (that is to say, fields which admit a finite extension in which the fundamental equality fails). In [14], Kuhlmann proposes some additional axioms involving additive polynomials, but the resulting system is still not known to be complete.

As an immediate consequence of the existence of a complete recursive axiom system, we would get that the theory of 𝔽_{p}[[t]] is decidable. In this paper we will explain how the decidability of the existential theory of 𝔽_{p}[[t]] in the language of discrete valuation rings follows from Resolution of Singularities. More precisely, let L^{DVR} be the language of rings with a single constant symbol π π π added. Let R be a discrete valuation ring with uniformizing parameter π (that is to say, the maximal ideal of R is πR). We view R as an L^{DVR}-structure by interpreting π π π as the uniformizing parameter π. Let R_{0} be the subring of R generated by π, then every term in L^{DVR} names an element of R_{0} and conversely. For instance, in case R = 𝔽_{p}[[t]] (with uniformizing parameter t) then R_{0} = 𝔽_{p}[t]. Note that in the language L^{DVR}, both formulae v(a) ≤ v(b) and v(a) < v(b) are existentially definable, by requiring that there exists c ∈ R with b = ca, respectively b = caπ. Therefore, our results on the decidability of the existential theory of R, also hold when we add a symbol for the valuation to the language.

Our main result is that, assuming Resolution of Singularities, there exists an algorithm which decides, for an arbitrary system of equations f_{1}(ξ) = ⋯ = f_{m}(ξ) = 0 and an inequation f_{0}(ξ) ≠ 0, with f_{i} ∈ 𝔽_{p}[t, ξ] and ξ a finite set of variables, whether this system has a solution in 𝔽_{p}[[t]]. In fact, we will prove this for a larger class of discrete valuation rings; see Theorem 4.3. Unfortunately, Resolution of Singularities (in the form we need it; see Theorem 1 below for the precise content) is still conjectural in positive characteristic. The weaker version of De Jong, which uses finite-to-one maps instead of birational maps, appears to be not strong enough to carry out the present method of proof. What follows is a brief description of our method.

On the Decidability of the Existential Theory of 𝔽_{p}[[t]] 3

As an immediate corollary of a theorem of Greenberg in [10], a system of polynomial equations in a finite number of variables ξ over an excellent discrete valuation ring R has a solution, if it has a solution modulo arbitrary high powers of the maximal ideal. This was generalized by Artin in [2] to Henselian local rings of the form R = κ[[t]] or R = κ[[t]]^{alg} (the ring of algebraic power series), where t is now a finite set of variables and κ is a field. Moreover, he obtains the following effective version for systems of equations with polynomial coefficients. If f_{i} ∈ κ[t, ξ], then to find a solution of the system f_{1}(ξ) = ⋯ = f_{m}(ξ) = 0 over R, it suffices to find an approximate solution modulo the N-th power of the maximal ideal, where N depends only on the total degree d of the f_{i} and the number of variables t and ξ. This result is now commonly known as Strong Artin Approximation. Using nonstandard methods, the first author et al., have shown in [4] that N depends even in a computable (recursive) way on d and the number of variables. For systems of equations with more general coefficients, see [6].

Moreover, Artin conjectured Strong Artin Approximation to be true for any excellent Henselian local ring. The status of this Conjecture has been unclear for a while, but now several proofs have been put forward, see for instance [22] or [18] (and the commentaries provided by Swan in an alas unpublished paper [23]). For our purposes (but not for the main case of interest, namely when R = 𝔽_{p}[[t]]), we need a Strong Artin Approximation theorem which includes parameters (Theorem 3.1). This theorem follows from these general results together with some structure theorems for complete Noetherian local rings.

In this paper we exhibit an algorithm that verifies whether a system of equations together with some inequations over R_{0} has a solution over an equicharacteristic Henselian discrete valuation ring R, at least relative to the residue field κ of R. (As before R_{0} is the subring generated by some uniformizing parameter). Relative to the residue field means that this algorithm will use the theory of κ as an oracle. In fact, the algorithm will reduce the problem to finding a solution of some (effectively constructible) system of equations and inequations over the residue field κ. Since the theory of any finite or any algebraically closed field is decidable, this will yield the decidability of the existential theory of any equicharacteristic Henselian discrete valuation ring R with a finite or algebraically closed residue field. Unfortunately, this result depends on the validity of Resolution of Singularities. This is known in characteristic zero, but still conjectural for positive characteristic. In particular, we do get a positive result for instance for the rings ℂ[[t]] and ℂ[[t]]^{alg}, where t is a single variable, but only a conjectural result for the rings F_{p}[[t]]. It should be noted, however, that the results over ℂ also follow from the work of Ax-Kochen-Ershov ([3] and [7, 8, 9]).

Sketch of the Algorithm. What follows is a brief sketch of the strategy in the main case that R = 𝔽_{p}[[t]]. Let there be given an open W in a closed subscheme X of 𝔸_{R}^{n}, both defined over R_{0} = 𝔽_{p}[t]. We describe an algorithm that decides whether or not W admits an R-rational point (that is to say, a solution over R of the system of equations and inequations that define W; this will be explained in more detail in 2.1). To simplify the argument, let us moreover assume that X is irreducible and reduced. (In general, we will only be allowed to assume that the generic fibre X_{K} =: X ×_{Spec R} Spec K is reduced, using Lemma 4.2.) If W = X, then using an effective version of Greenberg’s result ([4, Theorem 3.2], or in the more general case, Theorem 3.1 below), we can reduce the problem of finding an R-rational point on X to a similar problem over 𝔽_{p}, so that this particular instance is decidable, as already explained. Next we show that if the generic fibre of X has no singularities, then either X admits no R-rational points at all or the R-rational points are dense on X (see Theorem 2.4 below for an exact statement; the proof rests on some form of Néron Desingularization). Therefore, in the non-singular case, we reduced the problem of finding an R-rational point on W, to finding an R-rational point on X, and we know already how to deal with this. Finally, if the generic fibre X_{K} of X has singularities, and under the assumption that Resolution of Singularities for X_{K} holds, we can (effectively) find a proper, birational morphism h: V → X_{K} of schemes of finite type over K with V non-singular. We then ’clear denominators’ to define a scheme Y over R with generic fibre equal to V and a proper birational morphism f: Y → X which specializes to h after base change. Outside a nowhere closed subset Z of X, the morphism f is an isomorphism (defined over R). Since f is proper, there is therefore a one-one correspondence between R-rational points on f^{−1}(W) − f^{−1}(Z) and W − Z, by the Valuative Criterium for Properness. Since the generic fibre of Y is non-singular, we are back in the previous case. Finally, on Z we get by with an inductive argument on the dimension.

The above proof collapses for arbitrary (excellent) Henselian local rings R, since the Valuative Criterion for Properness fails for higher-dimensional local rings, so that R-rationality can no longer be preserved in the way we did above. However, for a W in general position, we can describe an algorithm which does not even rely on Resolution of Singularities. This is explained in the last section, where the precise definition of general position, in terms of the non-smooth locus of the generic fibre, can be found.

Acknowledgement. The main ideas in this paper, namely the results on the decidability of the existential theory of 𝔽_{p}[[t]] modulo Resolution of Singularities, are entirely due to the first author, who had made these observations already in 1983. The second author, while taking up the task of working out the details and preparing this manuscript for publication based on notes taken by F.- V. Kuhlmann during an Oberwolfach meeting in 1999, has further generalized these results to include arbitrary excellent Henselian discrete valuation rings.

2 Smooth Rational Points

2.1 Solutions and Rational Points. Let R be a ring and X a scheme over Spec R. Let us denote the structure morphism by s: X → Spec R. With an Rrational point x on X, we mean a section x: Spec R → X of the structure morphism s, that is to say, such that s ∘ x is the identity on Spec R. If X is affine, say X = Spec A with A an R-algebra, then an R-rational point x corresponds to an Ralgebra homomorphism ϕ: A → R. In particular, if A is moreover finitely generated as an algebra over R, say A ≅ R[ξ]/(f_{1}, …, f_{t}) with ξ = (ξ_{1}, …, ξ_{m}) variables, then an R-rational point on Spec A is uniquely determined by an m-tuple r = (r_{1}, …, r_{m}) ∈ R^{m} such that f_{1}(r) = ⋯ = f_{t}(r) = 0. Namely, r_{i} is the image of (the class of) ξ_{i} under ϕ. In this terminology, we see that an R-rational point simply corresponds to a solution over R of the system of equations f_{1} = ⋯ = f_{t} = 0.

If f: Y → X is a morphism of schemes over Spec R, then we say that the Rrational point y on Y is a lifting of the R-rational point x on X, or that x admits an R-rational lifting y, if the following diagram commutes

[figure: Spec R; Y; X; f; y; x]  (1)

The collection of all R-rational points y on Y lifting x is in one-one correspondence with the collection of all R-rational points on the fibre product Y ×_{X} Spec R given by the commutative diagram

[figure: Spec R; Y ×_{X} Spec R; X; Y; x; f]  (2)

If f is a locally closed immersion defined over R (that is to say, if Y is an open inside a closed subscheme X′ of X, where both X′ and Y and the two inclusion morphisms are defined over R), then an R-rational point x on X has at most one lifting on Y, and if such a lifting exists, we simply say that x is an R-rational point on Y. Moreover, if R is local and w is the closed point of Spec R corresponding to the maximal ideal of R, then x is an R-rational point on an open Y ⊂ X if, and only if, x(w) ∈ Y. Indeed, x^{−1}(Y) is an open in Spec R, since x is continuous. The only open of Spec R containing the closed point w is Spec R itself. Therefore, the image of x is entirely inside Y, showing that x is an R-rational point on Y. In particular, it follows that each R-rational point on X is already an R-rational point on an affine open subset of X, provided that R is local.

In spite of its name, an R-rational point on X is not a point of X. However, in case R = K is a field, we can identify it with a point of X as follows. Let η be the unique point of Spec K (that is to say, the point corresponding to the prime ideal (0)). Let x be a K-rational point on X, that is to say, a morphism x: Spec K → X. We now may identify x with the point x(η) of X. In fact x(η) is a closed point of X with residue field K and each such point arises as the image of η under some K-rational point.

For R a domain, let η denote the point of Spec R corresponding to the prime ideal (0). We say that η is the generic point of Spec R. Let x be an R-rational point on X. In particular, x(η) is a point of X. If X = Spec A is affine (and by the remark above, we may always assume this provided R is moreover local), then x corresponds to an R-algebra homomorphism ϕ: A → R. Therefore x(η) corresponds to the prime ideal 𝔭 =: ϕ^{−1}(0), that is to say, to the kernel of ϕ. If R is not a field, then 𝔭 is no longer a maximal ideal, so that x(η) is not a closed point of X. Let K denote the field of fractions of R and let i: Spec K → Spec R be the morphism corresponding to the inclusion R ⊂ K. We have a base change (or fibre product) diagram

[figure: X; X_{K}; Spec R; Spec K; s; i; j]  (3)

where X_{K} denotes the fibre product X ×_{Spec R} Spec K. In the rest of this paper, we will always adopt the use of a subscript K to mean base change over i; this convention might be applied to schemes as well as to morphisms.

The scheme X_{K} is called the generic fibre of X, since it can be identified with s^{−1}(η). In particular, since s ∘ x is by assumption the identity, we see that x(η) lies in fact on s^{−1}(η) ≅ X_{K}. We denote the corresponding K-rational point of X_{K} by x_{K} and call it the underlying point of x (on X_{K}). It is simply the base change of x over j, so that we have a commutative diagram

[figure: Spec R; Spec K; X; X_{K}; x_{K}; x; j; i]  (4)

Algebraically (that is to say, in case X = Spec A is affine), x_{K} corresponds to the kernel of the base change A ⊗_{R} K → K, which is just 𝔭(A ⊗_{R} K), since R ⊂ K is flat. In conclusion, the underlying point of an R-rational point x on X, is a K-rational point x_{K} on X_{K}.

A note of caution: one would be tempted to identify x_{K} (or even x(η)) with the composition xi. However, xi: Spec K → X is not even a K-rational point, since X is in general not a scheme over Spec K (which was a necessary condition in our definition).

2.2. Proposition Let R be a discrete valuation ring with field of fractions K. Let f: Y → X be a proper morphism of Noetherian schemes over Spec R. Let x be an R-rational point on X. If the underlying point x_{K} of x admits a K-rational lifting on the generic fibre Y_{K}, then x admits an R-rational lifting on Y.

More precisely, if w is a K-rational lifting of x_{K} on Y_{K}, then we can choose an R-rational lifting y of x on Y with underlying point equal to w.

Proof This is a direct application of the Valuative Criterium for Properness as follows. Namely, let w be a K-rational point on Y_{K} lifting x_{K}. This means that w: Spec K → Y_{K} and x_{K} = f_{K} ∘ w, where f_{K}: Y_{K} → X_{K} is the base change of f.

Let us denote by y_{0} : Spec K → Y the composition of w with the base change morphism Y_{K} → Y. We therefore have a commutative diagram

[figure: Spec R; Spec K; X; Y; y_{0}; x; f; i]  (5)

By [11, Chapter II, Theorem 4.7], there exists a morphism y: Spec R → Y, such that fy = x and y_{0} = yi, which therefore defines an R-rational lifting of x, with y_{K} = w.

2.3. Definition Let R be a domain with field of fractions K. Let X be a scheme over Spec R and let x be an R-rational point on X. By abuse of terminology, we will say that x is non-singular, if the underlying point x_{K} of x is a non-singular point of X_{K}. Algebraically, in case X = Spec A is affine, this means that A_{𝔭} ⊗_{R} K is a regular local ring, where 𝔭 is the kernel of the homomorphism A → R corresponding to x.

The following theorem shows that non-singular R-rational points are locally dense. The proof uses some form of Néron Desingularization (Claim 2.5).

2.4. Theorem Let (R, 𝔪) be an Henselian local domain with fraction field K. Let X be a scheme of finite type over Spec R. If X admits a non-singular R-rational point x, then there exists an open X′ of X, defined over R and admitting x as an R-rational point, with the following property. Every open W of X′ which is defined over R, admits at least one R-rational point. (We’ll simply say that the R-rational points are dense in a neighbourhood X′ of the non-singular point x).

Proof We may assume that X = Spec A is affine, since R is local (see the remark near the end of the second paragraph in 2.1). Let 𝔭 be the kernel of the R-algebra homomorphism A → R corresponding to x. Let A_{K} = A ⊗_{R} K, so that the generic fibre X_{K} of X is isomorphic to Spec A_{K}. Hence 𝔭A_{K} is the maximal ideal corresponding to the underlying point x_{K} of x and we will still write 𝔭 for its image in A_{K}.

Since by assumption (A_{K})_{𝔭} is regular, we can find a regular system of parameters (t_{1}, …, t_{h}) for (A_{K})_{𝔭}, with t_{i} ∈ A. Note that this simply means that (t_{1}, …, t_{h})(A_{K})_{𝔭} = 𝔭(A_{K})_{𝔭} where h is the dimension of (A_{K})_{𝔭}. Consider the K-algebra homomorphism

ψ: K[ξ] → A_{K}  (6)

given by sending ξ_{i} to t_{i}, where ξ = (ξ_{1}, …, ξ_{h}) are variables. Let 𝔫 denote the maximal ideal in K[ξ] generated by the ξ_{i}, so that

(A_{K})_{𝔭}/𝔫(A_{K})_{𝔭} = (A_{K})_{𝔭}/𝔭(A_{K})_{𝔭} = K.  (7)

Note that (ξ_{1}, …, ξ_{h}) is a regular sequence in K[ξ]_{𝔫} mapped bijectively by ψ onto the regular sequence (t_{1}, …, t_{h}) in (A_{K})_{𝔭}. By the Local Flatness Criterion [16, Theorem 22.3], we get that K[ξ]_{𝔫} → (A_{K})_{𝔭} is flat. Equation (7) shows that K[ξ]_{𝔫} → (A_{K})_{𝔭} is also unramified (note that both local rings have residue field K). Therefore ψ is etale at 𝔭; see for instance [17, Chapter I.§3] or [19, Chapitre V] for definitions. In other words, ψ induces a morphism f: X_{K} → 𝔸_{K}^{h} which is etale at x_{K}. Note that this implies in particular that X_{K} is smooth over K in the point x_{K}.

After a translation, since x is R-rational, we might as well have taken x so that x_{K} lies over the origin in 𝔸_{K}^{h} (identified with the n-tuple 0). By [17, Corollary 3.16], we can write A_{K} as

A_{K} ≅ K[ξ, ζ]/(f_{1}, …, f_{N})  (8)

with ξ = (ξ_{1}, …, ξ_{h}) and ζ = (ζ_{1}, …, ζ_{N}) variables, and where h is the dimension of X_{K} and f_{j} ∈ R[ξ, ζ] are polynomials without constant term, such that the Jacobian Criterion holds in the point (0, 0) with respect to the ζ-variables. This means that the determinant d of

\frac{∂(f_{1}, …, f_{N})}{∂(ζ_{1}, …, ζ_{N})} =: (\begin{matrix}∂f_{1}/∂ζ_{1} & ∂f_{1}/∂ζ_{2} & … & ∂f_{1}/∂ζ_{N} \\ ∂f_{2}/∂ζ_{1} & ∂f_{2}/∂ζ_{2} & … & ∂f_{2}/∂ζ_{N} \\ ⋮ & ⋮ & ... & ⋮ \\ ∂f_{N}/∂ζ_{1} & ∂f_{N}/∂ζ_{2} & … & ∂f_{N}/∂ζ_{N} \end{matrix} )  (9)

is non-zero when evaluated at (0, 0). Let d_{0} = d(0, 0) be this non-zero element. Note that d_{0} ∈ R.

Set

B =: R[ξ, ζ]/(f_{1}, …, f_{N})  (10)

and let Y be the affine scheme Spec B. By construction, X_{K} = Y_{K}, so that we can find an open W of X which is defined over R and admits x as an R-rational point, and an open V of Y, defined over R, such that W ≅ V (as schemes over Spec R). Moreover, we can find an R-rational point y on V with underlying point equal to x_{K}. Therefore R-rational points are dense on X in a neighbourhood of x if, and only if, they are dense on Y in a neighbourhood of y (in the terminology introduced in the statement), so that we may as well assume that Y = X.

We define an R-algebra endomorphism σ on R[ξ, ζ] by letting

\begin{cases}ξ_{j} & ↦ d_{0}^{2}ξ_{j} \\ ζ_{j} & ↦ d_{0}ζ_{j}. \end{cases}  (11)

Let f_{i}^{σ}(ξ, ζ) denote the image of f_{i} under σ. If r = (s_{1}, …, s_{h}, t_{1}, …, t_{N}) ∈ R^{h+N} is an R-rational solution of f^{σ} = 0, then (d_{0}^{2}s_{1}, …, d_{0}^{2}s_{h}, d_{0}t_{1}, …, d_{0}t_{N}) is an Rrational solution of f = 0. In particular, if the R-rational points are dense on the variety X^{σ} defined by f^{σ}, then so are the R-rational points on X.

2.5. Claim There exist g_{i} ∈ R[ξ, ζ], for i = 1, …, N, such that the variety over R defined by the g_{i} is X^{σ}, and, moreover, the determinant of \frac{∂(g_{1},...,g_{N})}{∂(ζ_{1},...,ζ_{N})} eval-

uated at (0, 0), equals 1, where \frac{∂(g_{1},...,g_{N})}{∂(ζ_{1},...,ζ_{N})} is defined as in (9) with the g_{i} instead of the f_{i}.

Assuming the claim, we therefore may assume upon replacing X by X^{σ}, that d(0, 0) = d_{0} = 1. Let 𝔪 denote the maximal ideal of R. Let W be a non-zero open subset of X, defined over R. We need to show that W admits an R-rational point. Without loss of generality, we may assume that W is the complement of the hypersurface defined by some f_{0} ∈ R[ξ, ζ]. Since W is non-empty, the ideal (f_{0}, …, f_{N}) has height at least N + 1 in K[ξ, ζ]. By taking generic hyperplanes, we can find a_{i} ∈ 𝔪, for i = 1, …, h − 1, such that the ideal

(f_{0}, …, f_{N}, ξ_{1} − a_{1}, …, ξ_{h−1} − a_{h−1})  (12)

has height h + N in K[ξ, ζ], whence has only finitely many solutions (over the algebraic closure of K). Therefore, we can choose a_{h} ∈ 𝔪, so that

(f_{0}, …, f_{N}, ξ_{1} − a_{1}, …, ξ_{h} − a_{h})K[ξ, ζ]  (13)

is the unit ideal of K[ξ, ζ].

Set F_{i}(ζ) = f_{i}(a_{1}, …, a_{h}, ζ), for i = 0, …, N, so that F_{i} ∈ R[ζ]. Write f for (f_{1}, …, f_{N}) and F for (F_{1}, …, F_{N}). Using (13), we get that

(F_{0}, …, F_{N})K[ζ] = (1)  (14)

Since f(0, 0) = 0 and a_{i} ∈ 𝔪, we get that F (0) ≡ 0 mod 𝔪. Moreover, since d(0, 0) = 1, we get that the determinant of \frac{∂(F_{1},...,F_{N})}{∂(ζ_{1},...,ζ_{N})} is a unit in R when evaluated at 0. Since R is Henselian, we can find t = (t_{1}, …, t_{N}) ∈ R^{N}, such that F (t) = 0. By (14), we must have that F_{0}(t) ≠ 0. In other words, if we let r = (a_{1}, …, a_{h}, t), then r defines an R-rational point on W, as required.

So remains to prove our Claim 2.5. Let us write J for \frac{∂(f_{1},...,f_{N})}{∂(ζ_{1},...,ζ_{N})} as defined in (9). Taylor expansion at (0, 0) of f gives (in matrix notation)

f = ζJ + p(ξ) + q(ξ, ζ)  (15)

with p_{i} linear forms in the variables ξ and with q_{i} ∈ (ξ, ζ)^{2}R[ξ, ζ], where we have written p = (p_{1}, …, p_{N}) and q = (q_{1}, …, q_{N}).

Let H be the adjoint matrix of J, so that H has also its entries in R and, moreover, we have that

HJ = JH = dE_{N}  (16)

where E_{N} denotes the (N ×N)-identity matrix. Applying H to equation (15) yields

fH = dζ + p′(ξ) + q′(ξ, ζ)  (17)

with the linear forms p′_{i} in the ξ-variables and the polynomials q′_{i} ∈ (ξ, ζ)^{2}R[ξ, ζ] the respective entries of the N-tuples p′ and q′. Let σ denote the change of variables (11). We will use in general a superscript σ to denote the image of an element or a matrix under σ. Hence applying σ to Equation (17) gives

f^{σ}H^{σ} = d^{σ}d_{0}ζ + d_{0}^{2}p′′(ξ) + d_{0}^{2}q′′(ξ, ζ)  (18)

with the linear forms p′′_{i} in the variables ξ and the polynomials q′′_{i} ∈ (ξ, ζ)^{2}R[ξ, ζ] the entries of p′′ and q′′ respectively. Since d^{σ}(0, 0) = d(0, 0) = d_{0}, we have in fact that

f^{σ}H^{σ} = d_{0}^{2}[ζ + p′′′(ξ) + q′′′(ξ, ζ)]  (19)

with the linear forms p′′′_{i} in the ξ-variables and the polynomials q′′′_{i} ∈ (ξ, ζ)^{2}R[ξ, ζ] the entries of p′′′ and q′′′ respectively. Put

g = ζ + p′′′(ξ) + q′′′(ξ, ζ),  (20)

so that f^{σ}H^{σ} = d_{0}^{2}g, by (19). In particular, g defines the same variety X^{σ} as f^{σ}. Moreover, the determinant of \frac{∂(g_{1},...,g_{N})}{∂(ζ_{1},...,ζ_{N})} evaluated at (0, 0) is 1, as required.

3 The Positive Existential Theory

The following theorem generalizes [4, Theorem 3.2] in that we allow now also parameters. Nonetheless, the (non-standard) method of proof is the same, in the main case that R is a power series ring over a field, but instead of using Artin’s original result [2, Theorem 1.10], we need the general solution of the Artin Conjecture due to [22] or [18].

3.1. Theorem (Strong Artin Approximation with Parameters) Let (R, 𝔪) be an equicharacteristic excellent Henselian local ring. Let u be a k-tuple (of parameters) over R. There exists a function N_{R,u} : ℕ^{2} → ℕ, only depending on R and on u, with the following property. Let f_{i}(U, ξ), for i = 1, …, t, be polynomials of degree at most d in the k variables U and the m variables ξ over ℤ. If there exists an m-tuple r ∈ R^{m} such that all f_{i}(u, r) ≡ 0 mod 𝔪^{N}, with N = N_{R,u}(d, m), then there exists s ∈ R^{m}, such that all f_{i}(u, s) = 0.

Proof Let f_{i} ∈ ℤ[U, ξ] be of degree at most d ≥ 2, for i = 1, …, t with U = (U_{1}, …, U_{k}) and ξ = (ξ_{1}, …, ξ_{m}) variables, where the U will play the role of parameter variables and the ξ of indeterminates. We first reduce to the case that R is complete, as follows. Let R be arbitrary and assume the theorem proven for equicharacteristic complete Noetherian local rings. Let R̂ be the completion of R (with respect to the 𝔪-adic topology). By the result [22] or [18] (see also [23]), the pair R ⊂ R̂ has Artin Approximation. In model-theoretic terms, this simply means that R is existentially closed in R̂. Algebraically, this means that any polynomial system of equations over R is solvable over R, if it is already solvable over R̂. We claim that we can simply take N_{R̂,u} for the function N_{R,u}. Indeed, let N = N_{R̂,u}(d, m) and suppose r ∈ R^{m} satisfies that all f_{i}(u, r) ≡ 0 mod 𝔪^{N}. Since this remains true in R̂, we get by assumption that there exists r̂ ∈ R̂^{m}, such that all f_{i}(u, r̂) = 0. Using Artin Approximation to the system of equations f_{i}(u, ξ) = 0, we therefore can find r̃ ∈ R^{m}, with all f_{i}(u, r̃) = 0.

Therefore, we may moreover assume that R is complete. Next we show that if the theorem holds for R, then it also holds for any homomorphic image of R. Indeed, assume that N_{R,u} has been shown to exist for R and all tuples u. Let 𝔞 = (v_{1}, …, v_{l}) be an ideal of R. Set R̄ = R/𝔞 and let u be a k-tuple over R. Let r ∈ R^{m} and assume that f_{i}(u, r) ≡ 0 mod 𝔪^{M} R̄, for some M ∈ ℕ (to be determined later). Hence there exists a_{ij} ∈ R, such that

f_{i}(u, r) ≡ ∑_{j=1}^{l} a_{ij}v_{j} mod 𝔪^{M}  (21)

in R, for all i = 1, …, t. Put

F_{i}(U, V, ξ, ζ) = f_{i}(U, ξ) − ∑_{j=1}^{l} ζ_{ij}V_{j}  (22)

for all i = 1, …, t, so that F_{i} is a polynomial over ℤ in the variables U, V = (V_{1}, …, V_{l}), ξ and ζ = (ζ_{ij}). Note that F_{i} has again degree at most d. Set a = (a_{ij}) and v = (v_{1}, …, v_{l}), so that F_{i}(u, v, r, a) ≡ 0 mod 𝔪^{M} in R by (21). If we let M be at least N_{R,(u,v)}(d, n + lt), then we can find a tuple (s, b) ∈ R^{n+lt}, such that all F_{i}(u, v, s, b) = 0. However, this simply means that all f_{i}(u, s) = 0 in R̄, as required.

Since any complete Noetherian local ring is a quotient of a complete regular local ring by [16, Theorem 29.4], we may moreover assume by the previous argument that R is an equicharacteristic complete regular local ring. Therefore, R is isomorphic to a power series ring over a field by Cohen’s Structure Theorem [16, Theorem 28.3]. In other words, R = κ[[T]], with T = (T_{1}, …, T_{d}) a finite set of variables (where d is the dimension of R) and κ the residue field of R. We would like to apply [4, Theorem 3.2], where the existence of the required computable function is shown. However, (with notation from that paper), this result is only applicable if u_{i} ∈ κ[T], by letting F_{i}(T, ξ) = f_{i}(u, ξ) and taking N_{R,u} equal to the function β(d, m, δ, 0), where δ is the total degree of the polynomials F_{i}.

For arbitrary u, we cannot apply [4] as it stands. Instead we prove a more general result using the same (non-standard) method of proof; for more details on these non-standard techniques, we refer to [4]. Therefore, towards a contradiction, assume that no such bound as in the statement exists for the pair (d, m). This means that we can find for each c ∈ ℕ a counterexample, f_{i}^{[c]} ∈ κ[U, ξ] (we may as well take coefficients in κ) and r^{[c]} ∈ R^{m} as follows. The total degree of each f_{i}^{[c]} is at most d and

f_{i}^{[c]}(u, r^{[c]}) ≡ 0 mod 𝔪^{c}  (23)

but no solution over R to the system of equations f_{i}^{[c]}(u, ξ) = 0 exists. Let U be some non-principal ultrafilter on ℕ and let R^{[U]} and κ^{[U]} be the ultrapowers of R and κ respectively. It follows from [4, Lemma 3.4] that

R^{[U]}/𝔪^{∞}R^{[U]} ≅ κ^{[U]}[[T]],  (24)

where 𝔪^{∞}R^{[U]} is the ideal of infinitesimals, that is to say, the intersection of all 𝔪^{n}R^{[U]}. Let r^{[U]} and f_{i}^{[U]} be the image of the sequences (r^{[c]})_{c} and (f_{i}^{[c]})_{c} in R^{[U]} and κ^{[U]}[U, ξ] respectively. Just observe that since each f_{i}^{[c]} has degree at most d, so does f_{i}^{[U]}, whence it is in particular a polynomial. From (23), it follows that f_{i}^{[U]}(u, r^{[U]}) ∈ 𝔪^{∞}R^{[U]}, for all i. Therefore, by (24), each f_{i}^{[U]}(u, r^{[U]}) = 0 when viewed as an element in κ^{[U]}[[T]].

Let A denote the localization of κ^{[U]}[T, u] (the κ^{[U]}-subalgebra of κ^{[U]}[[T]] generated by u and T) at the maximal ideal 𝔪κ^{[U]}[[T]] ∩ κ^{[U]}[T, u]. Since A is locally of finite type over the field κ^{[U]}, it is an excellent ring ([15, §34]). Note that f_{i}^{[U]}(u, ξ) ∈ A[ξ]. Since κ^{[U]}[T] ⊂ A, the completion of A is κ^{[U]}[[T]]. By Artin Approximation [22] or [18] applied to the Henselization A^{∼} of A, we can find already a solution r^{∼} over A^{∼} to the system f_{i}^{[U]}(u, ξ) = 0, that is to say, so that f_{i}^{[U]}(u, r^{∼}) = 0. Since both u and κ^{[U]}[T] are contained in R^{[U]}, so is A. By the universal property of Henselizations and the fact that R^{[U]} is again Henselian by Łos’s Theorem [13, Theorem 9.5.1], there is a unique A-algebra homomorphism γ: A^{∼} → R^{[U]}. Therefore, if we put s = γ(r^{∼}), then f_{i}^{[U]}(u, s) = 0 in R^{[U]}. However, choosing some tuples s^{[c]} over R so that the image s^{[U]} of the sequence of these tuples in R^{[U]} is equal to s, we see that for almost all c, we have that f_{i}^{[c]}(u, s^{[c]}) = 0, for all i = 1, …, t, contradicting our original assumptions.

3.2. Remark The above proof in fact shows that we can prove a slightly more general result. Namely in the statement of the theorem, we may take the f_{i} to have coefficients over any subfield λ of R.

3.3. Remark Let L(u) denote the language of rings together with constant symbols denoting the entries of u. Using a similar proof as in [4, Theorem 6.1], one can show that the function N_{R,u} in the above statement can be chosen to be computable modulo the L(u)-diagram of R (see [13, p. 16] for the definition of diagram). In other words, when computing the function N_{R,u}, we are allowed to use as oracles, all equations and inequations over ℤ among the entries of u which are true in R. In particular, if the the subring of R generated by u is computable, in the sense that it admits an enumeration of its elements for which addition and multiplication are computable functions, then N_{R,u} can be chosen to be computable.

3.4. Remark We will use this Strong Artin Approximation with Parameters below to prove certain decidability results for excellent equicharacteristic discrete valuation rings. In the main case of interest, that is, when R = 𝔽_{p}[[t]], we need the above result with u equal to t, so that we can apply [4, Theorem 3.2] without reserve. In particular, in this case, the proof does not rely on the general Artin Approximation Theorem [22] or [18], but only on Artin’s result [2, Theorem 1.10].

In [21], the second author gives a proof of a mixed characteristic form of Strong Artin Approximation with Parameters, by essentially the same methods.

3.5. Proposition Let R be an equicharacteristic excellent Henselian local domain with residue field κ. Let u be a k-tuple in R. Then the positive L(u)-existential theory of R is decidable relative to the existential theory of κ and the L(u)-diagram of R.

More precisely, given a morphism of finite type f: Y → X of schemes of finite type over R, we can obtain (in a constructive way from the parameters used to describe X, Y and f) a morphism of finite type 𝔣: 𝔜 → 𝔛 of schemes of finite type over κ, such that, for each R-rational point x: Spec R → X, we can construct a κ-rational point x̄ of 𝔛 with the property that x admits an R-rational lifting on Y if, and only if, the fibre 𝔜x̄ = 𝔣^{−1}(x̄) admits a κ-rational point.

Proof Let φ be a positive L(u)-existential formula, so that it is a disjunction of statements of the form

(∃ξ)f_{1}(u, ξ) = f_{2}(u, ξ) = ⋯ = f_{t}(u, ξ) = 0  (25)

with f_{i} ∈ Z[U, ξ] and U = (U_{1}, …, U_{k}) and ξ = (ξ_{1}, …, ξ_{m}) tuples of variables. Without loss of generality we may assume that φ is one such disjunct (25). Using Strong Artin Approximation with Parameters (Theorem 3.1), we can find some N, such that φ holds if, and only if, there exists r ∈ R^{m} such that

f_{1}(u, r) ≡ f_{2}(u, r) ≡ ⋯ ≡ f_{t}(u, r) ≡ 0 mod 𝔪^{N}.  (26)

Moreover, N depends in a computable way only on the L(u)-diagram of R, on m and on the total degrees of the f_{i}. In other words, we reduced the problem, modulo the L(u)-diagram of R, to the decidability of the existential theory of R/𝔪^{N}. As R/𝔪^{N} is a finite dimensional vector space over κ, we even reduced the problem to the decidability of the existential theory of κ.

The last statement is just a translation into a more geometric language of the above algorithm. Indeed, since the problem is local, we may assume that both X and Y are affine. Since X is a closed subscheme of some affine space 𝔸_{R}^{k}, we may as well assume that X is the affine space 𝔸_{R}^{k} = Spec R[U], with U = (U_{1}, …, U_{k}) some variables. If B is the coordinate ring of Y, then B = R[U, ξ]/(f_{1}, …, f_{t}), for some polynomials f_{i} and some variables ξ = (ξ_{1}, …, ξ_{m}). Suppose f_{i} = g_{i}(u′, U, ξ) with g_{i} defined over ℤ and u′ a k′-tuple over R. Set C = ℤ[U′, U, ξ]/(g_{1}, …, g_{t}), with U′ = (U′_{1}, …, U′_{k′}) variables. Let x be an R-rational point on 𝔸_{R}^{k} given by the k-tuple u. The tuple (u′, u) then defines an R-rational point on 𝔸_{R}^{k′+k}. Moreover, these rational points induce an equality of fibre products

Spec C ×_{𝔸_{R}^{k′+k}} Spec R = Y ×_{𝔸_{R}^{k}} Spec R.  (27)

Since a lifting of an R-rational point on 𝔸_{R}^{k′+k} or 𝔸_{R}^{k} corresponds to an R-rational point on these respective fibre products, we may assume, after enlarging the tuple of variables U, that the f_{i} have already coefficients over ℤ.

Let e_{1}, …, e_{τ} be a basis of R/𝔪^{N} over κ. Write the image of u in R/𝔪^{N} as l_{1}e_{1} + ⋯ + l_{τ} e_{τ} with l_{i} tuples over κ and set l equal to the tuple of all l_{i}. Let ζ_{j} and λ be tuples of variables with ζ equal to the tuple of all ζ_{j} and write

f̄_{i}(u, ζ_{1}e_{1} + … ζ_{τ} e_{τ}) = g_{i1}(l, ζ)e_{1} + ⋯ + g_{iτ} (l, ζ)e_{τ}  (28)

for i = 1, …, t, with g_{ij} ∈ κ[λ, ζ] and where f̄_{i} denotes the reduction of f_{i} modulo 𝔪. Then the equivalence (26) has a solution if, and only if, the system of equations g_{ij}(l, ζ) = 0 has a solution in κ. Therefore, we proved the last statement by setting 𝔜 = Spec κ[λ, ζ]/(g_{ij}) and 𝔛 = 𝔸_{κ}^{tτ}.

3.6. Remark In particular, if the subring generated by u is computable (see Remark 3.3) and if κ is either a finite field or an algebraically closed field, then the positive L(u)-existential theory of R is decidable. This is because in either case κ is decidable. In fact, if κ is finite, then we do not need to assume that R is equicharacteristic, provided we have the equivalent statement for mixed characteristic in Theorem 3.1, for then R/𝔪^{N} will also be finite whence decidable.

4 The Existential Theory of 𝔽_{p}[[t]].

We will assume the truth of the following Conjecture.

Conjecture 1 (Resolution of Singularities) Let X be a reduced scheme of finite type over a field K. Then there exists a morphism f: X̃ → X of schemes of finite type over K, such that

• f is a blowing up in a nowhere dense centre defined over K;

• X̃ is non-singular.

Note that a blowing up in a nowhere dense centre is a proper, birational morphism by [11, Chapter II Proposition 7.16]. In fact, one expects that if the conjecture is true then we can take f to be a composition of finitely many blowing ups with smooth centres.

The Conjecture is known in the following cases.

• If K has characteristic zero, by a theorem of Hironaka in [12]; see also [5].

• If X has dimension at most two, by a theorem of Abhyankar in [1].

4.1. Remark If the Conjecture holds for the scheme X, then we can in fact calculate the desingularization f in an effective way as follows. Firstly, without loss of generality, we may assume that X = Spec A is affine. Let K_{0} be a finitely generated (whence countable) field over which X is already defined, so that X = Spec A_{0}×_{K_{0}} K, where A_{0} is some finitely generated K_{0}-algebra. Let 𝔞_{1}, 𝔞_{2}, … be an enumeration of all ideals of A_{0} defining a nowhere dense closed subset of Spec A_{0}. For each i = 1, 2, …, let f_{i}: X_{i} → Spec A_{0} be the blowing up with respect to 𝔞_{i}. To check whether X_{i} is non-singular, we can use the Jacobian Criterion [16, Theorem 30.3], which amounts in checking whether certain determinants vanish or not. This establishes an effective procedure to find a desingularization for X, since after checking a finite number of ideals, we must arrive, according to Resolution of Singularities, at a situation where the blowing up is non-singular. This algorithm does rely though on the fact that we can verify identities holding in K_{0} (or K). In particular, if X is already defined over the prime field or a transcendental extension of the prime field (or, for that matter, over any computable subfield), then the desingularization is computable.

4.2. Lemma Let R be a domain with field of fractions K. Let X be a scheme of finite type over Spec R. There exists a closed subscheme Y of X, such that Y_{K} is equal to the reduced closed subscheme of X_{K} (that is to say, Y_{K} and X_{K} have the same underlying set and Y_{K} is reduced), and such that any R-rational point on X lies already on Y. Moreover, there exists an algorithm which calculates Y from X.

Proof We may assume that X = Spec A is affine, with A a finitely generated Ralgebra. Suppose A = R[ξ]/(f_{1}, …, f_{t}), with ξ = (ξ_{1}, …, ξ_{m}) variables. Therefore, K[ξ]/(f_{1}, …, f_{t})K[ξ] is the affine algebra of X_{K}. Let g_{1}, …, g_{s} ∈ R[ξ], so that the radical of (f_{1}, …, f_{t})K[ξ] equals (g_{1}, …, g_{s})K[ξ]. By [20, Theorem 2.10], there exists a uniform bound on the degrees of the g_{i}, depending in a computable way, only on the degrees of the f_{i}. This latter fact implies that there is an algorithm which effectively calculates these g_{i} at least over K, after which we just need to clear denominators to obtain polynomials over R.

Let B = R[ξ]/(f_{1}, …, f_{t}, g_{1}, …, g_{s}) and set Y = Spec B, so that Y is a closed subscheme of X. By construction Y_{K} equals the reduced closed subscheme with the same underlying set as X_{K}. Suppose that x is an R-rational point on X. To x there corresponds an R-tuple r ∈ R^{m} such that f_{1}(r) = ⋯ = f_{t}(r) = 0, as explained above in 2.1. Since the g_{i} belong to the radical of (f_{1}, …, f_{t})K[ξ], it follows that also g_{1}(r) = ⋯ = g_{s}(r) = 0. Using once more the correspondence between Rrational points and solutions over R, we see that x is an R-rational point on Y, as required.

We can now prove the main theorem of this paper.

4.3. Theorem Let us assume the validity of Conjecture 1. Let R be an excellent equicharacteristic Henselian discrete valuation ring with residue field κ. Then the existential theory of R in the language L^{DVR} is decidable relative to the existential theory of κ and the L^{DVR}-diagram of R.

In particular, the L^{DVR}-existential theory of 𝔽_{p}[[t]] is decidable, where t is a single variable.

Proof The last statement follows immediately from the first statement, as a finite field is definable. Hence remains to show the first statement. Let 𝔪 = πR be the maximal ideal of R. Let K denote the field of fractions of R and let R_{0} be the subring of R generated by the uniformizing parameter π. Let φ be an existential sentence in the language L^{DVR}. The theorem states that there is an algorithm deciding whether φ holds in R, where the algorithm is allowed to use the existential theory of κ as an oracle, that is to say, we may assume that we know how to decide whether an existential sentence is true over κ.

The sentence φ is a disjunction of sentences of the form

(∃ξ)f_{1}(π, ξ) = f_{2}(π, ξ) = ⋯ = f_{t}(π, ξ) = 0 ∧ f_{0}(π, ξ) ≠ 0  (29)

with f_{i} ∈ Z[U, ξ], for i = 0, …, t and where U and ξ = (ξ_{1}, …, ξ_{m}) are variables. We may assume that φ is just one such disjunct (29). Let X denote the closed subscheme of A_{R}^{m} defined by the ideal (f_{1}(π, ξ), …, f_{t}(π, ξ)), that is to say,

X = Spec(R[ξ]/(f_{1}(π, ξ), …, f_{t}(π, ξ)).  (30)

Let W be the Zariski open subset of X defined by the extra condition f_{0}(π, ξ) ≠ 0. We have to exhibit an algorithm which verifies whether or not W admits an Rrational point. Using Lemma 4.2, we may even assume that X_{K} is reduced, where as always

X_{K} ≅ Spec(K[ξ]/(f_{1}(π, ξ), …, f_{t}(π, ξ))  (31)

is the generic fibre of X.

Apply Conjecture 1 to the reduced scheme X_{K} to obtain a morphism h: V → X_{K} of schemes of finite type over K, such that h is a blowing up defined over K, and V is non-singular. Moreover, by Remark 4.1, there is a computable function that calculates this desingularization h, since X_{K} is defined over the field of fractions of R_{0}. By clearing denominators in the defining equations of the centre, we can find a scheme Y of finite type over Spec R (in fact, over R_{0}) and a blowing up f: Y → X with nowhere dense centre Z defined over R, such that Y_{K} ≅ V and the base change f_{K} of f coincides with h.

The algorithm now works as follows, by induction on the dimension of X. Check first whether W ∩ Z admits an R-rational point, using the induction hypothesis on the lower dimensional scheme Z. If a solution exists, we are done. So assume no such solution exists. We then check whether Y admits an R-rational point using Proposition 3.5. Suppose we found an R-rational point on Y. Since V is non-singular, the underlying point of an arbitrary R-rational point on Y is nonsingular. Therefore, using Theorem 2.4, it follows that also the non-empty open subset f^{−1}(W) − f^{−1}(Z) admits an R-rational point y. Since f is defined over R, it follows that f ∘ y is an R-rational point on W and we are done.

Finally, suppose neither does there exist an R-rational point on Y. I claim that in that case W does not admit an R-rational point. Indeed, assume that x is an R-rational point on W. By our first assumption, x must be an R-rational point on the open X − Z. Therefore, the underlying point x_{K} of x does not belong to Z_{K}. Since f is an isomorphism outside Z, so is h = f_{K} outside Z_{K}. Hence there exists exactly one (K-rational) point w on Y_{K} with h(w) = x_{K}. By Proposition 2.2 and the fact that f is proper ([11, Chapter II Proposition 7.16]), there exists therefore an R-rational point on Y (lifting x), contradiction.

4.4. Remark The restriction on R to be equicharacteristic comes from the same restriction in Proposition 3.5. However, using the remark following that Proposition, we can extend the above Theorem to the case that R has mixed characteristic with finite residue field, provided the mixed characteristic analogue of Theorem 3.1 holds. A similar remark applies to Theorem 5.2 below.

5 General Existential Sentences

5.1. Definition Let X be a reduced scheme of finite type over a field K. The smooth stratification of X is the chain of closed subsets

∅ = X_{0} ⊂ X_{1} ⊂ X_{2} ⊂ ⋯ ⊂ X_{h} ⊂ X_{h+1} = X  (32)

where each X_{i} is the non-smooth locus of X_{i+1}, for i = 1, …, h. Note that using the Jacobian Criterion for smoothness [16, Theorem 30.3], the non-smooth locus is closed. Moreover, given defining equations for X, one calculates the smooth stratification of X using this Jacobian Criterion.

We define the bad locus Σ of X as the union of all smooth connected components of some X_{i}, where i ranges from 1 to h. Note that this union is in fact a disjoint union. Indeed, let F be a smooth connected component of X_{i}, for some i = 1, …, h, and let F′ be another smooth connected component of X_{i′}, for some i′ = 1, …, h. If i = i′ but F ≠ F′, then clearly F and F′ are disjoint, so we may assume i′ < i. Since F is smooth, it is disjoint from X_{i−1} whence from X_{i′}, so that F ∩ F′ = ∅, proving our claim. In particular, the bad locus is itself a smooth scheme and its connected components are irreducible. The latter is a consequence of the fact that a smooth and connected scheme is irreducible.

For example, if the non-smooth locus of X consists of three lines forming a triangle together with a fourth line disjoint from these three, then the bad locus consists of the three vertices of the triangle together with the fourth line.

In this paper, we will say that an open subset W of X lies in general position, if its intersection with the bad locus is everywhere dense in the bad locus. Note that this means that the complement X −W of W does not contain any irreducible component of the bad locus. For instance, for the example in the previous paragraph, W will be in general position if it contains the three vertices and intersects the fourth line.

Let R be a domain with field of fractions K. Let f_{i} ∈ R[ξ], for i = 0, …, t, with ξ = (ξ_{1}, …, ξ_{m}) variables. Let X be the closed subscheme of 𝔸_{R}^{m} defined by the ideal (f_{1}, …, f_{t}). In other words, X has affine coordinate ring R[ξ]/(f_{1}, …, f_{t}). Let W be the open in X given by the extra condition f_{0} ≠ 0. We will say that the existential sentence

(∃ξ)f_{1}(ξ) = f_{2}(ξ) = ⋯ = f_{t}(ξ) = 0 ∧ f_{0}(ξ) ≠ 0  (33)

is general, if W_{K} lies in general position on the reduction of X_{K}, where as always a subscript K indicates the generic fibre of a scheme, that is to say, the base change over K. We call an arbitrary existential sentence general, if it is a disjunction of general sentences of the form (33).

5.2. Theorem Let R be an excellent equicharacteristic Henselian local domain. Let u be a k-tuple in R. There is an algorithm relative to the residue field of R and the L(u)-diagram of R, which decides whether a general existential sentence with parameters u, holds in R.

Proof Let κ be the residue field of R and 𝔪 its maximal ideal. Let K denote the field of fractions of R. Let U = (U_{1}, …, U_{k}) be a k-tuple of variables. Let φ be a general existential sentence with parameters u. The theorem then states that there is an algorithm deciding whether φ holds in R, where the algorithm is allowed to use the existential theory of κ and the equational theory of the subring generated by u as oracles, that is to say, we may assume that we know how to decide whether an (arbitrary) existential sentence is true over κ and whether a polynomial h(U) with integer coefficients vanishes on u in R.

Let φ be an arbitrary general existential sentence. In other words, φ is a disjunction of general sentences of the form

(∃ξ)f_{1}(u, ξ) = f_{2}(u, ξ) = ⋯ = f_{t}(u, ξ) = 0 ∧ f_{0}(u, ξ) ≠ 0  (34)

with f_{i} ∈ ℤ[U, ξ], for i = 0, …, t and where ξ = (ξ_{1}, …, ξ_{m}) is a tuple of variables. In order to prove the theorem, we may assume that φ is just one such disjunct (34). Let X denote the closed subscheme of A_{R}^{m} defined by the ideal (f_{1}(u, ξ), …, f_{t}(u, ξ)) and let W be the Zariski open subset of X defined by the extra condition f_{0}(u, ξ) ≠ 0. By definition, W_{K} lies in general position on the reduction of X_{K}. Using Lemma 4.2, we may assume that X_{K} is actually reduced (the sentence corresponding to this new X is equivalent over R with the original φ).

Choose an increasing sequence of closed subschemes

∅ = X_{0} ⊂ X_{1} ⊂ X_{2} ⊂ ⋯ ⊂ X_{h} ⊂ X_{h+1} = X  (35)

so that their generic fibers form the smooth stratification of X_{K}. Recall that this means that (X_{1})_{K} and all the open subsets (X_{i+1})_{K} − (X_{i})_{K}, for i = 1, …, h are smooth over K. Moreover, using the Jacobian Criterion for smoothness [16, Theorem 30.3], such a sequence can effectively be constructed from the f_{i}, modulo the L(u)-diagram of R.

We next describe the algorithm that will verify whether or not W admits an R-rational point. First check whether X_{1} has an R-rational point using Proposition 3.5. If there is an R-rational point on X_{1}, we stop and let the output of our algorithm be yes. If not, we check, using Proposition 3.5 again, whether X_{2} has an R-rational point. If it does, we stop and let the output be yes, otherwise we continue. At each stage, we check for the existence of an R-rational point on X_{i} using Proposition 3.5, stop when such a point exists and give the output yes, or continue otherwise. If we exhausted all the X_{i} (including the final X_{h+1} = X) and still have not found an R-rational point, we conclude that W has no R-rational point, so we stop and give the output no.

Let us verify the correctness of this algorithm. Obviously, if an R-rational point on W exists, then the algorithm will give output yes. Conversely, if the output is yes, then at some stage i ∈ {1, …, h + 1}, we found an R-rational point x in X_{i}, but no R-rational point was found in X_{i−1}. Therefore x lies in X_{i} − X_{i−1}. Hence its underlying point x_{K} lies in (X_{i})_{K} − (X_{i−1})_{K} whence is a smooth point of (X_{i})_{K}. By Theorem 2.4, the R-rational points are therefore dense on X_{i} in a neighbourhood of x. More precisely, there is an open V of X_{i} which is defined over R and admits x as an R-rational point, such that if W ∩ V is non-empty (in the scheme-theoretic sense), then W ∩ V admits also an R-rational point. Therefore we established the validity of the algorithm, provided we can show that W ∩ V is non-empty.

To this end, let F be an irreducible component of X_{i}. By construction of the bad locus, we can find an irreducible component Z of the bad locus of X_{K} with Z ⊂ F_{K}. Our general position assumption implies that Z ∩ W_{K} is non-empty. Therefore, F_{K} ∩ W_{K} whence F ∩ W is non-empty and therefore F ∩ W is dense in F. Since this holds for every irreducible component of X_{i}, it follows that W ∩ X_{i} is dense in X_{i}, so that W ∩ V is non-empty, as required.

References

1. S. Abhyankar, Resolution of singularities of embedded algebraic surfaces, Pure and Applied Math., vol. 24, Academic Press, New York, 1966.

2. M. Artin, Algebraic approximation of structures over complete local rings, Inst. Hautes Études Sci. Publ. Math. 36 (1969), 23–58.

3. J. Ax and S. Kochen, Diophantine problems over local fields I, II, Amer. J. Math. 87 (1965), 605–630, 631–648.

4. J. Becker, J. Denef, L. van den Dries, and L. Lipshitz, Ultraproducts and approximation in local rings I, Invent. Math. 51 (1979), 189–203.

5. E. Bierstone and P.D. Milman, Canonical desingularization in characteristic zero by blowing up the maximal strata of a local invariant, Invent. Math. 128 (1997), 207–302.

6. J. Denef and L. Lipshitz, Ultraproducts and approximation in local rings II, Math. Ann. 253 (1980), 1–28.

7. Y. Eršhov, On the elementary theory of maximal normed fields I, Algebra i Logica 4 (1965), 31–69.

8. , On the elementary theory of maximal normed fields II, Algebra i Logica 5 (1966), 8–40.

9. , On the elementary theory of maximal normed fields III, Algebra i Logica 6 (1967), 31–37.

10. M. J. Greenberg, Rational points in henselian discrete valuation rings, Inst. Hautes Études Sci. Publ. Math. 31 (1966), 59–64.

11. R. Hartshorne, Algebraic geometry, Springer-Verlag, New York, 1977.

12. H. Hironaka, Resolution of singularities of an algebraic variety over a field of characteristic zero, Ann. of Math. 79 (1964), 109–326.

13. W. Hodges, Model theory, Cambridge University Press, Cambridge, 1993.

14. F.-V. Kuhlmann, Elementary properties of power series fields over finite fields, Fields Institute Preprint Series, 1998.

15. H. Matsumura, Commutative algebra, W.A. Benjamin, 1970.

16. , Commutative ring theory, Cambridge University Press, Cambridge, 1986.

17. J. Milne, Etale cohomology, 33, Princeton Math., 1980.

18. D. Popescu, General Néron desingularization and approximation, Nagoya Math. J. 104 (1986), 85–115.

19. M. Raynaud, Anneaux locaux henséliens, Lect. Notes in Math., Springer-Verlag, 1970.

20. K. Schmidt and L. van den Dries, Bounds in the theory of polynomial rings over fields. A non-standard approach, Invent. Math. 76 (1984), 77–91.

21. H. Schoutens, Reduction modulo p of power series with integer coefficients, preprint available

on URL address http://www.math.ohio-state.edu/˜ schoutens/Postscript/IntegerPowerSeries.ps, 2001.

22. M. Spivakovsky, Smoothing of ring homomorphisms, approximation theorems, and the Bass-Quillen conjecture, preprint.

23. R. Swan, Néron-Popescu desingularization, expanded notes from a Univ. of Chicago series of lectures, Spring 1995.