Timeline for Applications of nonconstructive mathematics
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 22, 2012 at 7:08 | comment | added | Russell O'Connor | I was discussing Dickson's lemma with some colleagues last year. As far as I can tell, the statement becomes constructive if we weaken the statement to say that any non-empty subset is a contained in a union of finite many quarter planes. I don't know if this weaker version is sufficient for the Knuth-Bendix completion. ... BTW also any empty subset also works, so we can constructively prove that any empty or non-empty subset is contained in a union of finite many quarter planes. | |
| May 14, 2012 at 20:57 | comment | added | Andrej Bauer | Really? The proof I know relies on Dickson's lemma, en.wikipedia.org/wiki/Dickson's_lemma, which is non-constructive. But as far as I remember, the lemma is needed only to show termination. So, if you believe in Markov Principle, as some constructivists do, then that would count as a constructive theorem. | |
| May 14, 2012 at 18:43 | history | made wiki | Post Made Community Wiki by François G. Dorais | ||
| May 14, 2012 at 17:46 | comment | added | Henry Towsner | I'm not sure Kruskal's tree theorem is nonconstructive. I recall seeing several approaches to constructive proofs, though the only one I can find quickly is Wim Veldman's "An intuitionistic proof of Kruskal's Theorem". | |
| May 14, 2012 at 17:24 | history | answered | none | CC BY-SA 3.0 |