Timeline for Are there examples of nonconstructive metaproofs?
Current License: CC BY-SA 3.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 8, 2011 at 17:58 | comment | added | Henry Towsner | There's a stronger form of this assertion. If the proof system is recursive, the statement "T proves $\phi$" is itself a $\Sigma_1$ statement, so if the non-constructive proof itself takes place in a "reasonable" system, it is possible to extract an explicit witness, which would be a direct proof. | |
| Jun 8, 2011 at 16:47 | comment | added | Qiaochu Yuan | I don't know that this addresses the spirit of the question. This algorithm guarantees that it can find a proof but it does not guarantee that this will happen before I die or that the proof can be made short enough for me to finish reading it before I die, yet it is still possible that I can prove by other means that a proof exists in perhaps 10 minutes. | |
| Jun 8, 2011 at 16:37 | history | edited | David Harris | CC BY-SA 3.0 |
added 9 characters in body
|
| Jun 8, 2011 at 16:33 | comment | added | Andrej Bauer | You are implicitly using Markov principle, I think. | |
| Jun 8, 2011 at 16:30 | history | edited | David Harris | CC BY-SA 3.0 |
added 574 characters in body; added 9 characters in body; added 16 characters in body
|
| Jun 8, 2011 at 16:05 | comment | added | skeptical scientist | This can hardly be seen as a constructive proof, as the "constructive" part is entirely divorced from the "proof" part. | |
| Jun 8, 2011 at 15:48 | history | answered | David Harris | CC BY-SA 3.0 |