[FOM] Eliminability of AC

[joeshipman@aol.com]

One month ago, I noted the standard result that any use of the Axiom of 
Choice could be eliminated from proofs of arithmetical statements, and 
indeed from proofs of Sigma^1_2 statements, and asked the question:

What is the simplest example of a well-known open problem  in "ordinary 
mathematics" (that is, one of interest to mathematicians in general and 
not primarily of interest to logicians and set theorists) where there 
is a possibility some form of Choice is needed for any proof?

No one was able to provide one that met all three criteria (well-known 
AND open AND outside of logic and set theory), so I conclude that 
mathematicians outside of logic and set theory do not care about the 
Axiom of Choice anymore -- they are only interested in questions that 
are sufficiently absolute that their truth value does not depend on AC.

It is possible that this increased emphasis on concrete problems 
compared to several decades ago is a reaction to forcing and the 
independence proofs, combined with the failure to isolate sufficiently 
plausible or useful new axioms.

Since AC is an axiom one may use without explicit mention and still 
have a publishable paper, I don't see any remarks in current 
mathematical literature outside of logic and set theory that proofs do 
or do not depend on AC. This is more evidence that mathematicians do 
not care about AC.

But Shoenfield Absoluteness goes further: not only may AC be eliminated 
 from the proofs of arithmetical or Sigma^1_2 statements; so may V=L, a 
much stronger axiom. Can anyone provide examples, particularly 
arithmetical ones, of theorems outside of logic and set theory which 
were first proven (or are most easily proven) by showing they follow 
from V=L and then applying Absoluteness?

-- Joe Shipman