[proofplan] We use [quantifier elimination for algebraically closed fields](/theorems/4310) to reduce every sentence modulo $\mathrm{ACF}_p$ to a quantifier-free sentence. Let $\mathbb{F}_p$ denote the finite field $\mathbb{Z}/p\mathbb{Z}$ with $p$ elements. Since a quantifier-free sentence has no free variables, every ring term occurring in it is a closed term and hence evaluates in every characteristic-$p$ field to an element of the prime field canonically isomorphic to $\mathbb{F}_p$. Therefore the truth of such a quantifier-free sentence is independent of the chosen algebraically closed field of characteristic $p$. It follows that any two models of $\mathrm{ACF}_p$ satisfy exactly the same first-order sentences, which is precisely completeness. [/proofplan] [step:Reduce an arbitrary sentence to a quantifier-free sentence] Let $\varphi$ be an $\mathcal{L}_{\mathrm{ring}}$-sentence. By quantifier elimination for algebraically closed fields in fixed characteristic (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}_p \models \varphi \leftrightarrow \psi . \end{align*} Because $\varphi$ is a sentence and $\varphi$ is equivalent modulo $\mathrm{ACF}_p$ to $\psi$, we may take $\psi$ to be a quantifier-free sentence. [guided] We begin with an arbitrary first-order sentence $\varphi$ in the ring language \begin{align*} \mathcal{L}_{\mathrm{ring}} = \{0,1,+,-,\cdot\}. \end{align*} The key model-theoretic input is quantifier elimination for algebraically closed fields in fixed characteristic (citing a result not yet in the wiki: Quantifier Elimination for Algebraically Closed Fields). Applied to $\varphi$, it gives a quantifier-free $\mathcal{L}_{\mathrm{ring}}$-formula $\psi$ satisfying \begin{align*} \mathrm{ACF}_p \models \varphi \leftrightarrow \psi . \end{align*} Since $\varphi$ has no free variables, its equivalent quantifier-free formula may also be taken to have no free variables. Thus $\psi$ is a quantifier-free sentence. This reduction is the main point: to prove completeness of $\mathrm{ACF}_p$, it is now enough to show that all algebraically closed fields of characteristic $p$ agree on quantifier-free ring sentences. [/guided] [/step] [step:Show that closed ring terms evaluate in the prime field] Let $K$ be a model of $\mathrm{ACF}_p$. Every closed $\mathcal{L}_{\mathrm{ring}}$-term $t$ has an interpretation $t^K \in K$. We claim that $t^K$ lies in the prime subfield of $K$, which is canonically isomorphic to $\mathbb{F}_p$. Indeed, the constants $0$ and $1$ interpret as $0_K$ and $1_K$. The smallest subfield of $K$ containing $1_K$ is \begin{align*} \{n \cdot 1_K : n \in \mathbb{Z}\}, \end{align*} with the identification $n \cdot 1_K = m \cdot 1_K$ if and only if $n \equiv m \pmod p$. This subfield is isomorphic to $\mathbb{F}_p$. Since closed ring terms are built from $0$, $1$, $+$, $-$, and $\cdot$, induction on term formation shows that every $t^K$ belongs to this copy of $\mathbb{F}_p$. [guided] Fix a model $K \models \mathrm{ACF}_p$. Thus $K$ is an algebraically closed field and has characteristic $p$. We analyze what a closed ring term can denote in $K$. A closed $\mathcal{L}_{\mathrm{ring}}$-term is built from the symbols $0$, $1$, $+$, $-$, and $\cdot$, without variables. Therefore it can only produce elements obtained from $0_K$ and $1_K$ by repeatedly applying the field operations of $K$. The subfield generated by $1_K$ is \begin{align*} \{n \cdot 1_K : n \in \mathbb{Z}\}. \end{align*} Because $K$ has characteristic $p$, we have \begin{align*} p \cdot 1_K = 0_K, \end{align*} and the equality $n \cdot 1_K = m \cdot 1_K$ holds exactly when $n \equiv m \pmod p$. Hence this prime subfield is canonically isomorphic to $\mathbb{F}_p$. Now prove the assertion about terms by induction on their construction. The base terms $0$ and $1$ interpret as $0_K$ and $1_K$, both in the prime subfield. If closed terms $s$ and $t$ interpret in the prime subfield, then so do \begin{align*} (s+t)^K = s^K + t^K, \qquad (-s)^K = -s^K, \qquad (s \cdot t)^K = s^K t^K, \end{align*} because the prime subfield is closed under addition, additive inverse, and multiplication. Thus every closed term evaluates to an element of the prime field $\mathbb{F}_p \subset K$. [/guided] [/step] [step:Prove that all models agree on quantifier-free sentences] Let $K,L \models \mathrm{ACF}_p$. We show that $K \models \psi$ if and only if $L \models \psi$ for every quantifier-free $\mathcal{L}_{\mathrm{ring}}$-sentence $\psi$. Every atomic sentence in $\mathcal{L}_{\mathrm{ring}}$ has the form $s=t$, where $s$ and $t$ are closed ring terms. By the previous step, $s^K,t^K$ lie in the prime subfield $\mathbb{F}_p \subset K$, and $s^L,t^L$ lie in the prime subfield $\mathbb{F}_p \subset L$. Moreover the values are determined by the same formal calculation in $\mathbb{F}_p$. Hence \begin{align*} K \models s=t \quad \Longleftrightarrow \quad s^{\mathbb{F}_p}=t^{\mathbb{F}_p} \quad \Longleftrightarrow \quad L \models s=t . \end{align*} Since quantifier-free sentences are built from atomic sentences using Boolean connectives, induction on formula formation gives \begin{align*} K \models \psi \quad \Longleftrightarrow \quad L \models \psi . \end{align*} [guided] Let $K$ and $L$ be two arbitrary models of $\mathrm{ACF}_p$. We want to show that they agree on every quantifier-free sentence $\psi$. First consider an atomic sentence. In the language of rings, every atomic sentence has the form \begin{align*} s=t, \end{align*} where $s$ and $t$ are closed ring terms. From the previous step, the interpretations $s^K$ and $t^K$ lie in the prime subfield of $K$, and $s^L$ and $t^L$ lie in the prime subfield of $L$. Both prime subfields are canonically copies of $\mathbb{F}_p$, and the value of a closed term is obtained by performing the same formal ring calculation modulo $p$. Therefore \begin{align*} K \models s=t \quad \Longleftrightarrow \quad s^{\mathbb{F}_p}=t^{\mathbb{F}_p} \quad \Longleftrightarrow \quad L \models s=t . \end{align*} This proves agreement on atomic sentences. A quantifier-free sentence is obtained from atomic sentences by finitely many Boolean operations: negation, conjunction, disjunction, and possibly implication or biconditional as abbreviations. Truth under Boolean operations is determined solely by the truth values of the atomic components. Therefore an induction on the construction of $\psi$ gives \begin{align*} K \models \psi \quad \Longleftrightarrow \quad L \models \psi . \end{align*} Thus all models of $\mathrm{ACF}_p$ agree on all quantifier-free ring sentences. [/guided] [/step] [step:Conclude that $\mathrm{ACF}_p$ is complete] Let $K,L \models \mathrm{ACF}_p$, and let $\varphi$ be any $\mathcal{L}_{\mathrm{ring}}$-sentence. Choose a quantifier-free sentence $\psi$ such that \begin{align*} \mathrm{ACF}_p \models \varphi \leftrightarrow \psi . \end{align*} By the previous step, $K \models \psi$ if and only if $L \models \psi$. Hence \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}_p$ satisfy the same first-order sentences. Equivalently, for every sentence $\varphi$, either all models of $\mathrm{ACF}_p$ satisfy $\varphi$ or all models of $\mathrm{ACF}_p$ satisfy $\neg\varphi$. Therefore $\mathrm{ACF}_p$ is complete. [/step]