Elementary theory of finite fields

Let me explain how Ax eliminates his use of CH in the proof
of decidability.

The point is that if a given proof of
decidability of any first order theory in a countable
language uses CH, then it may be uniformly omitted. Thus,
the decidability of a theory like this can never depend on
CH or on the Axiom of Choice.

Theorem. The following are equivalent, for any first
order theory T in a countable language.

1. ZFC+CH proves that T is decidable.




2. ZFC proves that T is decidable.




3. ZF proves that T is decidable

In particular, if a given proof of decidability uses CH+AC,
then these uses can be omitted.

Proof. Clearly, each statement implies the previous, since
the theories are progressively weaker. Suppose now that we
have a proof that t is decidable, but the proof uses
ZFC+CH. The assertion that T is decidable is a statement of
arithmetic, since it says "there is a computer program,
which accepts all and only the theorems of T and rejects
all other strings." This statement has complexity
Sigma^0_3(T), which is to say, that it is fairly low in the
arithmetic hierarchy (relative to the set of Goedel codes
of T).

Let us now establish that T is decidable by arguing merely
in ZF. Assume that ZF holds in the set-theoretic universe
V. Goedel proved that ZFC+CH holds in the constructible
universe L. This argument relativizes to show that ZFC+CH
also holds in L[T], the constructible universe relative to
T. (Note, the theory T of the question above is actually in
L, so in this case, L[T]=L.) Thus, T is decidable in L[T].
Since this assertion is arithmetic, it has the same truth
value in L[T] as in V, since these two set-theoretic models
have the same arithmetic. So T is decidable. QED

One can push the argument much lower than ZF, down to
something like second order number theory. Of course, what
we would really like is to prove the decidability of T in
PA, but I don't think that this is always possible.
(Although PA proves all true existential statements, the
complexity of the assertion that T is decidable rises above
this.)

The more general fact is that arithmetic statements can never depend on AC or CH, because if one proves them in ZFC+CH, then they would be true in L, and hence true in V, where one might have only ZF. In fact, the same argument shows via
the Shoenfield Absoluteness theorem that a Sigma^1_2
statement is provable in ZFC+CH if and only it is provable
in ZF.

An instance of this would be: Fermat's Last Theorem is
provable in ZFC+CH if and only if it is provable in ZF.
In particular, any use of the Axiom of Choice in Wiles' proof can be
uniformly eliminated.

Edit: I changed the presentation to be clearer.