ACF is the theory of algebraically closed fields. Usually one works in the language of rings, with binary operations for multiplication, addition, and subtraction, and constant symbols for $0$ and $1$ .

The theory ACF is not complete, but models are determined up to elementary equivalence by the characteristic of the field. The completions of ACF are therefore the theories $ACF_{0}$ and $ACF_{p}$ for $p$ a prime, where $ACF_{n}$ denotes the theory of algebraically closed fields of characteristic $n$ .

The theory ACF has quantifier elimination in the language of rings. This amounts to Chevalley's result in algebraic geometry that the image of a morphism of varieties is a constructible set (a union of Zariski- locally closed sets). As ACF has quantifier elimination, it is model complete. In fact, it is the model companion of the theory of fields, as well as the theory of integral domains.

Using quantifier elimination, one sees that ACF is strongly minimal: every definable subset of the home sort is finite or cofinite. As a strongly minimal theory, ACF is stable, totally transcendental, and uncountably categorical. Countable categoricity fails, however.

ACF also has elimination of imaginaries.

Types in ACF[]

The transcendental type, the generic type of a variety… ::: ::: :::