3 ms·
> You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geom
by IngoBlechschmid 8y ago
> You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geometry though (thanks to Hilbert).
Just wanted to chime in regarding the last sentence: There are right now ongoing efforts to eliminate any uses of LEM in algebraic geometry.
We do this not only out of academic curiosity, in order to create a more elegant setup and to be able to extract algorithms from proofs, but also to carry out a program called "relativization by internalization". The idea is that we can automatically derive some results for "relative schemes" if we have proven them for ordinary schemes without using LEM or the axiom of choice.