[proofplan]
We prove completeness by showing that any two models of $\mathrm{ACF}_0$ satisfy the same first-order sentences. [Quantifier elimination for algebraically closed fields](/theorems/4310) reduces an arbitrary sentence to a quantifier-free sentence. Since a quantifier-free sentence contains no variables, its atomic formulas compare only closed ring terms, and closed ring terms always evaluate to integer multiples of the multiplicative identity. Characteristic $0$ makes all such integer equalities have the same truth value in every model, so every sentence has a model-independent truth value among models of $\mathrm{ACF}_0$.
[/proofplan]
[step:Reduce an arbitrary sentence to a quantifier-free sentence]
Let $\varphi$ be an arbitrary $\mathcal{L}_{\mathrm{ring}}$-sentence. By the quantifier-elimination theorem for algebraically closed fields (citing a result not yet in the wiki: Quantifier Elimination for Algebraically Closed Fields), there exists a quantifier-free $\mathcal{L}_{\mathrm{ring}}$-formula $\psi$ such that
\begin{align*}
\mathrm{ACF}_0 \models \varphi \leftrightarrow \psi.
\end{align*}
Because $\varphi$ is a sentence and logical equivalence preserves free variables, we may take $\psi$ to be a quantifier-free sentence.
[guided]
We want to prove that the truth value of $\varphi$ is the same in every algebraically closed field of characteristic $0$. The main model-theoretic input is quantifier elimination for algebraically closed fields (citing a result not yet in the wiki: Quantifier Elimination for Algebraically Closed Fields). Applied to the sentence $\varphi$, it gives a quantifier-free $\mathcal{L}_{\mathrm{ring}}$-formula $\psi$ such that every algebraically closed field of characteristic $0$ satisfies the equivalence
\begin{align*}
\varphi \leftrightarrow \psi.
\end{align*}
Equivalently,
\begin{align*}
\mathrm{ACF}_0 \models \varphi \leftrightarrow \psi.
\end{align*}
Since $\varphi$ has no free variables, the equivalent quantifier-free formula may also be chosen with no free variables: replacing a sentence by an equivalent formula with unused free variables would not change the truth value, but those variables play no role. Thus the problem is reduced from arbitrary first-order sentences to quantifier-free sentences in the language of rings.
[/guided]
[/step]
[step:Identify the values of closed ring terms]
Let $t$ be a closed $\mathcal{L}_{\mathrm{ring}}$-term. We associate to $t$ an integer $n(t) \in \mathbb{Z}$ by structural recursion:
\begin{align*}
n(0) &= 0, &
n(1) &= 1, \\
n(t_1 + t_2) &= n(t_1) + n(t_2), &
n(-t_1) &= -n(t_1), \\
n(t_1 \cdot t_2) &= n(t_1)n(t_2).
\end{align*}
For every field $K$ viewed as an $\mathcal{L}_{\mathrm{ring}}$-structure, the interpretation $t^K$ of $t$ in $K$ satisfies
\begin{align*}
t^K = n(t)\cdot 1_K,
\end{align*}
where $n\cdot 1_K$ denotes the usual integer multiple of $1_K$.
This follows by induction on the construction of $t$. The constants $0$ and $1$ satisfy the claim by definition of the ring structure. The recursive clauses for $+$, unary $-$, and $\cdot$ agree exactly with addition, additive inverse, and multiplication of integer multiples of $1_K$.
[guided]
A quantifier-free sentence is built from atomic formulas, and in the language of rings the atomic formulas are equalities between terms. Since our sentence has no variables, all terms appearing in it are closed terms. We now record exactly what such terms can denote.
For each closed $\mathcal{L}_{\mathrm{ring}}$-term $t$, define an integer $n(t) \in \mathbb{Z}$ recursively by
\begin{align*}
n(0) &= 0, &
n(1) &= 1, \\
n(t_1 + t_2) &= n(t_1) + n(t_2), &
n(-t_1) &= -n(t_1), \\
n(t_1 \cdot t_2) &= n(t_1)n(t_2).
\end{align*}
This integer is the formal value obtained by evaluating the term using the usual ring operations on $\mathbb{Z}$.
We claim that if $K$ is any field, then the interpretation $t^K$ of $t$ in $K$ is
\begin{align*}
t^K = n(t)\cdot 1_K.
\end{align*}
The proof is structural induction on $t$. For $t=0$, the interpretation is $0_K = 0\cdot 1_K$. For $t=1$, the interpretation is $1_K = 1\cdot 1_K$. If the claim holds for $t_1$ and $t_2$, then
\begin{align*}
(t_1+t_2)^K
&= t_1^K+t_2^K \\
&= n(t_1)\cdot 1_K+n(t_2)\cdot 1_K \\
&= \bigl(n(t_1)+n(t_2)\bigr)\cdot 1_K \\
&= n(t_1+t_2)\cdot 1_K.
\end{align*}
The unary minus case is
\begin{align*}
(-t_1)^K
&= -t_1^K \\
&= -\bigl(n(t_1)\cdot 1_K\bigr) \\
&= \bigl(-n(t_1)\bigr)\cdot 1_K \\
&= n(-t_1)\cdot 1_K.
\end{align*}
Finally, for multiplication,
\begin{align*}
(t_1\cdot t_2)^K
&= t_1^K t_2^K \\
&= \bigl(n(t_1)\cdot 1_K\bigr)\bigl(n(t_2)\cdot 1_K\bigr) \\
&= n(t_1)n(t_2)\cdot 1_K \\
&= n(t_1\cdot t_2)\cdot 1_K.
\end{align*}
Thus every closed ring term denotes an integer multiple of the multiplicative identity.
[/guided]
[/step]
[step:Show atomic closed equalities have field-independent truth values in characteristic $0$]
Let $K$ be a field of characteristic $0$, and let $t_1,t_2$ be closed $\mathcal{L}_{\mathrm{ring}}$-terms. By the preceding step,
\begin{align*}
K \models t_1=t_2
\quad\Longleftrightarrow\quad
n(t_1)\cdot 1_K = n(t_2)\cdot 1_K.
\end{align*}
Equivalently,
\begin{align*}
K \models t_1=t_2
\quad\Longleftrightarrow\quad
\bigl(n(t_1)-n(t_2)\bigr)\cdot 1_K = 0_K.
\end{align*}
Since $K$ has characteristic $0$, the map $\mathbb{Z}\to K$ given by $m\mapsto m\cdot 1_K$ is injective. Therefore
\begin{align*}
K \models t_1=t_2
\quad\Longleftrightarrow\quad
n(t_1)=n(t_2).
\end{align*}
The right-hand condition depends only on the two syntactic terms, not on $K$.
[guided]
Let $K$ be a field of characteristic $0$, and consider an atomic sentence $t_1=t_2$, where $t_1$ and $t_2$ are closed $\mathcal{L}_{\mathrm{ring}}$-terms. From the previous step, both sides evaluate to integer multiples of $1_K$:
\begin{align*}
t_1^K &= n(t_1)\cdot 1_K, \\
t_2^K &= n(t_2)\cdot 1_K.
\end{align*}
Hence
\begin{align*}
K \models t_1=t_2
\quad\Longleftrightarrow\quad
n(t_1)\cdot 1_K = n(t_2)\cdot 1_K.
\end{align*}
Subtracting the right-hand side inside the additive group of $K$, this is equivalent to
\begin{align*}
K \models t_1=t_2
\quad\Longleftrightarrow\quad
\bigl(n(t_1)-n(t_2)\bigr)\cdot 1_K = 0_K.
\end{align*}
Now we use characteristic $0$. By definition, characteristic $0$ means that no positive integer multiple of $1_K$ is equal to $0_K$. Equivalently, the canonical ring homomorphism
\begin{align*}
\mathbb{Z} &\to K \\
m &\mapsto m\cdot 1_K
\end{align*}
is injective. Therefore
\begin{align*}
\bigl(n(t_1)-n(t_2)\bigr)\cdot 1_K = 0_K
\quad\Longleftrightarrow\quad
n(t_1)-n(t_2)=0,
\end{align*}
and hence
\begin{align*}
K \models t_1=t_2
\quad\Longleftrightarrow\quad
n(t_1)=n(t_2).
\end{align*}
This criterion is purely arithmetic in $\mathbb{Z}$ and does not depend on which characteristic $0$ field $K$ we chose.
[/guided]
[/step]
[step:Extend field-independence from atomic formulas to quantifier-free sentences]
Let $\psi$ be a quantifier-free $\mathcal{L}_{\mathrm{ring}}$-sentence. Since $\psi$ has no variables, it is obtained from finitely many atomic closed equalities $t_i=s_i$ using the Boolean connectives $\neg$, $\wedge$, and $\vee$. The preceding step shows that each atomic equality $t_i=s_i$ has the same truth value in every field of characteristic $0$. By induction on the Boolean construction of $\psi$, the sentence $\psi$ has the same truth value in every field of characteristic $0$.
[guided]
A quantifier-free sentence in the language of rings is built from atomic formulas by Boolean connectives. Since the sentence has no free variables, each atomic formula appearing in it is an equality
\begin{align*}
t_i=s_i
\end{align*}
between closed $\mathcal{L}_{\mathrm{ring}}$-terms. The previous step proves that, in every field of characteristic $0$,
\begin{align*}
K \models t_i=s_i
\quad\Longleftrightarrow\quad
n(t_i)=n(s_i).
\end{align*}
Thus each atomic equality has a truth value independent of $K$.
We now pass from atomic formulas to the full quantifier-free sentence. This is a structural induction on the Boolean construction of $\psi$. If $\psi$ is atomic, the claim is exactly the preceding paragraph. If $\psi$ is $\neg \theta$, then its truth value is the opposite of the field-independent truth value of $\theta$. If $\psi$ is $\theta_1\wedge \theta_2$, then its truth value is determined by the two field-independent truth values of $\theta_1$ and $\theta_2$. The case $\theta_1\vee \theta_2$ is identical, with disjunction replacing conjunction. Therefore every quantifier-free $\mathcal{L}_{\mathrm{ring}}$-sentence has the same truth value in every field of characteristic $0$.
[/guided]
[/step]
[step:Conclude that all models of $\mathrm{ACF}_0$ satisfy the same sentences]
Let $K$ and $L$ be arbitrary models of $\mathrm{ACF}_0$. Then $K$ and $L$ are algebraically closed fields of characteristic $0$. For the original sentence $\varphi$, choose the quantifier-free sentence $\psi$ from the first step. Since
\begin{align*}
\mathrm{ACF}_0 \models \varphi \leftrightarrow \psi,
\end{align*}
we have
\begin{align*}
K \models \varphi
\quad\Longleftrightarrow\quad
K \models \psi
\quad\Longleftrightarrow\quad
L \models \psi
\quad\Longleftrightarrow\quad
L \models \varphi.
\end{align*}
Thus any two models of $\mathrm{ACF}_0$ satisfy the same $\mathcal{L}_{\mathrm{ring}}$-sentences. Therefore $\mathrm{ACF}_0$ is complete.
[guided]
Let $K$ and $L$ be any two models of $\mathrm{ACF}_0$. By definition of $\mathrm{ACF}_0$, both are algebraically closed fields of characteristic $0$. We started with an arbitrary $\mathcal{L}_{\mathrm{ring}}$-sentence $\varphi$, and quantifier elimination gave a quantifier-free sentence $\psi$ such that
\begin{align*}
\mathrm{ACF}_0 \models \varphi \leftrightarrow \psi.
\end{align*}
Since $K\models \mathrm{ACF}_0$ and $L\models \mathrm{ACF}_0$, this equivalence holds inside both structures:
\begin{align*}
K \models \varphi \leftrightarrow \psi,
\qquad
L \models \varphi \leftrightarrow \psi.
\end{align*}
The previous step says that $\psi$ has the same truth value in every field of characteristic $0$, so
\begin{align*}
K \models \psi
\quad\Longleftrightarrow\quad
L \models \psi.
\end{align*}
Combining these equivalences gives
\begin{align*}
K \models \varphi
\quad\Longleftrightarrow\quad
K \models \psi
\quad\Longleftrightarrow\quad
L \models \psi
\quad\Longleftrightarrow\quad
L \models \varphi.
\end{align*}
Because $\varphi$ was arbitrary, $K$ and $L$ satisfy exactly the same $\mathcal{L}_{\mathrm{ring}}$-sentences. Therefore all models of $\mathrm{ACF}_0$ are elementarily equivalent, which is precisely completeness of $\mathrm{ACF}_0$.
[/guided]
[/step]