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:

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). 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.

EDIT 3: I've come to realize that consistency statements Con(T) don't satisfy what I'm trying to ask, because the only warrant of their independence from ZF is that we assume that the underlying theory T is in fact consistent. Because if the theory were inconsistent, then the falsehood of Con(T) could be proven in ZF and even in PA. The reason for that is that consistency statements are all Pi_1 statements, and every false Pi_1 statement can be proven wrong in PA and thus ZF. So I want the arithmetical statement P to be higher up in the arithmetical hierarchy than Pi_1.

Now, as @WillSawin has pointed out, it's easy to show that there are truths of first-order arithmetic that are independent of ZF + (All Pi_1 truths), because otherwise an oracle who could decide Pi_1 truths would be able to decide all truths of first-order arithmetic, which is obviously wrong. So we know that such a statement exists. But I would prefer to have a concrete statement, not just a proof that a statement exists.

And more importantly, while I do want P to be a statement of first-order arithmetic, I would prefer that X not be a statement of arithmetic. I want X to be a set-theoretic statement that's not an arithmetic statement, something like the axiom of choice, the continuum hypothesis, or a large cardinal axiom. The fundamental intent of my question is, can there be an unfalsifiable disagreement about which set theory is correct, which leads to an unfalsifiable disagreement about which statements of first-order arithmetic are correct? As noted above, Schoenfield's absolute theorem rules out the axiom of choice and the continuum hypothesis, and this answer to my Math.SE question suggests that large cardinals won't work either. So does anyone know any non-arithmetical set-theoretic statement, independent of ZF, which implies a non-Pi_1 statement of first-order arithmetic that's independent of ZF?

Metamathematics of first-order arithmetic, where most of this is covered carefully. $\endgroup$ – Andrés E. Caicedo Aug 15 '13 at 3:32