# Proof with axiom of choice implies proof without?

Is there a theorem that guarantees the existence of a proof not using AC given there is a proof using AC, at least under some circumstances? What is its name (if there is one) and its most general form?

This of course excludes the trivial cases for example a finite collection of non-empty sets.

-
An enormous number of consequences of AC are specifically known to be independent of ZF, so I rather think that such a result will be either very technical or too narrow to be of much interest. – Brian M. Scott Mar 9 '12 at 15:07

There are important such results, for example the Shoenfield Absoluteness Theorem.

Among other things, it shows that any $\Pi_2^1$ sentence of Peano Arithmetic that (with the usual translation) can be proved in ZFC can already be proved in ZF. (That had already been shown much earlier by Gödel. Shoenfield's result is stronger.) The $\Pi_2^1$ sentences include well-known open problems such as the Goldbach Conjecture, the Riemann Hypothesis, $\text{P}=\text{NP}$, many more.

-
Doesn't the application of Shoenfield Absoluteness require a limit on the complexity of the statement? – arjafi Mar 9 '12 at 15:08
@Arthur Fischer: I was very much oversimplifying. Have changed answer to make it correct. – André Nicolas Mar 9 '12 at 15:18
Your original answer had me starting to think that I was missing something quite trivial. I'm relieved that I wasn't. (At least about this; I'm certain that there are innumerable trivial things that I'm missing.) – arjafi Mar 9 '12 at 15:25
It is not worth editing the answer, but just to clarify potential future confusion, usually $\Pi^1_2$ sentences are considered in second-order arithmetic, and Peano arithmetic is formalized so that it only has arithmetical ($\Sigma^0_\infty$) sentences. – Carl Mummert Mar 11 '12 at 12:13