alt Hacker NewsI think what's interesting about Lean is that Lean is a language, and what most people are talking about is a library called Mathlib. From what I've read about Mathlib, the creators are very pragmatic, which is why they encode classical logic in Lean types, with only a bit of intuitionistic logic[1].
[1] for those unfamiliar with math lingo, classical logic has a lot of powerful features. One of those is the law of the excluded middle, which says something can't be true and false at the same time. That means not not true is true, which you can't say in intuitionistic logic. Another feature is proof by contradiction, where you can prove something by showing that the alternative is unsound. There's quite a few results that depend on these techniques, so trying to do everything in intuitionistic logic has run into a lot of roadblocks.
Replies
> I think what's interesting about Lean is that Lean is a language, and what most people are talking about is a library called Mathlib. From what I've read about Mathlib, the creators are very pragmatic, which is why they encode classical logic in Lean types, with only a bit of intuitionistic logic
The computer science folks are now working on their own CSLib. https://www.cslib.io https://www.github.com/leanprover/cslib Given that intuitionistic logic is really only relevant to computational content (the whole point of it is to be able to turn a mathematical argument into a construction that could in some sense be computed with), it will be interesting to see how they deal with the issue. Note that if you write algorithms in Lean, you are already limited to some kind of construction, and perhaps that's all the logic you need for that purpose.
Five stages of accepting constructive mathematics:
Denial
Anger
Bargaining
Depression
Acceptance
A talk about constructive mathematics by Andrej Bauer at the Institute for Advanced Study.
When/why would one prefer to use intuitive logic, given the limitations/roadblocks?
> One of those is the law of the excluded middle, which says something can't be true and false at the same time.
That would be the law of non-contradiction (LNC). The law of the excluded middle (LEM) says that for every proposition it is true or its negation is true.
LEM: For all p, p or not p.
LNC: For all p, not (p and not p).
Classical logic satisfies both, intuitionistic logic only satisfies LNC.
> Another feature is proof by contradiction, where you can prove something by showing that the alternative is unsound.
As far as lean is concerned, this isn't an example of classical logic. It's just the definition of "not" - to say that some proposition implies a contradiction, and to say that that proposition is untrue, are the same statement.
Most "something"s that you'd want to prove this way will require a step from classical logic, but not all of them. (¬p ⟶ F) ⟶ p is classical; (p ⟶ F) ⟶ ¬p is constructive.
This makes it good for formal maths, but bad for philosophy, since it means it can’t encode the speculative movement
>the law of the excluded middle, which says something can't be true and false at the same time
This is the not excluded middle, it is the "Law of noncontradiction"
Excluded middle means: either p is true or the negation of p is true
https://en.wikipedia.org/wiki/Law_of_noncontradiction