3 ms·

You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geomet

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). Practically, intuitionistic logic has a lot of applications to computer science thanks to Curry-Howard. Philosophically, soundness of LEM depends on where one originates the source of mathematics. If you're like Kant (or Brouwer) then LEM would make little sense since the source of mathematics, just like any other cognitive ability, is human cognition which exists independent of abstractions of the outer world. But, even without being a Platonist (like Godel) if mathematics has any sort of external source (e.g. abstracting the world or being a good abstraction of the world) then it's really hard to argue against LEM, although some epistemological arguments exist.

YorkshireSeason 8y ago
soundness of LEM depends on where one originates the source of mathematics I disagree! One of Goedel's many great contributions was the double-negation translation (later refined by others), and what it does is show that (simplifying a bit) intuitionistic logic and classical logic are equiconsistent! In other words: any contradiction you can derive in classical logic, you can convert into a contradiction in intuitionistic logic. (The reverse direction is trivial because all intuitionistic proof principles are also classical.)
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.

YorkshireSeason 8y ago

soundness of LEM depends on where one originates the source of mathematics I disagree! One of Goedel's many great contributions was the double-negation translation (later refined by others), and what it does is show that (simplifying a bit) intuitionistic logic and classical logic are equiconsistent! In other words: any contradiction you can derive in classical logic, you can convert into a contradiction in intuitionistic logic. (The reverse direction is trivial because all intuitionistic proof principles are also classical.)

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.