[proofplan] We prove that existential projection preserves quantifier-free definability over algebraically closed fields. A quantifier-free formula defines a constructible subset of affine space, because it is a finite Boolean combination of polynomial equations. The uniform form of [Chevalley's theorem](/theorems/2618) says that the projection of such a constructible set is again constructible, and the Noetherian nature of polynomial rings lets this constructible set be described by one finite quantifier-free formula with integer coefficients. Once existential quantifiers are eliminated, arbitrary formulas are handled by induction on the number of quantifiers, using Boolean operations and rewriting universal quantifiers through negation. [/proofplan]

[step:Translate quantifier-free formulas into constructible sets]Let $m \geq 0$ and let $z = (z_1,\dots,z_m)$ be a tuple of variables. Every $\mathcal L_{\mathrm{ring}}$-term in the variables $z$ is represented, modulo the ring axioms, by a polynomial in $\mathbb Z[z_1,\dots,z_m]$. Hence every atomic $\mathcal L_{\mathrm{ring}}$-formula in the variables $z$ is equivalent, over fields, to an equation \begin{align*} f(z) = 0 \end{align*} for some polynomial $f \in \mathbb Z[z_1,\dots,z_m]$. Let $K$ be an algebraically closed field, and let $\theta(z)$ be quantifier-free. The set \begin{align*} \theta(K) := \{a \in K^m : K \models \theta(a)\} \end{align*} is a finite Boolean combination of subsets of the form \begin{align*} V_K(f) := \{a \in K^m : f(a) = 0\}, \end{align*} where $f \in \mathbb Z[z_1,\dots,z_m]$. Thus $\theta(K)$ is a constructible subset of $K^m$ in the Zariski topology.[/step]

[guided]We first connect syntax with algebraic geometry. In the language of rings, every term is built from the variables, $0$, $1$, addition, subtraction, and multiplication. Therefore each term in variables $z = (z_1,\dots,z_m)$ is interpreted in every ring by a polynomial with integer coefficients. An atomic formula has the form $t_1(z) = t_2(z)$, and this is equivalent to \begin{align*} t_1(z) - t_2(z) = 0. \end{align*} Writing $f \in \mathbb Z[z_1,\dots,z_m]$ for the polynomial represented by $t_1 - t_2$, the atomic formula defines the algebraic set \begin{align*} V_K(f) := \{a \in K^m : f(a) = 0\} \end{align*} inside $K^m$. A quantifier-free formula is obtained from atomic formulas by finitely many applications of $\neg$, $\wedge$, and $\vee$. Taking negations, intersections, and unions of algebraic sets gives finite Boolean combinations of algebraic sets. These are precisely constructible subsets of affine space. Therefore, for every algebraically closed field $K$, the realization \begin{align*} \theta(K) := \{a \in K^m : K \models \theta(a)\} \end{align*} is constructible in the Zariski topology on $K^m$.[/guided]

[step:Eliminate one existential quantifier]Let $\theta(x,y)$ be a quantifier-free $\mathcal L_{\mathrm{ring}}$-formula, where $x = (x_1,\dots,x_n)$ and $y$ is one variable. We prove that there is a quantifier-free formula $\eta(x)$ such that \begin{align*} \mathrm{ACF} \models \forall x_1\cdots\forall x_n\bigl((\exists y\,\theta(x,y)) \leftrightarrow \eta(x)\bigr). \end{align*} For an algebraically closed field $K$, define \begin{align*} X_K := \{(a,b) \in K^n \times K : K \models \theta(a,b)\}. \end{align*} By the preceding step, $X_K$ is constructible in $K^{n+1}$. Let \begin{align*} \pi_K: K^n \times K &\to K^n \\ (a,b) &\mapsto a \end{align*} be the coordinate projection. By the uniform form of Chevalley's theorem, applied to the constructible family defined over $\mathbb Z$ by the finitely many polynomials occurring in $\theta$, there is a constructible condition on $K^n$, given uniformly by finitely many polynomial equations and inequalities with integer coefficients, whose realization is exactly $\pi_K(X_K)$ for every algebraically closed field $K$. Equivalently, there exist polynomials $g_{ij},h_{ij} \in \mathbb Z[x_1,\dots,x_n]$, with $1 \leq i \leq r$ and $1 \leq j \leq s_i$, such that for every algebraically closed field $K$ and every $a \in K^n$, \begin{align*} a \in \pi_K(X_K) \end{align*} if and only if \begin{align*} K \models \bigvee_{i=1}^r \left(\bigwedge_{j=1}^{s_i} g_{ij}(a)=0 \wedge \bigwedge_{j=1}^{s_i} h_{ij}(a)\neq 0\right), \end{align*} after omitting empty conjunctions when necessary. Define $\eta(x)$ to be this quantifier-free formula. Since $a \in \pi_K(X_K)$ exactly means that there exists $b \in K$ with $K \models \theta(a,b)$, this $\eta$ eliminates the existential quantifier. Here we are using the following external algebraic-geometric input: (citing a result not yet in the wiki: Uniform Chevalley Theorem for constructible subsets defined over $\mathbb Z$).[/step]

[guided]The problem is to remove the quantifier from \begin{align*} \exists y\,\theta(x,y). \end{align*} Fix an algebraically closed field $K$. The formula $\theta(x,y)$ defines a subset \begin{align*} X_K := \{(a,b) \in K^n \times K : K \models \theta(a,b)\}. \end{align*} By the previous step, $X_K$ is constructible, because $\theta$ is quantifier-free. Now the formula $\exists y\,\theta(x,y)$ asks whether the point $a \in K^n$ is the first coordinate part of some point of $X_K$. Define the projection map \begin{align*} \pi_K: K^n \times K &\to K^n \\ (a,b) &\mapsto a. \end{align*} Then \begin{align*} K \models \exists y\,\theta(a,y) \end{align*} if and only if \begin{align*} a \in \pi_K(X_K). \end{align*} We now invoke the uniform form of Chevalley's theorem for constructible subsets defined over $\mathbb Z$ (citing a result not yet in the wiki: Uniform Chevalley Theorem for constructible subsets defined over $\mathbb Z$). Its hypotheses apply here because the set $X_K$ is described by finitely many polynomial equations and inequalities whose coefficients lie in $\mathbb Z$, independently of the algebraically closed field $K$. The theorem gives a constructible subset of $K^n$, described uniformly by finitely many polynomial equations and inequalities with integer coefficients, whose points are exactly $\pi_K(X_K)$ for every algebraically closed field $K$. Therefore there are polynomials $g_{ij},h_{ij} \in \mathbb Z[x_1,\dots,x_n]$ such that membership in the projection is expressed by the finite Boolean condition \begin{align*} \bigvee_{i=1}^r \left(\bigwedge_{j=1}^{s_i} g_{ij}(x)=0 \wedge \bigwedge_{j=1}^{s_i} h_{ij}(x)\neq 0\right). \end{align*} Call this quantifier-free formula $\eta(x)$. For every algebraically closed field $K$ and every $a \in K^n$, we then have \begin{align*} K \models \eta(a) \end{align*} if and only if \begin{align*} a \in \pi_K(X_K), \end{align*} which holds if and only if \begin{align*} K \models \exists y\,\theta(a,y). \end{align*} Thus $\eta(x)$ is equivalent over $\mathrm{ACF}$ to $\exists y\,\theta(x,y)$.[/guided]

[step:Induct on formulas to eliminate all quantifiers] We prove by induction on the formation of formulas that every $\mathcal L_{\mathrm{ring}}$-formula is equivalent over $\mathrm{ACF}$ to a quantifier-free formula. Atomic formulas are already quantifier-free. If $\alpha$ and $\beta$ are equivalent over $\mathrm{ACF}$ to quantifier-free formulas $\alpha_0$ and $\beta_0$, respectively, then $\neg\alpha$, $\alpha \wedge \beta$, and $\alpha \vee \beta$ are equivalent over $\mathrm{ACF}$ to $\neg\alpha_0$, $\alpha_0 \wedge \beta_0$, and $\alpha_0 \vee \beta_0$, respectively. It remains to handle quantifiers. Suppose $\varphi(x)$ has the form $\exists y\,\rho(x,y)$. By the induction hypothesis, $\rho(x,y)$ is equivalent over $\mathrm{ACF}$ to a quantifier-free formula $\theta(x,y)$. The preceding step gives a quantifier-free formula $\eta(x)$ equivalent over $\mathrm{ACF}$ to $\exists y\,\theta(x,y)$, hence also to $\exists y\,\rho(x,y)$. If $\varphi(x)$ has the form $\forall y\,\rho(x,y)$, then \begin{align*} \forall y\,\rho(x,y) \end{align*} is equivalent in first-order logic to \begin{align*} \neg \exists y\,\neg\rho(x,y). \end{align*} The existential case applied to $\neg\rho(x,y)$ therefore gives a quantifier-free equivalent for $\forall y\,\rho(x,y)$. This completes the induction and proves that every $\mathcal L_{\mathrm{ring}}$-formula is equivalent over $\mathrm{ACF}$ to a quantifier-free formula. [/step]