Candidates on proved false arithmetic statements

Questions

Are there any known proved pure existence arithmetic statements? I.e. statements of the form $\exists n P(n)$, for which no upper bound on $n$ is known? If yes, is there some where the predicate expressed by $P(n)$ is computable (i.e. $\exists n P(n)$ is $\Sigma_1^0$ statement)? Is there some as in the first question proved in ZFC and independent of PA? Is there some required AC?

Motivation

The questions are motivated by the problem of arithmetical soundness of ZFC. While arithmetical soundness of PA is doubtless, I'm not so sure about ZFC. The evidence for the former is given by real physical implementation of natural numbers via ordinary counting, which is surely satisfies PA axioms. On the contrary, ZFC reasons about infinite entities, for which such evidence can not be provided. And ZFC proves more arithmetical statements, than PA does ($\mathrm{Con}_{\mathrm{PA}}$ and Paris-Harrington theorem are examples). So, it is a possibility that some of them false, even if ZFC is consistent. It's also related to Hilbert's conservation program.

This conclusion is sad, but I've got a worse one. If ZFC is consistent and arithmetically sound, then it is impossible even to prove the implication $\mathrm{Con}_{\mathrm{ZFC}}\rightarrow \mathrm{ArithmSnd}_{\mathrm{ZFC}}$, where $\mathrm{ArithmSnd}_{\mathrm{ZFC}}$ denotes some internal formalization of arithmetical soundness. I'm not diving into details of how exactly it is defined, but I feel ZFC can formalize this concept, at least because it has the model theory machinery. For my argument the exact definition is not important. What is important is that $\mathrm{ArithmSnd_{ZFC}}$ internally implies that proved to be provable statements are indeed provable, namely $\mathrm{ZFC}\vdash \mathrm{ArithmSnd_{ZFC}}\rightarrow (\Box\Box\varphi\rightarrow\Box\varphi)$, where $\varphi$ is an arithmetical statement and $\Box$ denotes provability in ZFC. Also, according to this answer, the latter is equivalent to arithmetical $\Sigma_1^0$-soundness. In particular, $\mathrm{ArithmSnd_{ZFC}}\rightarrow(\Box\Box\bot\rightarrow\Box\bot)\rightarrow(\neg\Box\bot\rightarrow\neg\Box\Box\bot)\leftrightarrow(\mathrm{Con_{ZFC}}\rightarrow\neg\Box\neg\mathrm{Con_{ZFC}})$, where $\bot$ denotes a contradiction.

So assume ZFC consistent is arithmetically sound and $\mathrm{ZFC}\vdash \mathrm{Con_{ZFC}}\rightarrow \mathrm{ArithmSnd_{ZFC}}$. Then $$\mathrm{ZFC}\vdash \mathrm{Con_{ZFC}}\rightarrow \neg\Box\neg\mathrm{Con_{ZFC}}\\ \mathrm{ZFC}\vdash\mathrm{Con_{ZFC}}\rightarrow \mathrm{Con_{ZFC+Con_{ZFC}}}\\ \mathrm{ZFC}+\mathrm{Con_{ZFC}}\vdash \mathrm{Con_{ZFC+Con_{ZFC}}}.$$ By the second incompleteness theorem, the latter means $\mathrm{ZFC}+\mathrm{Con_{ZFC}}$ is inconsistent, and taking into account the assumption of ZFC consistency, it gives $\mathrm{ZFC}\vdash\neg\mathrm{Con_{ZFC}}$, which contradicts the arithmetical soundness assumption.

As a result, the situation is similar to that with consistency. If ZFC is consistent and arithmetical sound, then there is no hope to prove the implication $\mathrm{Con}_{\mathrm{ZFC}}\rightarrow \mathrm{ArithmSnd}_{\mathrm{ZFC}}$ someday. But, as was mentioned, if ZFC is arithmetically unsound, there exist provable arithmetically false statements, even if it's consistent. And pure existence results are candidates on such statements: ZFC proves $\exists nP(n)$, but in reality such $n$ doesn't exist. So I'm wondering if any such "suspicious" proved results are known.

