Timeline for Are there examples of nonconstructive metaproofs?
Current License: CC BY-SA 3.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 8, 2011 at 17:55 | comment | added | Henry Towsner | If we're talking about proofs in formal systems of nonstandard analysis, there are general methods for extracting the standard proof from it. For instance, "Weak theories of nonstandard arithmetic and analysis" by Jeremy Avigad. | |
| Jun 8, 2011 at 16:28 | comment | added | Gerald Edgar | One can go from nonstandard proof to standard proof using ultrapowers. It is just that such a proof may not be as "elegant". | |
| Jun 8, 2011 at 16:19 | history | answered | Noah | CC BY-SA 3.0 |