News for hackers. Stuff that matters.
Re:What is the Axiom of Choice? by veltas on Friday July 16, 2021 @06:03AM (#27854642)
Why does AoC implying LEM mean you can't use LEM in constructive maths?

EDIT: misread

Re:What is the Axiom of Choice? by reuben364 on Friday July 16, 2021 @06:14AM (#27854691)
Constructive mathematics by it's nature does not use LEM. The idea is that proof of existance must be done by construction of the object in question. LEM implies DNE, which means existance can be shown by showing non-existance is not the case.

EDIT: Apologies, misunderstood.

Re:What is the Axiom of Choice? by siraben on Friday July 16, 2021 @06:05AM (#27854651)
I said that if you don't want to use LEM in constructive maths you must also give up AOC, since AOC -> LEM.
Re:What is the Axiom of Choice? by veltas on Friday July 16, 2021 @06:19AM (#27854721)
Oh right. Also hi siraben didn't notice it was you.
Re:What is the Axiom of Choice? by siraben on Friday July 16, 2021 @06:35AM (#27854799)
Hello! Nice to see another IRCer :)