[FOM] Eliminating AC

[Timothy Y. Chow]

Joe Shipman wrote:

> He knows what a proof from ZFC is, he knows what a proof from ZF is, he 
> prefers the latter, and he wants insight into how, if he has a proof of 
> an arithmetical statement from ZFC, he can find a proof of that 
> statement from ZF that he could then present to his colleagues instead 
> of the proof from ZFC that he currently has.

I'm a little confused at the motivation behind this request.

Does he merely want insight or does he actually want to carry out the 
elimination procedure?  If he actually wants to carry it out, then he's 
evidently willing to put some time and effort into this, so why would he 
be unwilling to put in the time and effort to learn what L is?

Or is the issue that while *he* might be willing to learn what L is, his 
colleagues won't be, and moreover his colleagues won't be impressed if he 
just quotes a theorem that choice is eliminable?  In that case, it sounds 
like he doesn't just want to understand some procedure, any procedure, for 
eliminating choice; he wants a way to convert an *elegant* ZFC proof into 
an *elegant* ZF proof.  Right?  But is there any reason to believe that 
there will always be an elegant ZF proof, if we declare by fiat that L and 
any other specialized concepts from set theory are inelegant?

Tim