Gödel's speed up theorem and Matiyasevich polynomials

Unless I am sadly mistaken, there should exist a polynomial $P\in\mathbb Z[X_1,X_2,\dots, X_n]$ coding for the speed-up theorem (for, say, ZFC), i.e. having the following properties : 1) P has an integer root (i.e. $\exists (k_1,\dots,k_n)\in\mathbb N^n, P(k_1,\dots,k_n)=0$) 2) P is explicit (i.e. n , the number of monomials of P, and the coefficients are all small (say $<10^4$). 3) The smallest proof of 1) in ZFC has more than $10^{10^{100}}$ symbols but 4) There exists a short (not much longer than P itself) proof of 1) in ZFC + Consis (ZFC)

a) Am I right ? b) is it obvious then that one of the $k_i$ is greater than $10^{10^{99}}$ ? c) and that all of the $k_i$ (of the smallest solution) are computable ?

• Regarding (c), what would it mean for a particular natural number k to not be computable? Every natural number is computable. – Joel David Hamkins Apr 28 '14 at 18:26
• Well, if I have a proof in ZFC that there exist k such that f(k)=0 (where f is recursive),I have usually no way to exhibit such a k (so long as I have no bound for it). But in the particular case of P, I would suspect an explicit bound exists (but it should be much higher than $10^{10^{100}}$) – Feldmann Denis Apr 28 '14 at 18:54

In Gödel's speed-up theorem, one may consider the statement $\sigma$, asserting that "there is no proof of $\sigma$ in PA of length less than a googolplex symbols." Now, if there were a short proof of $\sigma$, in less than a googolplex symbols, then we would be able to prove that the proof had that property, and thereby prove a contradiction in PA. So if PA is consistent, then $\sigma$ is true. Meanwhile, assuming again that PA is consistent, then we can also see that $\sigma$ is actually provable in PA, by enumerating all the proofs. So we see that in fact PA proves $\sigma$, but only by a very long proof, whereas PA+Con(PA) provides a very quick proof of $\sigma$ by formalizing the argument we have just given.
Now, by the MRDP theorem, there is an integer polynomial $p(x,\vec x)$ such that $p(k,\vec k)=0$ for integers just in case $k$ codes a proof of $\sigma$ in PA. Although the coding of c.e. sets into diophantine equations is complicated, it is ultimately managable, and one can get an explicit polynomial $p$. I haven't worked out the polynomial explicitly — and I don't intend to do so — but I believe that the particular bounds that you mention are not unreasonable. It may be useful to compare with this polynomial, whose solutions are exactly the primes. The difficulty of the primeness representation seems basically comparable to yours, and this is why I think your bounds are reasonable.
So what we have is a comparatively small polynomial $p(x,\vec x)$, such that PA proves that $\exists k,\vec k\ p(k,\vec k)=0$ and furthermore proves that any such $k$ will be the code of a proof of $\sigma$ in PA. Thus, there can be no short proof of this. But meanwhile, PA+Con(PA) proves $\exists k,\vec k\ p(k,\vec k)=0$ by a very short proof, which simply formalizes our argument above. So we've got all your desired properties.
So I think (a) you're basically right; (b) yes, the $k$'s must be large, for otherwise we could have a short proof of $\sigma$ just by evaluating $p(k,\vec k)=0$, combined with the fact that PA proves (by a short proof) that any such $k$ must code a proof of $\sigma$. Regarding statement (c), however, I don't think it makes any sense, because every particular natural number is computable, by the algorithm that simply writes it down. If it was merely bounds on $k$ that you wanted, these are provided by the size of the proof of $\sigma$ in PA, which proceeds by enumerating all proofs of size less than a googolplex symbols, and noting that it is not a proof of $\sigma$.
• There are still a few open questions here : in PA, I believe there is no way to prove the existence of a zero except by essentially exhibiting it. But I asked the question for ZFC, where it could happen that a very long (and still non-constructive) proof exists, but no way to exhibit a k (for instance, becaus the theorem would be false without AC). Is there a way to force P to have "explicit" zeos ? (edit) Sorry, I didn't read your last line. So you mean that the zeros of P are essentially explicitly computed by coding the proof ($\sigma$) for the theorem ? – Feldmann Denis Apr 29 '14 at 3:30
• We can describe explicit but very long proofs of $\sigma$, and this provides an upper bound on the zeros of $p$, which are exactly the codes of such proofs. There are likely other somewhat shorter proofs (but still very long), which, say, handle big chunks of the cases at once, but they must still be very long, since after all there is no short proof. – Joel David Hamkins Apr 29 '14 at 10:17