Can different extensions of ZF have contradictory consequences for first-order arithmetic?

Question

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?

Answer 1

Let me, for a moment, follow Joel in taking "sound" to mean arithmetically sound, i.e., all arithmetical statements provable in ZF are true. That fact is expressible as a sentence $S$ in the language of set theory. Then Con(ZFC $+\ S$) is true but not deducible from the soundness assumption $S$.

Now let me suppose instead that you intended soundness to mean more than arithmetical soundness, say, for example, that all ZF-provable statements of higher-order arithmetic are true. That's also expressible as a sentence in the language of set theory, so the same idea as above still gives an example.

To escape from this sort of example, one needs to interpret "soundness" in a way that can't be expressed in the language of ZF. For example, it might mean that every sentence provable in ZF is true in the full universe of sets. Truth in the universe is not expressible in the language of ZF, so you don't get cheap examples as above. But by eliminating the cheap answer, this version of soundness raises questions about the very meaning of the question. What does it mean for something to "follow from" soundness, when soundness can't be expressed in the language of set theory? You'd need to explain (at least) what sort of deductions are intended by "follow".

Answer 2

Since you want ZF+X to prove P and ZF+$\neg$X to prove $\neg$P, it follows that X is equivalent to P. So basically, you are asking for an arithmetic assertion that is independent of ZF, but which satisfies your requirement that it "not follow from the assumption that ZF is sound".

Of course, there are plentiful arithmetic assertions that are independent of ZF, provided that ZF is consistent, such as the Rosser sentence for ZF. But presumably this doesn't satisfy your requirement.

If large cardinals are consistent, then we get more examples. For example, Con(ZF + there is a measurable cardinal) is thought by many set theorists to be true, and in this case it is not provable in ZF, since it implies Con(ZF). But one cannot deduce that it is true just from the assumption that ZF proves only true arithmetic assertions, since if ZF is consistent, then it is consistent with ZF that this assertion is false, yet ZF has an $\omega$-model and hence is arithmetically sound. (This is because the assumption that ZF has an $\omega$-model has weaker consistency strength than a measurable cardinal.)

This reasoning shows that for any consistent theory T whose consistency strength is stronger than an $\omega$-model of ZF (and this includes all of the usual large cardinals), then Con(T) will be an example of a statement independent of ZF yet not deducible merely from the fact that ZF is arithmetically sound.

Update. You have explained that you want to find an arithmetic statement independent of ZF and not provable from the assumption that ZF is sound, where this is formalized in Kelley-Morse set theory.

Indeed, the soundness of ZF is formalizable in KM, since this theory proves the existence of a full satisfaction class for first-order truth. And so in KM we can formulate the assertion $S$ that says "every theorem of ZF is true". Indeed, S is a theorem of KM, which can be seen by induction on the length of proofs, since we have a truth predicate for first-order truth.

So the example sentence $P$ you seek could just be Con(KM). If true, this will be independent of ZF, and you cannot prove it from the assumption that ZF is sound, since then you could prove it in KM, which you cannot by the incompleteness theorem.

(But since you've made the move from ZF to KM, one might think you now want to consider statements P independent of KM, which are not deducible from the "soundness" of KM, and we would be back to the essence of the earlier objections, one level up.)

Answer 3

Harvey Friedman has discovered a number of arithmetic (actually, $\Pi^0_1$) statements of combinatorics which are independent of $ZFC$. This is part of his ongoing research project, "Boolean Relation Theory" (see http://www.math.osu.edu/~friedman.8/pdf/BoolRelnThyNotes100601.pdf).

Now, since these statements follow from (in fact, are equivalent to) the consistency of large cardinal propositions, it's not clear that they are what you are looking for; but you may still find them interesting.