3 ms·
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
by Chinjut 11y ago
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).
- digama 11y agoI 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).