[FOM] Eliminability of AC

[Francois G. Dorais]

joeshipman at aol.com wrote:
> 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?

Is there any reason to believe that the V=L proof would be any easier?

Speedups do occur when moving from first-order to second-order logic,
for example. This partly explains why an analytic proof of the prime
number theorem was discovered before an elementary proof. I'm not aware
of any speedup associated with Shoenfield absoluteness. If there is, I
would really like to know.

In any case, I'm pretty sure that you won't find any known arithmetical
theorem whose "easy proof" requires, e.g., using a morass and Shoenfield
absoluteness.

-- 
François G. Dorais
Department of Mathematics
Cornell University