News for hackers. Stuff that matters.

A comment on Will Computers Redefine the Roots of Math?. Parent comment

Re:Will Computers Redefine the Roots of Math? by yaantc on Wednesday May 20, 2015 @05:24AM (#9575255)
The typical way to prove that there is an infinity of primes is to do a reductio ad absurdum: you assume there is a finit number of primes, call the biggest P and build another bigger one that is prime. This is a contradiction, so you can conclude that there is no highest prime and hence there is an infinity of them.

The thing here is that this uses the law of the excluded middle: a proposition is either true or false, there is no other possibility. That's the basis of a proof using reduction ad absurdum. But that's not part of Coq (or any P.A. based on constructive logic) by default. If one is not aware of this indeed doing this proof will be impossible in Coq. This said Coq can work with the law of excluded middle (so support classical logic), but you have to explicitly assert it and use it.

This being said, I haven't tried this proof in Coq ;) Just seeing this point as something to take into account, and that may be a problem for some people new to Coq and not aware of it.

[ Parent | on HN ]
Re:Will Computers Redefine the Roots of Math? by Chinjut on Wednesday May 20, 2015 @02:41PM (#9578263)
Proving NOT P by showing a contradiction follows from P is perfectly fine in intuitionistic logic (the sort used in Coq), and not dependent upon the law of the excluded middle in that sense. What's not available to you is proving P by showing that a contradiction follows from NOT P (rather, you end up with NOT NOT P, which is not assumed to entail P simpliciter).
[ Parent | on HN ]
Re:Will Computers Redefine the Roots of Math? by digama on Wednesday May 20, 2015 @07:24PM (#9580025)
I believe that in the context of the infinitude of primes, this is the difference between "NOT (finitely many primes)" and "infinitely many primes", where "infinitely many" means that the primes are in bijection with the natural numbers (and of course finitely many means in bijection with some natural number). A proof by contradiction will only give the weaker first statement in intuitionistic logic.

One explanation for why many people say that Euclid's proof is not a proof by contradiction is because you can actually get the second statement with only a little more care (i.e. n!+1 has a prime divisor, which is thus greater than n).

[ Parent | on HN ]