Elementary theory of finite fields I read on Ax's article that the elementary theory of finite fields is decidable if one assumes the continuum hypothesis to be true. What about if one assumes the hypothesis to be false?
 A: I'm not sure why you say this.  I am right now looking at the following paper of Ax:

MR0229613 (37 #5187)
Ax, James
The elementary theory of finite fields.
Ann. of Math. (2) 88 1968 239--271. 

The first sentence is: "In this paper, we prove the decidability of the theory of finite fields and the theory of p-adic fields."  He goes on in the introduction to explain exactly what this means: given a statement E in the language of rings, he gives an algorithm for determining the set of prime powers q such that E holds in the finite field of order q.  He doesn't say anything about dependence on CH, and I don't see how this could possibly be the case ("decidability given CH" is a far cry from decidability!). 
The only mention of CH in the introduction to the paper is in Theorem B, which states that a certain isomorphism of ultraproducts holds given CH.  This makes more sense, since cardinality questions come into play in the isomorphism of elementarily equivalent objects.
A: 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.


*

*ZFC+CH proves that T is decidable.

*ZFC proves that T is decidable.

*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.
