4 ms·
> In constructive mathematics, there can also be numbers d such that d^2 = 0 but not necessarily d = 0. In the footnote, it mentions that d is not a real numbe
by andrewla 8y ago
> In constructive mathematics, there can also be numbers d
such that d^2 = 0 but not necessarily d = 0.
In the footnote, it mentions that d is not a real number (which seems right). But I find this very confusing -- this seems to be using a deliberately non-constructible number to facilitate proofs in constructive mathematics?
Regardless of whether this meets a formal criteria for being a tool in constructive mathematics, it does seem to be in direct opposition to the notion of intuitionalist mathematics, which has as a fundamental goal to dispense with axiom-of-choice-style proofs of things that are clearly ridiculous (like Banach-Tarski).
- xelxebar 8y agoWe can explicitly construct such numbers using 2x2 matrices. These are called "dual numbers"[0], and the matrix representation is essentially an analoge of the same for complex numbers. So if you accept the complex unit, i, as a reasonable algebraic thing, then the "dual unit" shouldn't be too much of a stretch. Anyway, all that is completely fine in standard foundations. The LEM contradictions only come in when we impose other axioms. For example, in Anders Kock's Sythetic Differential Geometry[1], we essentially start out by assuming that every function is differentiable. This seems sorta crazy at first blush, and it does give contradictions, but the interesting bit as that those problems hinge solely on LEM. Thus, in a way, we're left with chosing between universal differentiability or LEM. Kock explores what happens if we pick the former, and it turns out to be pretty deep, interesting and useful. [0]:https://en.wikipedia.org/wiki/Dual_number https://en.wikipedia.org/wiki/Dual_number [1]:http://home.imf.au.dk/kock/sdg99.pdf http://home.imf.au.dk/kock/sdg99.pdf