Timeline for "Strange" proofs of existence theorems
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 13, 2018 at 11:55 | comment | added | Nik Weaver | There's an umlaut on Lob too, but I don't remember how to make them ... | |
| Oct 13, 2018 at 10:44 | comment | added | Hagen von Eitzen | Since we had the Erdős vs. Erdös debate in the comments to another answer, I'd like to nitpick that its Gödel, not Godel | |
| Oct 13, 2018 at 1:35 | comment | added | Nik Weaver | @Timothy_Chow: that is helpful, thank you. | |
| Oct 12, 2018 at 20:41 | comment | added | Timothy Chow | Great example. Perhaps one way to answer the questions of Sam Hopkins and Qfwfq is to distinguish between the "informal" argument P that establishes the existence of a PA-proof of L, and the formalization P' of P in PA. The informal argument doesn't tell you how to construct a PA-proof of L. To construct a PA-proof of L, it has to occur to you to take the informal argument P and formalize it as P'. P does not construct its own formalization; rather, just by "being itself" it provides the raw material for a constructive proof. | |
| Oct 12, 2018 at 12:03 | comment | added | Nik Weaver | @Sam_Hopkins: it is both. | |
| Oct 12, 2018 at 12:02 | comment | added | Nik Weaver | The point is that the argument shows that there is a proof but does not tell us what it is. But it is itself the proof that it nonconstructively finds! So yes, in fact we do know what the proof is, but it does not tell us this. | |
| Oct 12, 2018 at 10:31 | comment | added | Qfwfq | If the above argument can be formalized in PA, why is it fair to say that "we don't know what that proof is"? | |
| Oct 12, 2018 at 10:10 | comment | added | Sam Hopkins | If, as you said, the argument you just gave can be formalized in PA, then isn't it in fact just a "proof of L" and not a "nonconstructive proof that there exists a proof of L"? | |
| Oct 12, 2018 at 6:55 | history | answered | Nik Weaver | CC BY-SA 4.0 |