Timeline for Community experiences writing Lamport's structured proofs
Current License: CC BY-SA 2.5
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 16, 2020 at 11:42 | comment | added | user82537 | Related: there is a question on Math SE about identifying the mistake in Kelley's proof — Lamport claims there is an error in Kelley's proof of the Schroeder-Bernstein theorem. What is it? | |
| Feb 4, 2016 at 11:28 | comment | added | darij grinberg | Related: academia.stackexchange.com/questions/52435/… | |
| Aug 19, 2010 at 11:12 | comment | added | Jyotirmoy Bhattacharya | Typo in last line above: "each element y in B". | |
| Aug 19, 2010 at 11:10 | comment | added | Jyotirmoy Bhattacharya | @Pete. Elaborating on @Russell. Using the notation from Kelley (books.google.co.in/… ) p. 28, I think his claim that "f maps A_E onto B_O" is not correct since x might already belong to the set of ancestors of x. For eg. if f is onto and g=f^{-1} then each element x in A has exactly two ancestors {x,f(x)} and each element in y also has exactly two ancestors {y,g(y)} | |
| Aug 16, 2010 at 20:02 | comment | added | Russell O'Connor | @Pete I looked at it 5 years ago and had trouble spotting the error. But when I went to formalized Kelley's proof in Coq I found an error. It was something about neglecting the possibility of an element x being its own ancestor. | |
| Aug 16, 2010 at 8:58 | comment | added | Pete L. Clark | Lamport's article says that there is a mistake in Kelley's proof of Schroeder-Bernstein. But he doesn't say what the mistake is (maybe he does that to reinforce his point that mistakes are hard to find, but nevertheless I wish he did explicitly identify the error). Does anyone know whether this mistake has been found and acknowledged by others? | |
| Aug 16, 2010 at 8:36 | answer | added | Neel Krishnaswami | timeline score: 22 | |
| Aug 16, 2010 at 5:39 | history | edited | Anthony Pulido | CC BY-SA 2.5 |
clarification
|
| Aug 16, 2010 at 5:30 | history | asked | Anthony Pulido | CC BY-SA 2.5 |