4
$\begingroup$

Recently I was reading again this propositions as types paper by Philip Wadler:

http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf

It gives an impression, that programs are proofs. So my first question was that why they are not enough for mathematical proofs then, for example in case of Riemann Hypothesis. Billions of zeros on critical line have been calculated in many many ways. I suppose they use some sophisticated algorithms or computer programs in that sense.

http://mathworld.wolfram.com/pdf/posters/Zeta.pdf

So, I was just stuck there. Why aren't these programs, or proofs in the system of Curry–Howard correspondence, enought?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
6
$\begingroup$

The fact of the matter is, if a proof exists, then a Curry-Howard version of the program exists too. That doesn't mean that it's easy to find, though.

Undecidability still holds for Curry-Howard: if your types are advanced enough to capture logic, then there's no algorithm which takes in a type and outputs a program of that type, if it exists. Just like there's no algorithm that looks at a proposition and tells you if it's true or not.

Billions of zeros on critical line have been calculated in many many ways.

Curry-Howard does not say that a program to compute zeroes can be turned into a proof of the Reimann hypothesis. It doesn't say that any program is a proof. What it says is, there is a dependently typed programming language where there's a type corresponding to the Reimann hypothesis, and a program with that type iff there's a proof of the Reimann hypothesis.

What this program would actually look like, if it's a proof, is a function that takes a number and a proof that that number is a zero of the Zeta function, and outputs a proof that that number is either a negative integer or has complex part 1/2. (Notice how the type of the input proof depends on the value of the given input, this is the "dependent" of dependent types).

Improve this answer
$\endgroup$
3
  • $\begingroup$ Informative and explanatory for me, thanks! $\endgroup$
    – MarkokraM
    Dec 12, 2017 at 8:09
  • $\begingroup$ Btw. do you mean with "there's no algorithm which takes in a type and outputs a program of that type, if it exists" that there is no way of being sure, that output type is same as the input type, or exactly, that there can't be such a program? $\endgroup$
    – MarkokraM
    Dec 12, 2017 at 8:51
  • $\begingroup$ @MarkokraM I mean no such algorithm can exist. We're not talking about types of the algorithm, but at a meta level, talking about taking types as inputs. See also en.m.wikipedia.org/wiki/Entscheidungsproblem $\endgroup$
    – jmite
    Dec 12, 2017 at 8:57
2
$\begingroup$

The programs that you describe are very good at searching for zeroes in an interval; they can find all of the zeroes of the form $s+it$ between $t=0$ and $t=10^9$, say, and show that all these zeroes have $s=\frac12$. But that upper bound is critical, because it defines the search space. RH is the statement that all of the zeroes lie on the critical line, and no serial analysis of the zeroes within a given range will ever answer the question for all zeroes (so far as we know). What you're asking is exactly analogous to asking 'we've written programs to show that the Goldbach Conjecture is true for the first $n$ numbers, so why don't those programs constitute a proof that it's true for all numbers?'.

Improve this answer
$\endgroup$
1
  • $\begingroup$ For some reason I was thinking that those programs could have run forever but for practical reason they were halted at some point. On the other hand, analogy to calculating prime numbers can be made. It has been prooved since Erastothenes that are infinitely many primes but supposedly the actual computer program to sieve primes does not necessarily prove infinityness? Is that true? Also, could any computer program actually prove it? Maybe a question good for separate topic... $\endgroup$
    – MarkokraM
    Dec 13, 2017 at 5:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.