Timeline for "Strange" proofs of existence theorems
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 12, 2018 at 0:20 | comment | added | Mario Carneiro | I think the key here is how you show the family is precompact, because this is where the exists is. (It claims that every sequence has some accumulation point, or every open cover has a finite subcover, or every filter has a limit point - no matter how you slice it it's an existence claim.) Unless you are using Heine-Borel in which case the construction comes from Heine-Borel itself which is using (countable) choice. | |
| Oct 10, 2018 at 20:55 | comment | added | Joseph Granata | I too was considering a similar point when writing the question. I think this relates to @usul’s discussion of “nondeteministic constructive algorithm” A few answers up. I’m not sure yet where I stand on whether these are examples or nonexamples | |
| Oct 10, 2018 at 19:33 | comment | added | Carl Mummert | I was not sure whether this would count as constructive, or whether it would be viewed as using the axiom of choice somehow. Certainly it would be constructive if it was possible to construct approximations to a single limiting object. | |
| Oct 10, 2018 at 18:51 | history | answered | Martin Hairer | CC BY-SA 4.0 |