Timeline for When are two proofs of the same theorem really different proofs
Current License: CC BY-SA 2.5
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 5, 2010 at 2:53 | comment | added | Sergey Melikhov | My understanding is that the difficulty is well-known, and the standard solution has been to switch from classical logic to intuitionistic. The references are in my answer in this thread, mathoverflow.net/questions/3776/… | |
| Nov 3, 2009 at 4:33 | comment | added | Reid Barton | I follow you up to the point where you transform "(1) argument A; (2) argument B; (3) conclude X from 1" to "(1) argument A; (2) argument B; (3) conclude X from 2". I can imagine that not being allowed as a "proof homotopy". But certainly you'd have to be careful to ensure that that was the case. | |
| Nov 3, 2009 at 2:49 | comment | added | Aaron Mazel-Gee | Perhaps this issue could be explained using homotopy theory (as Tom mentioned). Adding an irrelevant couple of lines certainly doesn't change the homotopy type of a path, and it's possible that the disjoint union of two sufficient proofs could be interpreted as the concatenation of their paths. (I'll readily admit that I wasn't able to make much headway in the papers Tom linked, so I have no idea if this is actually how things are done...) | |
| Nov 2, 2009 at 11:01 | history | answered | Kevin Buzzard | CC BY-SA 2.5 |