Timeline for True by accident (and therefore not amenable to proof)
Current License: CC BY-SA 4.0
28 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Nov 5, 2023 at 11:02 | comment | added | Manfred Weis | I'd prefer "evidently true" over "true by accident" to put the emphasis on the limited ressources that are available for finding counter examples or for disproving the conjecture because of the length of such a proof. | |
Apr 5, 2023 at 22:05 | comment | added | LSpice | Why should something that is true by accident be therefore not amenable to proof? I can buy that the two things often occur together, but not that the first implies the second. For example, it is surely, in any reasonable sense, only true by accident that my name is what it is, but nonetheless I can prove easily that that is my name. | |
Aug 12, 2022 at 8:00 | history | edited | Martin Sleziak | CC BY-SA 4.0 |
added 1 character in body
|
Nov 3, 2021 at 15:12 | comment | added | Timothy Chow | I'm intrigued by the idea that the length of the shortest proof of S(n) tends to infinity as n tends to infinity. But consider P(n) = "there is no PA proof of 0=1 of length at most n". For any n, PA proves P(n), but the proofs get longer and longer. Moreover, PA doesn't prove ∀n P(n). On the other hand, I would say that ∀n P(n) is true for a reason; namely that the natural numbers exist. If you buy this argument, then sometimes things are true for a reason, but they're still not amenable to proof, because our methods of proof suffer from an intrinsic limitation. | |
Sep 1, 2011 at 2:29 | history | edited | Gordon Royle | CC BY-SA 3.0 |
Response to first round of replies; added 4 characters in body
|
Sep 1, 2011 at 2:05 | vote | accept | Gordon Royle | ||
Aug 26, 2011 at 20:17 | comment | added | Timothy Chow | @Neil: Suppose the shortest possible proof of some theorem involves case-by-case checking of the list of finite simple groups, but there is a longer "conceptual" proof. Does this make the theorem "true by accident"? I wouldn't say so. Neither the length of the proof nor the number of cases one needs to check counts decisively in my mind. "Obscure" properties may become less so the more you familiarize yourself with them. | |
Aug 26, 2011 at 13:55 | comment | added | Neil Strickland | It's conceivable that the shortest possible proof (in some specified system, say HOL light) of the conjecture is 17241 pages long and involves examination of 3261 cases of special configurations of large subgraphs with various obscure properties. In that case I would say that the conjecture is 'true by accident' even though it is provable. | |
Aug 26, 2011 at 12:56 | answer | added | Gil Kalai | timeline score: 29 | |
Aug 26, 2011 at 2:39 | comment | added | Daniel Mehkeri | @Carl: And the procedure could be made to always work, in the sense of either reconstructing the graph or refuting the conjecture. (And of course it's infeasible anyway.) | |
Aug 26, 2011 at 2:28 | comment | added | Daniel Mehkeri | Well, the last paragraph has: can't be proved or disproved, but not formally undecidable. If we interpret "can" ideally, like most here seem to, then the desired formalisation is simply $\bot$. But for most values of "can", I can not always find a witness to a true $\Sigma^0_1$ sentence! | |
Aug 25, 2011 at 22:39 | comment | added | Qiaochu Yuan | @Mark: "true by accident" could be interpreted as "true but not amenable to a satisfying human proof." I don't know if this is what the OP means, though. | |
Aug 25, 2011 at 20:16 | comment | added | Timothy Chow | @Andrej: The reconstruction conjecture is false for directed graphs. I've usually seen it stated for simple graphs (no loops or multiple edges) though I suspect that this distinction may not matter much. | |
Aug 25, 2011 at 20:12 | comment | added | François G. Dorais | It is truly fascinating how all the answers interpret your question in radically different ways... | |
Aug 25, 2011 at 18:18 | answer | added | Timothy Chow | timeline score: 17 | |
Aug 25, 2011 at 18:07 | answer | added | user9072 | timeline score: 12 | |
Aug 25, 2011 at 15:31 | history | edited | François G. Dorais | CC BY-SA 3.0 |
added wikipedia link
|
Aug 25, 2011 at 13:15 | comment | added | Andrej Bauer | What sort of graphs are we talking about? Directed, with loops, with multiple edges? I am asking out of idle curiosity. | |
Aug 25, 2011 at 13:09 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
edited title
|
Aug 25, 2011 at 12:26 | answer | added | Carl Mummert | timeline score: 10 | |
Aug 25, 2011 at 12:18 | comment | added | Mark Grant | Perhaps, when you try to formalize the concept "true by accident", you arrive at the concept "true but formally undecidable"? At least I am having difficulty seeing what the distinction between the two might be. | |
Aug 25, 2011 at 12:15 | answer | added | Joel David Hamkins | timeline score: 39 | |
Aug 25, 2011 at 12:12 | answer | added | François G. Dorais | timeline score: 20 | |
Aug 25, 2011 at 11:53 | comment | added | Carl Mummert | Assuming the conjecture is true, one could computably reconstruct the original graph from the subgraphs by brute force - enumerate all the graphs on $n$ vertices and then eliminate them one at a time if they do not have the correct collection of subgraphs. So the truth of the conjecture would imply the existence of the procedure, but that procedure only works because the conjecture is already known to be true, and the procedure itself would exist even if the conjecture is false, although in that case the procedure doesn't do what it is supposed to do. | |
Aug 25, 2011 at 11:50 | comment | added | André Henriques | @Gjergji: There exist hard conjectures that look quite unlikely, at least at first sight. On the other hand, there exist hard conjectures that look excessively plausible. | |
Aug 25, 2011 at 11:46 | comment | added | André Henriques | It seems unlikely to me that the question "Has anyone has formalized this concept?" will produce an interesting answers. Probably this is not the case and the answer is simply "No: no one has formalized that concept". On the other hand, asking for a list of examples of similar-sounding conjectures (i.e. things that are true by accident - Goldbach's conjecture being the prototypical example) might be more fruitful. If you decide to change the question in the way I suggest, then please don't forget to make it community-wiki. | |
Aug 25, 2011 at 11:44 | comment | added | Gjergji Zaimi | Can't one ask the same question about any hard conjecture? | |
Aug 25, 2011 at 11:31 | history | asked | Gordon Royle | CC BY-SA 3.0 |