[FOM] Eliminating AC

[Aatu Koskensilta]

Quoting François Dorais <fgdorais at gmail.com>:

> I had a naive idea regarding elimination of AC which turns out to be
> flawed but I wonder if it could be fixed or permanently shot down.
>
> The naive idea was to replace the uses of AC by uses of finitely many
> Skolem functions and then syntactically eliminate them to get a proof
> without AC nor Skolem functions. Of course, that's not how Skolem
> functions work. We can add a bunch of Skolem functions to get a
> conservative extension of ZF but the comprehension axioms are not
> allowed to use these Skolem functions. For example, we do get a new
> function that picks a representative from each Vitali class, but we
> cannot comprehend the range of that function to form a Vitali set.
> Thus, there is no reason to believe the original ZFC proof of the
> arithmetical statement has a translation in this expansion of ZF.
>
> Is there a refined version of this naive idea that works? Is there a
> way to see that such an argument couldn't possibly work?

   There's nothing in your idea that's specific to arithmetical  
statements, so if it'd work it would show that choice was provable in  
ZF. In a sense a refined version of the idea does work: we can  
eliminate choice in this way when the Skolem (or choice) functions are  
definable. In practice this is often the case.

-- 
Aatu Koskensilta (aatu.koskensilta at uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus