[FOM] Eliminating AC

[Joe Shipman]

No, he understands that there is not going to be a simple and elegant procedure to transform the proof that works in a completely general way. That is why I was careful with my words. What I said is that he wants INSIGHT as to why Choice is eliminable that would facilitate his finding a Choice-free proof if he already has one that uses choice.

-- JS

Sent from my iPhone

On Mar 26, 2013, at 9:21 PM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

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
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom