1) Can the Riemann Hypothesis (RH) be expressed as a $\Pi_1$ sentence?
More formally,
2) Is there a $\Pi_1$ sentence which is provably equivalent to RH in PA?
Update (July 2010):
So we have two proofs that the RH is equivalent to a $\Pi_1$ sentence.
- Martin Davis, Yuri Matijasevic, and Julia Robinson,
"Hilbert's Tenth Problem. Diophantine Equations: Positive Aspects of a Negative Solution", 1974.
Published in "Mathematical developments arising from Hilbert problems", Proceedings of Symposium of Pure Mathematics", XXVIII:323-378 AMS.
Page 335 $$\forall n >0 \ . \ \left(\sum_{k \leq \delta(n)}\frac{1}{k} - \frac{n^2}{2} \right)^2 < 36 n^3 $$
2. Jeffrey C. Lagarias, "An Elementary Problem Equivalent to the Riemann Hypothesis", 2001 $$\forall n>60 \ .\ \sigma(n) < \exp(H_n)\log(H_n)$$
But both use theorems from literature that make it difficult to judge if they can be formalized in PA. The reason that I mentioned PA is that, for Kreisel's purpose, the proof should be formalized in a reasonably weak theory. So a new question would be:
3) Can these two proofs of "RH is equivalent to a $\Pi_1$ sentence" be formalized in PA?
Motivation:
This is mentioned in P. Odifreddi, "Kreiseliana: about and around George Kreisel", 1996, page 257. Feferman mentions that when Kreisel was trying to "unwind" the non-constructive proof of Littlewood's theorem, he needed to deal with RH. Littlewood's proof considers two cases: there is a proof if RH is true and there is another one if RH is false. But it seems that in the end, Kreisel used a $\Pi_1$ sentence weaker than RH which was sufficient for his purpose.
Why is this interesting?
Here I will try to explain why this question was interesting from Kreisel's viewpoint only.
Kreisel was trying to extract an upperbound out of the non-constructive proof of Littlewood. His "unwinding" method works for theorems like Littlewood's theorem if they are proven in a suitable theory. The problem with this proof was that it was actually two proofs:
- If the RH is false then the theorem holds.
- If the RH is true then the theorem holds.
If I remember correctly, the first one already gives an upperbound. But the second one does not give an upperbound. Kreisel argues that the second part can be formalized in an arithmetic theory (similar to PA) and his method can extract a bound out of it assuming that the RH is provably equivalent to a $\Pi_1$ sentence. (Generally adding $\Pi_1$ sentences does not allow you to prove existence of more functions.) This is the part that he needs to replace the usual statement of the RH with a $\Pi_1$ statement. It seems that at the end, in place of proving that the RH is $\Pi_1$, he shows that a weaker $\Pi_1$ statement suffices to carry out the second part of the proof, i.e. he avoids the problem in this case.
A simple application of proving that the RH is equivalent to a $\Pi_1$ sentences in PA is the following: If we prove a theorem in PA+RH (even when the proof seems completely non-constructive), then we can extract an upperbound for the theorem out of the proof. Note that for this purpose, we don't need to know whether the RH is true or is false.
Note: Feferman's article mentioned above contains more details and reflections on "Kreisel's Program" of "unwinding" classical proofs to extract constructive bounds. My own interest was mainly out of curiosity. I read in Feferman's paper that Kreisel mentioned this problem and then avoided it, so I wanted to know if anyone has dealt with it.