Timeline for "Strange" proofs of existence theorems
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 12, 2018 at 17:54 | comment | added | usul | Here's what's different about this proof and the strategy-stealing one below. Explicitly construct candidate A. Case 1, A satisfies the criteria. Case 2, leverage A to construct new candidate B and proves B works using the assumption that A is a nonexample. We end with a pair of candidates one of which works, but no guarantee which. So it's "partially constructive", especially depending on the magic that gave us B. I think excluded middle is somewhat of a red herring (it can be proven constructively in some cases), as are mere proofs of the form "Assume P. Or assume not P. In both cases Q." | |
| Oct 12, 2018 at 5:31 | vote | accept | Joseph Granata | ||
| Oct 12, 2018 at 5:31 | |||||
| Oct 11, 2018 at 23:46 | comment | added | Mario Carneiro | @CarlMummert The scheme $\bot\to\phi$ is not proof by contradiction, it is the principle of explosion or ex falso quodlibet. Proof of $\neg\phi$ by assuming $\phi$ and deducing $\bot$ is also not a proof by contradiction, although this is often mistaken for proof by contradiction. I don't think this proof principle has a special name, it's just the definition of $\neg$. I guess you could call it negation introduction? | |
| Oct 11, 2018 at 22:58 | comment | added | KConrad | @GerryMyerson, that first proof the class number conjecture was not about GRH and its negation, but more precisely about GRH for $L$-functions of imaginary quadratic fields or its negation. The proof couldn't make any use of a hypothetical counterexample to GRH for some other type of $L$-function. | |
| Oct 10, 2018 at 20:49 | comment | added | Gerry Myerson | Gauss' conjecture on class numbers of imaginary quadratic fields is an example of something that was first proved by showing that it's a consequence of both the (generalized) Riemann hypothesis and of its negation. | |
| Oct 10, 2018 at 20:42 | comment | added | Joseph Granata | Yeah, I think you’re onto what I’m thinking of. I also agree that this is conceptually and technically different from a contradiction | |
| Oct 10, 2018 at 19:38 | comment | added | Carl Mummert | @RobertFurber I don't know of one if there is. There is also the proof by contradiction axiom scheme $\bot \to \phi$ which is generally included in intuitionistic logic ("every formula $\phi$ follows from a contradiction") | |
| Oct 10, 2018 at 19:36 | comment | added | Robert Furber | @CarlMummert Oh, I see you are using "proof by contradiction" in a different manner from me. To me it means proving $P$ by assuming $\lnot P$ and producing a contradiction, which in intuitionistic logic only produces a proof of $\lnot\lnot P$, not of $P$. Of course, if instead you want to prove $\lnot P$, the way you do it in both classical and intuitionistic logic is to assume $P$ and deduce a contradiction. Is there a standard terminology for distinguishing these two cases? | |
| Oct 10, 2018 at 19:29 | comment | added | Carl Mummert | @RobertFurber: indeed, what is not clear to me is whether the OP considers this the same as proof by contradiction. Of course intuitionistic logic has proof by contradiction but not excluded middle, so in general the two techniques are not always the same. | |
| Oct 10, 2018 at 19:25 | comment | added | Robert Furber | @CarlMummert It's a proof that uses excluded middle in an essential fashion, which is nonconstructive in the same manner as a proof that relies on converting a double negative to a positive. | |
| Oct 10, 2018 at 16:43 | history | edited | Sam Hopkins | CC BY-SA 4.0 |
added 12 characters in body
|
| Oct 10, 2018 at 16:33 | review | Suggested edits | |||
| Oct 10, 2018 at 16:43 | |||||
| Oct 10, 2018 at 16:02 | comment | added | Carl Mummert | I was not sure if this counted as a proof by contradiction to the OP, but I also think it is a different kind of proof, just a proof by cases. Similarly, I think there are some results I can't remember where the proof goes by cases depending on whether the continuum hypothesis holds, but in each case the same result is obtained. | |
| Oct 10, 2018 at 14:49 | comment | added | Sam Hopkins | Whoops, I didn’t see this was mentioned by Carl Mummert in the comments. | |
| Oct 10, 2018 at 14:48 | history | answered | Sam Hopkins | CC BY-SA 4.0 |