Does ZFC prove a sentence in the language of arithmetic that PA+Con(ZFC) cannot prove?

Assume ZFC is consistent.

Then its clear that PA+Con(ZFC) proves a sentence whose translation cannot be proved by ZFC (namely, that ZFC is consistent).

Does ZFC prove a sentence in the language (relativized to $\omega$) of arithmetic that PA+Con(ZFC) cannot prove? I'm guessing "yes."


Yes, of course. An example is the statement that all Goodstein sequences terminate. The point is that this sentence is not only independent of $\mathsf{PA}$, but in fact of the theory resulting from adding to $\mathsf{PA}$ all $\Pi^0_1$ statements true in the standard model of arithmetic. Note that $\mathrm{Con}(\mathsf{ZFC})$ is an example of such a $\Pi^0_1$ statement.

That Goodstein's theorem has this property follows from the standard proof of its independence using the method of indicators: One begins with a nonstandard model of $\mathsf{PA}$; the argument produces an initial segment $I$ that satisfies $\mathsf{PA}$ but where Goodstein's theorem fails. Starting with a model of true arithmetic, the segment $I$ can be arranged to satisfy not just $\mathsf{PA}$, but the true $\Pi^0_1$ theory. A good reference is the book

Petr Hájek, and Pavel Pudlák. Metamathematics of First-Order Arithmetic, 2nd printing, Perspectives in Mathematical Logic, Volume 3, Berlin: Springer-Verlag, 1998. MR1219738 (94d:03001).

(You may find this related answer of some interest.)

Going beyond: Goodstein's theorem is $\Pi^0_2$. Adding all true $\Pi^0_2$ statements to $\mathsf{PA}$ does not prove all true $\Pi^0_3$ statements. Etc. And $\mathsf{ZFC}$ is strong enough to verify all this.