My question is basically, does there exist a statement X independent of ZF such that ZF + X implies a statement P of first-order arithmetic, but ZF + not X implies not P? Now X cannot be the axiom of constructibility due to Schoenfield's absoluteness theorem, which states that the axiom of constructibility, and thus its consequences like the axiom of choice and the continuum hypothesis, can't be used to prove any statement of first-order arithmetic that you couldn't already prove using ZF: http://en.wikipedia.org/wiki/Absoluteness#Shoenfield.27s_absoluteness_theorem Also, there are examples like Con(ZF), but they're not really interesting, because obviously Con(ZF) is a true statement assuming that ZF is sound. So I'm specifically looking for statements X whose truth value cannot be deduced from the assumption that ZF is sound. So perhaps a preliminary question should be, does there exist any statement independent of ZF which can prove statements of first-order arithmetic that ZF can't prove, but whose truth value does not follow from the assumption that ZF is sound? Any help would be greatly appreciated. Thank You in Advance. EDIT: This is based on a question of mine from Math.Stackexchange: http://math.stackexchange.com/questions/467017/do-the-axiom-of-choice-and-its-negation-have-contradictory-consequences-for-arit