Timeline for Endless controversy about the correctness of significant papers
Current License: CC BY-SA 3.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 15, 2020 at 7:27 | history | edited | CommunityBot |
Commonmark migration
|
|
| Jan 5, 2019 at 15:26 | comment | added | Monroe Eskew | @PeterHeinig I was taught early on that we can resolve such controversies by inching a bit closer to the application formal deduction rules to precisely stated assumptions. I was convinced that in principle, there is a rock bottom to hit. | |
| Jan 5, 2019 at 15:21 | comment | added | Peter Heinig | @MonroeEskew: to a large degree, the non-sequitur type of controversy is nothing else than the familiar platitude that in sentential logic (aka propositional logic, aka zeroth-order logic), ANY true statement follows from ANY true statement. Of course, this kind of coarse implication is not accepted as a mathematical proof. As there is no generally recognized standard of the 'resolution' with which the implication ought to be explained, controversies still abound in practice. | |
| Jan 5, 2019 at 15:14 | comment | added | Peter Heinig | @MonroeEskew: well, there are degrees of clarity and thoroughness of a proposed proof. Needless to say, most proofs still are not being written in a formal proof system, and hence no step in usual paper can be verified mechanically, but needs human judgement to assess. By non-sequitur I mean that (1) an author makes a claim C, (2) an author proposes a proof P, (3) P does not contain any wrong statement, (4) the referee disagrees with the implicit claim that P proves C. Often, this is not easy to justify. Sometimes, the author then writes to the editor denouncing the referee as incompetent. | |
| Jan 1, 2019 at 11:14 | comment | added | Monroe Eskew | I don’t know what to make of the nonsequitur type. If the referee is unable to formulate a specific objection or question, isn’t that more their own problem? | |
| Jan 1, 2019 at 1:14 | comment | added | LSpice | My experience, and the definition in Wiktionary (sense 3), agrees with @AlexKruckman. | |
| Oct 7, 2017 at 3:52 | comment | added | Alex Kruckman | Sorry for the off-topic comment, but: as a native English speaker, I don't think the word "qualm" has a connotation of irony or unjustified concern. For me, it does sometimes have a connotation of a vague or imprecise concern. But I would have no qualms about saying that I have qualms about a proof of type (non-sequitur). | |
| Oct 6, 2017 at 18:53 | comment | added | Peter Heinig | [...] Surely not an intentional 'straw man', yet this is some of those patterns of arguing where an extreme view, which none from the 'other side' ever voiced, is negated. Again, I am not criticizing you, but one should say that the new 'school' of formalization is informed, humble, and 'embraces' incompleteness, and diversity, and what not. They know what they are doing. One of the deepest things VV has said in the relevant lectures is that this is all about reasoning reliably with inconsistent formal systems. This statement contains much in one sentence. We shouldn't continue here. | |
| Oct 6, 2017 at 18:51 | comment | added | Peter Heinig | @JamesSmith: thanks for pointing out. Personally, I like this talk of Neil Strickland very much and watched it at least three times over the last months. I don't think it is an accurate summary to say that he 'mentions some of the same qualms as Voevodsky'. In my understanding of the English language, 'qualm' is always used ironically and criticizingly to mean 'unjustified concern'. I think the concern are justified. While I recognize you didn't say the proponents of formalization say they have "all the answers", this reminds me of (please do not take offense) a 'straw man' argument. [...] | |
| Oct 6, 2017 at 18:33 | comment | added | James Smith | On the subject of formal verification, Neil Strickland gave a talk on the subject. I don't think it's a great talk, but he does mention some of the same qualms as Voevodsky, if that's the way to put it. Personally I don't think formal verification has all the answers, and not only because there is obvious dispute about foundations. I think it is partly, perhaps mostly a problem of culture. | |
| Oct 5, 2017 at 14:35 | history | made wiki | Post Made Community Wiki by Todd Trimble | ||
| S Oct 5, 2017 at 14:11 | history | suggested | David Richerby | CC BY-SA 3.0 |
Replaced image with text, for searchability and accessibility.
|
| Oct 5, 2017 at 13:48 | review | Suggested edits | |||
| S Oct 5, 2017 at 14:11 | |||||
| Oct 5, 2017 at 13:02 | history | edited | Peter Heinig | CC BY-SA 3.0 |
Added a relevant (methodo-)logical suggestion.
|
| Oct 5, 2017 at 12:21 | history | edited | Peter Heinig | CC BY-SA 3.0 |
Typos corrected.
|
| Oct 5, 2017 at 12:16 | history | answered | Peter Heinig | CC BY-SA 3.0 |