[FOM] Eliminating AC
Timothy Y. Chow
tchow at alum.mit.edu
Tue Mar 26 21:21:32 EDT 2013
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?
More information about the FOM