[FOM] Eliminating AC

[François Dorais]

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?

Best wishes,

François G. Dorais