4 ms·

>mathematicians have been fighting about non-constructive proofs and the law of excluded middle far longer than they've been writing proof assistants Yes, and

>mathematicians have been fighting about non-constructive proofs and the law of excluded middle far longer than they've been writing proof assistants Yes, and Brouwer lost that fight. Classical logic is an implicit assumption for professional mathematicians. LEM is simply taught as the truth in university courses. My SO who is a math phd student hadn't even heard of intuitionistic logic before. If you want working mathematicians to use theorem provers, they need LEM. But this isn't actually all that much of an issue, since you can just introduce LEM as an axiom. It breaks computationality, but it's not like proof assistants using classical logic would have this either.

a1369209993 6y ago
> LEM is simply taught as the truth in university courses. So is[0] the notion that quantum systems magically undergo non-local, non-linear, non-unitary, CPT-violating, Liouville's-Theorem-violating, non-deterministic evolutions whenever a macroscopic system that happens to implement a sapient intellegence looks at something[1]. So that's not a very good yardstick for "this is not obviously false". 0: sample size of one univerity (circa 2010) for "simply taught as the truth", but I think it's recent enough and widespread enough to make a good example. See [2] if you want to investigate further. 1: aka the collapse postulate or Copenhagen interpretation 2: https://en.wikipedia.org/wiki/Copenhagen_interpretation#Acceptance_among_physicists https://en.wikipedia.org/wiki/Copenhagen_interpretation#Acce...
- JoeCamel 6y ago
  I would argue that trying to describe our physical world and reality has only one "axiom" which is: your description has to be consistent with our observations of the world. Mathematics doesn't have this limitation so I don't think your example is valid. If you don't like LEM, fine, maybe there is something interesting in systems without LEM, but most math is done with LEM. I don't think is a matter of "right" and "wrong".

a1369209993 6y ago

> LEM is simply taught as the truth in university courses. So is[0] the notion that quantum systems magically undergo non-local, non-linear, non-unitary, CPT-violating, Liouville's-Theorem-violating, non-deterministic evolutions whenever a macroscopic system that happens to implement a sapient intellegence looks at something[1]. So that's not a very good yardstick for "this is not obviously false". 0: sample size of one univerity (circa 2010) for "simply taught as the truth", but I think it's recent enough and widespread enough to make a good example. See [2] if you want to investigate further. 1: aka the collapse postulate or Copenhagen interpretation 2: https://en.wikipedia.org/wiki/Copenhagen_interpretation#Acceptance_among_physicists https://en.wikipedia.org/wiki/Copenhagen_interpretation#Acce...

JoeCamel 6y ago
I would argue that trying to describe our physical world and reality has only one "axiom" which is: your description has to be consistent with our observations of the world. Mathematics doesn't have this limitation so I don't think your example is valid. If you don't like LEM, fine, maybe there is something interesting in systems without LEM, but most math is done with LEM. I don't think is a matter of "right" and "wrong".