• Does en.wikipedia.org/wiki/Mills%27_constant fall under your requirements? – Patrick Stevens Mar 11 '18 at 13:04
• "real physical implementation of natural numbers via ordinary counting, which is surely satisfies PA axioms", really? You have physical implementation of infinitely many objects? – Asaf Karagila Mar 11 '18 at 13:04
• @AsafKaragila okay, not so, but we can count, and counting is exactly what PA talks about. – Seriy Mar 11 '18 at 13:32
• @PatrickStevens I'm interested in statements expressible in elementary number theory, and the mentioned talks about reals and seems not expressible in it. Though it's quite close and interesting anyway, thank you. – Seriy Mar 11 '18 at 13:35
• The "motivation" is a little verbose for me to read. Phrases such as "This conclusion is sad, but I've got a worse one." sound more like an essay than a question. Including the motivation is important for the site, but ideally it should be written in a brief and neutral manner. – Carl Mummert Mar 11 '18 at 14:52

I believe there is no upper bound on TREE(3) that is expressible in a more concrete way than by referring back to the TREE function. The fact that TREE(3) exists is expressible by a $\Sigma^0_1$ sentence $(\exists n)\text{TREE}(3,n)$ with parameter $3$.

The fact that TREE($m$) exists for all $m$ is not "suspicious" in my opinion, but the sequence does grow very quickly. See (1) for some info on the TREE sequence and see (2) for this claim:

Theorem (Friedman). TREE(3) is greater than the halting time of any Turing machine initialized with a blank tape, which can be proved to halt in $\text{ACA}_{0} + \Pi^1_2\text{-BI}$ by a proof with at most $2^{1000}$ symbols.

Here BI refers to Bar Induction. The point is that if we had any "nice" upper bound, presumably we would be able to print out the result with a Turing Machine and prove that the machine halts using a reasonable number of symbols. Note that the theorem does not require us to prove that the upper bound is an upper bound, only to construct a machine that prints the upper bound and prove that the machine eventually halts.

Regarding later parts of the question: it is true that ZFC proves more arithmetical sentences than PA. But PA proves every true $\Sigma^0_1$ sentence, so these can never be independent of PA. What tends to happen, as in TREE, is that there is a hidden parameter: e.g. for each $m$, PA proves $(\exists n)\text{TREE}(\dot m, n)$, but PA doesn't prove $(\forall m)(\exists n)\text{TREE}(m, n)$.

ZFC and ZF prove the same arithmetical sentences, so the axiom of choice is not relevant.

• "PA proves every true $\Sigma_1^0$ sentence" what about $\mathrm{Con_{PA}}$? It's $\Sigma_1^0$, isn't it? – Seriy Mar 11 '18 at 15:59
• Con(PA) is a $\Pi^0_1$ sentence. If a $\Sigma^0_1$ sentence $(\exists n)\phi(n)$ is true, then it is true for some $m$, and so $\phi(\dot m)$ is a true formula with only bounded quantifiers, which can be proved in PA using essentially a proof by cases. – Carl Mummert Mar 11 '18 at 16:41
• Ah, of course, I was inattentive. I've kept in mind $\neg\mathrm{Con_{PA}}$, which is $\Sigma_1^0$. – Seriy Mar 11 '18 at 16:58
• Yes, although because the sentence is a true $\Sigma^0_1$ sentence we know that a proof in PA does exist, and we can show any such proof is extremely large. – Carl Mummert Mar 11 '18 at 17:07
• The existence of TREE(3) can be proved in systems of second-order arithmetic much weather than ZF. But, yes, if you don't believe that the system used to prove a theorem is sound then you don't need to believe the theorem is true. – Carl Mummert Mar 11 '18 at 17:15

As described here you can construct over any practical $Σ_1$-sound formal system $S$ a sentence $Q$ such that $S$ proves $Q$ and also that ( if $S$ is $Σ_1$-sound then $Q$ is true but whose shortest proof over $S$ has at least on the order of $2^{10000}$ symbols ). However, I can say with complete confidence that you can never encode or verify any such proof, because it is far too long for the observable universe!

So the answer to your question is yes! Observe that $S$ proves that ( $S$ proves $Q$ ), which is a mere $Σ_1$-sentence that is true in the real-world if $S$ is $Σ_1$-sound, but if you believe that $S$ is $Σ_1$-sound then you must believe that there is no real-world proof of $Q$ over $S$!

The only way out would be if $S$ is not $Σ_1$-sound, but we all want to believe that our foundational system for mathematics is $Σ_1$-sound! So either we have to give up our belief that our foundational system is sound, or we have to accept that it proves an existential sentence that has no real-world witness.

In any case, the very notions of "formal system" and "consistency", not to say "$Σ_1$-soundness", all essentially rely on the (abstract) collection of all finite binary strings or something equivalent, so in some sense it will no longer make sense to ask your question once you accept my claim that the real world does not have an exact embedding of a model of PA. I do not know of any viable way around that...