Timeline for Status of the fundamental theorem of algebra for the locale of real numbers
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 9, 2022 at 7:02 | comment | added | saolof | @MadeleineBirchfield Yes, and that makes solutions of polynomial equations a lot more complicated. | |
| Dec 9, 2022 at 3:49 | comment | added | Madeleine Birchfield | @saolof the "real numbers" used in smooth topoi are only a local ring, because if they were a Heyting field, then one could prove that equality is stable with respect to double negation, (because given a proposition $P$, $\neg \neg \neg P$ implies $\neg P$, and in a Heyting field, the negation of apartness is equality), and thus every element which is not not equal to zero is equal to zero. | |
| Nov 27, 2022 at 18:51 | comment | added | saolof | The main issue is that choiceless constructive mathematics is consistent with having a nonempty (where I do not mean inhabited) set of nilpotent infinitesimals, since smooth topoi exist. I would imagine that square roots become rather different for those. In constructive math with the fan theorem or open induction (to make things simple and avoid pointless topology for now) but without choice, you can use the EVT to prove that monic polynomials have a minimum in a closed circle which is not not zero, and use induction to find n roots where p is not not zero. They can be infinitesimal though | |
| Nov 22, 2022 at 15:31 | comment | added | David Roberts♦ | @MadeleineBirchfield you are aware of ncatlab.org/nlab/show/quadratic+formula#constructive_issues ? | |
| Nov 22, 2022 at 14:39 | comment | added | Emil Jeřábek | I may well be confusing something as this is not my area, but the quadratic formula requires square roots, and complex square roots seem to require LLPO: mathoverflow.net/q/353435 . | |
| Nov 22, 2022 at 11:18 | history | edited | Paul Taylor | CC BY-SA 4.0 |
added 499 characters in body
|
| Nov 21, 2022 at 21:58 | comment | added | user44143 | It is constructively valid that for $a>0$ and $b^2-4ac\ge 0$, both the $+$ and the $-$ options in the quadratic formula are (well-defined and) zeroes of the quadratic. What more generality would you want? | |
| Nov 21, 2022 at 21:08 | history | edited | Paul Taylor | CC BY-SA 4.0 |
deleted 6 characters in body
|
| Nov 21, 2022 at 20:44 | history | edited | Paul Taylor | CC BY-SA 4.0 |
added 312 characters in body
|
| Nov 21, 2022 at 20:34 | history | edited | Paul Taylor | CC BY-SA 4.0 |
added 712 characters in body
|
| Nov 21, 2022 at 20:20 | comment | added | Madeleine Birchfield | Is the quadratic formula constructive in general? | |
| Nov 21, 2022 at 20:00 | history | answered | Paul Taylor | CC BY-SA 4.0 |