Is the Riemann Hypothesis equivalent to a $\Pi_1$ sentence? - MathOverflow most recent 30 from http://mathoverflow.net2013-06-19T22:33:29Zhttp://mathoverflow.net/feeds/question/31846http://www.creativecommons.org/licenses/by-nc/2.5/rdfhttp://mathoverflow.net/questions/31846/is-the-riemann-hypothesis-equivalent-to-a-pi-1-sentenceIs the Riemann Hypothesis equivalent to a $\Pi_1$ sentence?Kaveh2010-07-14T12:55:13Z2010-07-23T04:12:36Z
<blockquote>
<p>1) Can the Riemann Hypothesis (RH) be expressed as a $\Pi_1$ sentence?</p>
</blockquote>
<p>More formally,</p>
<blockquote>
<p>2) Is there a $\Pi_1$ sentence which is provably equivalent to RH in PA?</p>
</blockquote>
<p>(This is mentioned in P. Odifreddi, "Kreiseliana: about and around George Kreisel", AK Peters, 1996, on 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.)</p>
<hr>
<h2>Update:</h2>
<p>So we have two proofs that the RH is equivalent to a $\Pi_1$ sentence. </p>
<p>The first is DMR 1974: <a href="http://books.google.ca/books?id=4lT3M6F745sC&pg=PA335" rel="nofollow">http://books.google.ca/books?id=4lT3M6F745sC&pg=PA335</a></p>
<p>$$\forall n >0 \ . \ \left(\sum_{k \leq \delta(n)}\frac{1}{k} - \frac{n^2}{2} \right)^2 < 36 n^3 $$</p>
<p>The second is by J. Lagarias: <a href="http://www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.ps" rel="nofollow">http://www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.ps</a></p>
<p>$$\forall n>60 \ .\ \sigma(n) < \exp(H_n)\log(H_n)$$</p>
<p>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:</p>
<blockquote>
<p>3) Can these two proofs of "RH is equivalent to a $\Pi_1$ sentence" be formalized in PA?</p>
</blockquote>
<hr>
<h2>EDIT : Why is this interesting?</h2>
<p>Here I will try to explain why this question was interesting from Kreisel's viewpoint only.</p>
<p>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: </p>
<ol>
<li>If the RH is false then the theorem holds.</li>
<li>If the RH is true then the theorem holds.</li>
</ol>
<p>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.</p>
<p>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.</p>
<p>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.</p>
http://mathoverflow.net/questions/31846/is-the-riemann-hypothesis-equivalent-to-a-pi-1-sentence/31854#31854Answer by Andres Caicedo for Is the Riemann Hypothesis equivalent to a $\Pi_1$ sentence?Andres Caicedo2010-07-14T13:38:20Z2010-07-14T13:38:20Z<p>Yes. This is a consequence of the Davis-Matiyasevich-Putnam-Robinson work on Hilbert's 10th problem, and some standard number theory. A number of papers have details of the $\Pi^0_1$ sentence. To begin with, take a look at the relevant paper in <strong>Mathematical developments arising from Hilbert's problems</strong> (Proc. Sympos. Pure Math., Northern Illinois Univ., De Kalb, Ill., 1974), Amer. Math. Soc., Providence, R. I., 1976.</p>
http://mathoverflow.net/questions/31846/is-the-riemann-hypothesis-equivalent-to-a-pi-1-sentence/31870#31870Answer by François G. Dorais for Is the Riemann Hypothesis equivalent to a $\Pi_1$ sentence?François G. Dorais2010-07-14T15:51:17Z2010-07-14T15:51:17Z<p>I don't know the best way to express RH inside PA, but the following inequality
$$\sum_{d \mid n} d \leq H_n + \exp(H_n)\log(H_n),$$
where $H_n = 1+1/2+\cdots+1/n$ is the $n$-th harmonic number, is known to be equivalent to RH. [J. Lagarias, <a href="http://www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.ps" rel="nofollow">An elementary problem equivalent to the Riemann hypothesis</a>, Amer. Math. Monthly, 109 (2002), 5347–543.] The same paper mentions another inequality of Robin,
$$\sum_{d \mid n} d \leq e^\gamma n \log\log n \qquad (n \geq 5041),$$
where $e^\gamma = 1.7810724\ldots$, which is also equivalent to RH. Despite the appearance of $\exp,$ $\log$ and $e^\gamma$, it is a routine matter to express these inequalities as $\Pi^0_1$ statement. (Indeed, the details in Lagarias's paper make this even simpler than one would originally think.)</p>
http://mathoverflow.net/questions/31846/is-the-riemann-hypothesis-equivalent-to-a-pi-1-sentence/31942#31942Answer by T. for Is the Riemann Hypothesis equivalent to a $\Pi_1$ sentence?T.2010-07-15T02:32:58Z2010-07-23T04:12:36Z<p>One can write a program that, given enough time, will eventually detect the presence of zeros off the critical line if any exist, by computing contour integrals of
$\zeta' (s)/ \zeta(s)$ on a sequence of small squares (with rational vertices) exhausting increasingly fine finite grids that cover more and more of the critical strip to greater and greater height. </p>
<p>From the formulae for analytic continuation of $\zeta (s) $ one can extract effective moduli of uniform continuity and from that one can approximate the integral by dividing each side of the square into some large number of equal pieces, approximating the function at those rational points, and calculating the Riemann sum. The necessary accuracy can be determined from the modulus of continuity and formulas for $\zeta$. </p>
<p>(The grids I have in mind come within $1/n$ of the sides of the critical strip, with height going from $0$ to $n$, and are divided into squares of size $1/n^2$, so eventually any zero will be isolated inside one such square.)</p>
<p>EDIT: to express RH in Peano Arithmetic, there are two ways. </p>
<p>One is to use Matiyasevich (sp?) theorem that for any halting problem one can construct a Diophantine equation whose solvability is equivalent to halting. Or in the same vein, use Matiyasevich/Robinson approach to Diophantine encode an elementary inequality equivalent to RH, as was done in Matiyasevich-Davis-Robinson's paper on <em>Hilbert's 10th Problem: Positive Aspects of a Negative Solution</em>. Another way is to express enough complex analysis in Peano Arithmetic to carry the contour integral argument above, which can be done because ultimately everything involves formulas and estimates that can be made sufficiently explicit. How to do this is explained in Gaisi Takeuti's essay <em>Two Applications Of Logic to Mathematics</em>.</p>
<p>EDIT-2: re: verifications of RH, the ZetaGrid distributed computation checked that at least the first 100 billion (10^11) zeros, ordered by imaginary part, are on the critical line. The zero computations are opposite to the $\Pi_1$ approach: instead of falsifying RH if it's wrong, if run for unlimited time they would validate RH as far as the program can reach, but could get stuck if there are double zeros anywhere. The algorithms assume RH and whatever other conjectures are useful for finding zeros, such as the absence of multiple roots, or GUE spacings between zeros. Every time they locate another zero, a contour integral then verifies that there are no other zeros up to that height, and RH continues to hold. But if there is a double zero the program could get stuck in an endless attempt to show that it's a single zero. Single zeros off the line would be detected by most algorithms, but not necessarily localized: once you know one is there you can take a big gulp and run a separate program to find it precisely.</p>
<p>(Concerning the philosophical interest of the $\Pi_1$ formulation of RH, see also the comments under the question.)</p>
http://mathoverflow.net/questions/31846/is-the-riemann-hypothesis-equivalent-to-a-pi-1-sentence/31981#31981Answer by Russell O'Connor for Is the Riemann Hypothesis equivalent to a $\Pi_1$ sentence?Russell O'Connor2010-07-15T09:01:39Z2010-07-15T09:01:39Z<p>Andres Caicedo's answer is the correct one, but my comment is too big to fit in a comment box.</p>
<p>Here is a Haskell program that exhibits the Riemann Hypothesis:</p>
<pre><code>rh :: Integer -> Bool
rh n = (h - n'^2/2)^2 < 36*n'^3
where
n' = toRational n
h = sum [1/toRational k|k <- [1..d]]
d = product [product [e j|j <- [2..m]] | m <- [2..n-1]]
e x = foldr gcd 0 [a|a <- [2..x], x `mod` a == 0]
</code></pre>
<p>The Riemann Hypothesis is equivalent to saying that the program <code>rh</code> returns <code>True</code> on all positive inputs. This equivalence is, of course, mathematical equivalence and not logical equivalence. Once we prove or disprove the Riemann Hypothesis it will be known to be mathematically equivalent to a $\Delta^0_0$ statement.</p>