[FOM] Eliminating AC

[Monroe Eskew]

On Mar 24, 2013, at 6:47 PM, Joe Shipman <JoeShipman at aol.com> wrote:

> This still doesn't help me. Please assume that my mathematical interlocutor understands the axiomatic method, predicate calculus, and what the ZFC axioms actually are and how to derive "ordinary mathematics" from them, but he does not know any technical set-theoretical results about constructibility, absoluteness, etc. 
> 
> 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 don't think this is possible unless you can find a new proof the consistency of ZFC relative to ZF, one that is simpler than going through HOD or L.  Because the statement, "ZFC does not prove arithmetical statements that are not already provable in ZF," is a generalization of the statement, "ZFC is consistent if ZF is consistent."  It would be interesting if you could find such a proof.

Monroe