The theory ACF of algebraically closed fields admits quantifier elimination: every formula is equivalent to a quantifier-free formula. This makes ACF decidable, categorical in every infinite cardinality, and strongly minimal. ACF is the canonical example of a complete, model-complete, strongly minimal theory and demonstrates how quantifier elimination unlocks strong model-theoretic structure.
Verify quantifier elimination for ACF by eliminating a single quantifier from a formula, then observe the consequences for decidability and categoricity.
From your work on quantifier elimination, you know that a theory T admits quantifier elimination (QE) if every formula is equivalent, within T, to a quantifier-free formula. From definability, you know that quantifier-free formulas over a field are polynomial equations and inequations. Putting these together: in the theory ACF of algebraically closed fields, every first-order statement about algebraic varieties reduces to a question about whether certain polynomials vanish or not — no "there exists" or "for all" survives in the simplified form. This is a remarkable compression of expressive power.
The proof of QE for ACF uses the following key lemma: any formula of the form ∃y (p₁(x,y) = 0 ∧ ... ∧ pₙ(x,y) = 0 ∧ q(x,y) ≠ 0) is equivalent over ACF to a quantifier-free formula in the variables x alone. The quantifier ∃y is eliminated by computing the resultant of the polynomial system — a classical tool from algebraic geometry that expresses the condition "these polynomials have a common root in y" purely in terms of their coefficients, which are polynomials in x. Algebraic closure is essential: it guarantees that every polynomial of degree ≥ 1 has a root, so there are no obstructions to solving systems that complicate other field theories.
Two major consequences follow from QE. First, decidability: every sentence of ACF (a formula with no free variables) is equivalent over ACF to either ⊤ (true) or ⊥ (false), since quantifier-free sentences with no variables are just truth values. This means you can algorithmically determine whether any first-order statement about algebraically closed fields is a theorem — the theory has a decision procedure. Second, completeness: once you fix the characteristic (0, 2, 3, 5, 7, ...), there is only one complete theory extending ACF. Every two algebraically closed fields of the same characteristic and the same uncountable cardinality are isomorphic — this is categoricity in uncountable cardinals, and it is the cleanest possible behavior a theory can have.
ACF is also strongly minimal: every definable subset of the domain (in one free variable) is either finite or cofinite. This is the minimal possible complexity for a non-trivial theory. Strong minimality implies that the Morley rank (a model-theoretic dimension) is well-defined and coincides with the algebraic-geometric dimension of varieties. This is why ACF is the canonical example in stability theory: every property you want to prove about stable theories — that types are well-behaved, that forking is algebraic independence, that model structure is controlled — works out beautifully and cleanly in ACF, making it the ideal laboratory for developing intuitions before attacking more general theories.