A **difference field** is a field with an endomorphism . The theory of difference fields is inductive, and **ACFA** is its model companion. Therefore, models of **ACFA** are existentially closed difference fields.

ACFA can be explicitly axiomatized as follows. if and only if the following conditions hold:

- is an algebraically closed field
- is an
*automorphism*of , in particular, it is surjective - If is an irreducible affine variety over , and if is the image of under , and if is an irreducible closed subvariety of such that the projection maps and are dominant, and if is a proper closed subvariety of , then there is some such that .

The fact that this third condition is first-order is a little non-trivial, and uses the fact that irreducibility is definable in ACF.

ACFA is supersimple, but not stable. It is probably one of the most important examples of a simple unstable theory. ACFA has elimination of imaginaries. ACFA does *not* have quantifier elimination, but comes very close.

A model of ACFA is determined up to elementary equivalence by the isomorphism class of , where is the algebraic closure of the prime field, and is the restriction of to . Conversely, if is the algebraic closure of a prime field, and is any automorphism of , then some model of ACFA extends , so all the possibilities occur.

The upshot is that the completions of ACFA are in bijection with pairs , where is 0 or a prime, and where is a conjugacy class in , where is the prime field of characteristic .

ACFA does not have quantifier elimination. However, every formula is equivalent to one of the form where is a single variable, is a polynomial, monic in , and is quantifier-free.

If , the fixed field of is pseudo-finite. More generally, it turns out that for any nonzero integer , so the fixed fields of the powers of are also pseudofinite.

In the unpublished paper *The Elementary Theory of the Frobenius*, Hrushovski proves that ACFA is the limit theory of the Frobenius automorphism, in the same sense that the theory of pseudo-finite fields is the limit theory of finite fields.

More precisely, for each prime power , let be the difference field whose underlying field is , and whose automorphism is the th power Frobenius map. Then Hrushovski proves that any non-principal ultraproduct of 's models ACFA. This fact generalizes Ax's theorem that non-principal ultraproducts of finite fields are pseudo-finite. The part of Ax's proof that is hardest to generalize is the Lang-Weil estimates, so Hrushovski is forced to prove "twisted Lang-Weil" estimates, which have some independent interest with algebraic geometers.

Some analogue of the Zilber Trichotomy holds in ACFA (which is unstable). This was proven by Chatzidakis and Hrushovski, maybe, at least in the characteristic 0 case.

As an application, this can be used to give yet another proof of the Manin-Mumford conjecture.

Hrushovski's result on the elementary theory of the frobenius has been used to prove results in algebraic dynamics about periodic points, by Fakhruddin and someone else.

Also, the trichotomy in ACFA has been used by Medvedev and Scanlon to prove results in algebraic dynamics, about periodic varieties.