Definition 9.1 (ACF). $\mathrm{ACF}$ is the $L_{\text{rings}}$ theory axiomatising algebraically closed fields. It consists of:

• field axioms

• for every $d\ge 1$, we add an axiom:

  $$\forall v_0,\dots ,v_d,\exists x(v_d\ne 0⟹v_0+v_{1}x+\cdots +v_d{x}^d=0).$$