Timeline for Are there examples of nonconstructive metaproofs?
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 8, 2011 at 22:23 | comment | added | Kevin Buzzard | I once spent 5 hours, as an undergraduate, trying to do a certain homework problem about top spaces (proving that if they had certain properties then they were metrizable). I gave up and admitted defeat and showed up at my supervision, where my supervisor took one look at the question and said "that's not true! The Stone-Cech compactification of the integers is a counterexample!" and I said "the what??". | |
| Jun 8, 2011 at 19:19 | vote | accept | skeptical scientist | ||
| Jun 8, 2011 at 16:35 | comment | added | Andrej Bauer | Another example is completeness of Grothendieck toposes for higher-order intiotionistic logic. I think the proof is classical, and it's not clear how to make it intuitionistic. | |
| Jun 8, 2011 at 16:34 | comment | added | Andrej Bauer | Isn't there some question on how to show intuitionistically that Kripke models are complete for first-order intuitionistic (single-sorted) theories. Isn't the usual proof classical? | |
| Jun 8, 2011 at 16:19 | answer | added | Noah | timeline score: 0 | |
| Jun 8, 2011 at 16:03 | comment | added | Emil Jeřábek | @Qiaochu: you are very optimistic about the infallibility of your teacher. | |
| Jun 8, 2011 at 16:03 | comment | added | skeptical scientist | Isn't there a story where a famous mathematician was assigned an open problem as homework by a devious professor, and ended up solving it? | |
| Jun 8, 2011 at 16:01 | comment | added | Qiaochu Yuan | Sure. Metatheorem: any question I get on my homework has a proof. Metaproof: suppose otherwise. Then it would not be on my homework. | |
| Jun 8, 2011 at 15:58 | answer | added | Emil Jeřábek | timeline score: 24 | |
| Jun 8, 2011 at 15:48 | answer | added | David Harris | timeline score: 5 | |
| Jun 8, 2011 at 15:30 | history | asked | skeptical scientist | CC BY-SA 3.0 |