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

EDIT 2: Just to clarify, when I said "does not follow from the assumption that ZF is sound", I was speaking metamathematically, I wasn't talking about reasoning within the language of ZF. I meant that we shouldn't be obliged to believe either X or its negation just because we believe that the axioms of ZF are true. The axiom of choice is an example of such a statement: if we accept that the axioms of ZF are true, that doesn't compel us to accept either the axiom of choice or its negation. But unfortunately, the axiom of choice doesn't have any new consequences for first-order arithmetic, outside of what ZF already allows us to prove. So I want a statement like that that does have consequences for first-order arithmetic.

Still, if people find it too informal to talk about metamathematical reasoning, we can make things more precise by defining the truth predicate of ZF within NBG set theory, as shown in theorem 1 of (Mostowski 1950): http://matwbn.icm.edu.pl/ksiazki/fm/fm37/fm37110.pdf Or, if @JoelDavidHamkins is right and we can't define a truth predicate within NBG, I'm happy to define the truth predicate within Morse-Kelley set theory instead. But however we formalize it, I hope my intent is clear: I want a statement X such that mathematicians who agree that the axioms of ZF are true can still disagree about whether statement X is true.