Verification of simple quantifier elimination in $T_{acf}$

Question

I'm doing some model theory, and just want to make sure I'm not making a mistake here. We consider $T_{acf}$, the theory of algebraically closed fields. I'm asked to find a $T_{acf}$ equivalent, quantifier free sentence for: $$\exists x (x^2+1=0\wedge x+1\not=0)$$ My reasoning: since we are working over algebraically closed fields, the content of this sentence is just that $-1$ is not a double root of $x^2+1$, so $$T_{acf}\vDash (\exists x (x^2+1=0\wedge x+1\not=0)) \Leftrightarrow \neg((-1)^2+1=0\wedge (1+1)(-1)=0)$$ and this last sentence is the same as $$1+1\not=0$$ i.e. the characteristic of the field is not $2$. Is this correct?

Answer 1

Yes, your reasoning is correct.

To make this into a slightly more substantial answer, I'll point out that since $\mathrm{ACF}_p$ is complete whenever $p$ is prime or $0$, it follows by compactness that every sentence $\psi$ in the language of fields is equivalent, modulo $\mathrm{ACF}$, a sentence of the form $\bigvee_{p\in F} \varphi_p$ (if $\psi$ is not in $\mathrm{ACF}_0$) or $\bigwedge_{p\in F}\lnot \varphi_p$ (if $\psi$ is in $\mathrm{ACF}_0$), where $F$ is a finite set of primes (I'm including the cases when $F$ is empty, so we get $\bot$ in the first case and $\top$ in the second), and $\varphi_p$ is the sentence $\underbrace{1+1+\dots+1}_{p\text{ times}} = 0$.