[FOM] Status of AC

[Robert M. Solovay]

On Wed, 1 Mar 2006, joeshipman at aol.com wrote:

>
> For practically all the most important mathematical questions, the use
> of AC is eliminable, because of metatheorems like Shoenfield's
> Absoluteness Theorem, which ensures that AC can be eliminated from the
> proof of any statement of logical type no higher than Sigma^1_2 or
> Pi^1_2. (In fact, not only AC but allso V=L is eliminable and can
> therefore can be used freely when attempting to prove such statements)

 	One can slightly sharpen this: If a Sigma^1_3 sentence follows 
from V=L it is a theorem of ZFC. This is best possible since "Every real 
is constructible" is Pi^1_3.

 	--Bob Solovay