Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
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
up vote 10 down vote accepted

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.

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.