Hacker News Reader

There does not seem to be any reason for mathematicians to be turned about by these engines using constructive mathematics. One can use excluded middle as an axiom and do all the classical mathematics one likes. What becomes much easier if the engine is constructive is telling which theorems depend on excluded middle and which do not.

View on HN

This is in fact how Lean works - the basic logic is constructive and excluded middle is an "extra" axiom. But even that is not as elegant as just writing non-constructive statements in the negative fragment of the logic, where (AIUI) one can already reason classically with no need for extra axioms.

I know we've discussed on HN before whether the elegance of the negative fragment extends to practice, but something about Lean is that it doesn't have LEM as an axiom. It's a theorem following from (a version of) the axiom of choice, the existence of quotient types, proof irrelevance (proofs of the same theorem are equal), and proposition extensionality (logically equivalent propositions are equal). Lean doesn't let you construct things that materially depend on LEM however -- you can only use it to prove that already constructed things have desired properties.

In case anyone is curious, the proof of LEM from AC is: Diaconescu's Theorem [0]

[0]: https://en.wikipedia.org/wiki/Diaconescu%27s_theorem#:~:text....

Reply on news.ycombinator.com