In Bruno Poizat's Model Theory I found the following proof of ACF's decidability:
1) ACF is $\Sigma_1$, i.e. the set of sentences which are proved by ACF is definable by a $\Sigma_1$ formula.
2) The complement of ACF is also $\Sigma_1$.
3) As a consequence, ACF is $\Delta_1$, hence decidable.
Points (2-3) are clear. Could someone help me proving point (1)? Proving that the set of sentences that axiomatize ACF is $\Sigma_1$ is sufficient.
Thank you in advance.
Here are informal descriptions of the $\Sigma_1$ formulas:
(1) There exists a finite set $\Phi$ of axioms of ACF and a proof of $\varphi$ from $\Phi$.
(2) There exists a prime number $p$ and a finite set $\Phi$ of axioms of ACF and a proof of $\lnot\varphi$ from $\Phi \cup \{p = 0\}$, or there exists a finite set $\{p_1,\dots,p_k\}$ of prime numbers and a finite set $\Phi$ of axioms of ACF and a proof of $\lnot\varphi$ from $\Phi \cup \{p_1 \neq 0\mid 1\leq i\leq k\}$.
To check that these formulas are $\Sigma_1$, you just need to know that that you can recognize axioms of ACF and proofs in a $\Delta_0$ (i.e. recursive) way.
As for why they work: (1) is completely straightforward, but (2) is a bit more involved. The point is that $\varphi$ is not a consequence of ACF, if and only if it's false in some algebraically closed field $K$, if and only if $\lnot\varphi$ is a consequence of $\text{Th}(K)$. And the complete consistent theories containing ACF are exactly ACF$_p$, where $p$ is a prime number or $0$.