Return to Answer

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.

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$.

(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.)

EDIT: to express RH in Peano Arithmetic, there are two ways.

One is to use Matiyasevich (sp?) theorem that for any halting problem one can construct a Diophantine equation whose solvability is equivalent to halting. Another is to express enough complex analysis in PA to carry the 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 Two Applications Of Logic to Mathematics.

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.

(Concerning the philosophical interest of the $\Pi_1$ formulation of RH, see also the comments under the question.)

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.

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$.

(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.)

EDIT: to express RH in Peano Arithmetic, there are two ways.

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 Hilbert's 10th Problem: Positive Aspects of a Negative Solution. 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 Two Applications Of Logic to Mathematics.

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.

(Concerning the philosophical interest of the $\Pi_1$ formulation of RH, see also the comments under the question.)

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.

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$.

(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.)

EDIT: to express RH in Peano Arithmetic, there are two ways.

One is to use Matiyasevich (sp?) theorem that for any halting problem one can construct a Diophantine equation whose solvability is equivalent to halting. Another is to express enough complex analysis in PA to carry the 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 Two Applications Of Logic to Mathematics.

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, they validate it as high as it holds up the critical line. 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, so 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.

(Concerning the philosophical interest of the $\Pi_1$ formulation of RH, see also the comments under the question.)

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.

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$.

(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.)

EDIT: to express RH in Peano Arithmetic, there are two ways.

One is to use Matiyasevich (sp?) theorem that for any halting problem one can construct a Diophantine equation whose solvability is equivalent to halting. Another is to express enough complex analysis in PA to carry the 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 Two Applications Of Logic to Mathematics.

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.

(Concerning the philosophical interest of the $\Pi_1$ formulation of RH, see also the comments under the question.)

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.

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$.

(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.)

EDIT: to express RH in Peano Arithmetic, there are two ways.

One is to use Matiyasevich (sp?) theorem that for any halting problem one can construct a Diophantine equation whose solvability is equivalent to halting. Another is to express enough complex analysis in PA to carry the 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 Two Applications Of Logic to Mathematics.

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.

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$.

(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.)

EDIT: to express RH in Peano Arithmetic, there are two ways.

One is to use Matiyasevich (sp?) theorem that for any halting problem one can construct a Diophantine equation whose solvability is equivalent to halting. Another is to express enough complex analysis in PA to carry the 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 Two Applications Of Logic to Mathematics.

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, they validate it as high as it holds up the critical line. 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, so 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.

(Concerning the philosophical interest of the $\Pi_1$ formulation of RH, see also the comments under the question.)