6 ms·

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

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[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.

bowsamic 6mo ago
This makes it good for formal maths, but bad for philosophy, since it means it can’t encode the speculative movement
- drdeca 6mo ago
  Which logic are you saying “can’t encode the speculative moment”? I think the two logics can emulate one another? Or, at the very least, can describe what the other concludes. I know intuitionistic logic can have classical logic embedded in it through some sort of “put double negation on everything”. I think if you add some sort of modal operator to classical logic you could probably emulate intuitionistic logic in a similar way?
  - bowsamic 6mo ago
    Any logic with LEM
  - zozbot234 6mo ago
    You don't even need to add a modal operator since modal logic itself can be embedded in classical logic via possible-world semantics. Of course the whole thing becomes a bit clunky - but that's the argument for starting with intuitionistic logic, where you wouldn't need to do that.
vscode-rest 6mo ago
When/why would one prefer to use intuitive logic, given the limitations/roadblocks?
- thaumasiotes 6mo ago
  For ideological reasons.
- ux266478 6mo ago
  Classical logic has plenty of limitations/roadblocks, all logics do. Logic isn't a unified domain, but an infinite beach of structural shards, each providing a unique lens of study. Classical logic was rejected in computer science because the non-constructive nature made it inappropriate for an ostensibly constructive domain. Theoretical mathematics has plenty of uses to prove existences and then do nothing with the relevant object. A computer, generally, is more interested in performing operations over objects, which requires more than proving the object exists. Additionally, while you can implement evaluation of classical logic with a machine, it's extremely unwieldy and inefficient, and allows for a level of non-rigor that proves to be a massive footgun.
  - zozbot234 6mo ago
    But proving the object exists is still useful, of course: it effectively means you can assume an oracle that constructs this object without hitting any contradiction. Talking about oracles is useful in turn since it's a very general way of talking about side-conditions that might make something easier to construct.
    - ux266478 6mo ago
      Of course. Though it's also important to note: whether or not an object exists is dependent on the logic being utilized itself, which is to say nothing of how even if the object holds some structural equivalent in the given logic of attention, it might not have all provable structure shared between the two, and that's before we get into how the chosen axioms on top of the logical system also mutate all of this. It's not that classical logic is useless, it's just that it's not particularly appropriate to choose as the basis for a system built on algorithms. This goes both ways. Set theory was taken as the foundation of arithmetic, et al. because type theory was simply too unwieldy for human beings scrawling algebras on blackboards.
Chinjut 6mo ago
You mean intuitionistic logic, not "intuitive logic".
- smj-edison 6mo ago
  Oops, just edited. I'm still fairly new to this area, so I keep mixing up my terms :)
thaumasiotes 6mo ago
> 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.
- smj-edison 6mo ago
  So proof by contradiction proves ¬p, but it requires the law of excluded middle to prove p (in the case of ¬p -> F)? I didn't realize that was constructive in the first case.
  - thaumasiotes 6mo ago
    Well, at some point you have to define what you mean by "proof by contradiction". I was responding to your statement, "prove something by showing that the alternative is unsound". You can prove that something is false that way without needing classical logic. Mathlib defines `by_contradiction` as a theorem proving `(¬p → False) → p` for any proposition p. ( https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Basic.html#by_contradiction https://leanprover-community.github.io/mathlib4_docs/Mathlib... ) This does require classical logic. For what's happening with `¬p -> F`, recall that this is by definition the statement `¬¬p`; classical logic will let you conclude `p` from `¬¬p`, or it will let you apply the law of the excluded middle to conclude that either `p` or `¬p` must be the case, and then show that since it isn't `¬p`, it must be `p`. (Again, not really different approaches, but perhaps different in someone's mental model.) On the other hand, if you have `p -> F`, that is by definition the statement `¬p`, and if you've established `¬p`, you've already finished proving that p is false. Something that I find particularly absurd about the hypothetical distinction between intuitionistic and classical logic is that intuitionistic logic is sufficient to prove `¬p` from `¬¬¬p`. (This is quite similar to how 'proof by contradiction' is constructive if you're proving a negative but not if you're proving a positive; it might be the same result.) So for any proposition that can be restated in a "negative" way, the law of the excluded middle remains true in intuitionistic logic. The difference lies only in "fundamentally positive" propositions. (You can do that proof yourself at https://incredible.pm/ https://incredible.pm/ ; it's in section 4, `((A→⊥)→⊥)→⊥` -> `A→⊥`.) There's a fun article on this very blog telling a similar story: https://lawrencecpaulson.github.io/2021/11/24/Intuitionism.html https://lawrencecpaulson.github.io/2021/11/24/Intuitionism.h... > Martin-Löf designed his type theory with the aim that AC should be provable and in his landmark Constructive mathematics and computer programming presented a detailed derivation of it as his only example. Briefly, if (∀x : A)(∃y :B) C(x,y) then (∃f : A → B)(∀x : A) C(x, f(x)). > Spoiling the party was Diaconescu’s proof in 1975 that in a certain category-theoretic setting, the axiom of choice implied LEM and therefore classical logic. His proof is reproducible in the setting of intuitionistic set theory and seems to have driven today’s intuitionists to oppose AC. > It’s striking that AC was seen not merely as acceptable but clear by the likes of Bishop, Bridges and Dummett. Now it is being rejected and the various arguments against it have the look of post-hoc rationalisations. Of course, the alternative would be to reject intuitionism altogether. This is certainly what mathematicians have done: in my experience, the overwhelming majority of constructive mathematicians are not mathematicians at all. They are computer scientists.
cubefox 6mo ago
> 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.
zozbot234 6mo ago
> 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.cslib.io https://www.github.com/leanprover/cslib 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.
deleted 6mo ago
[deleted]
hackandthink 6mo ago
>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 https://en.wikipedia.org/wiki/Law_of_noncontradiction
leonidasrup 6mo ago
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. https://www.youtube.com/watch?v=21qPOReu4FI https://www.youtube.com/watch?v=21qPOReu4FI http://dx.doi.org/10.1090/bull/1556 http://dx.doi.org/10.1090/bull/1556

bowsamic 6mo ago

This makes it good for formal maths, but bad for philosophy, since it means it can’t encode the speculative movement

drdeca 6mo ago
Which logic are you saying “can’t encode the speculative moment”? I think the two logics can emulate one another? Or, at the very least, can describe what the other concludes. I know intuitionistic logic can have classical logic embedded in it through some sort of “put double negation on everything”. I think if you add some sort of modal operator to classical logic you could probably emulate intuitionistic logic in a similar way?
- bowsamic 6mo ago
  Any logic with LEM
- zozbot234 6mo ago
  You don't even need to add a modal operator since modal logic itself can be embedded in classical logic via possible-world semantics. Of course the whole thing becomes a bit clunky - but that's the argument for starting with intuitionistic logic, where you wouldn't need to do that.

vscode-rest 6mo ago

When/why would one prefer to use intuitive logic, given the limitations/roadblocks?

thaumasiotes 6mo ago
For ideological reasons.
ux266478 6mo ago
Classical logic has plenty of limitations/roadblocks, all logics do. Logic isn't a unified domain, but an infinite beach of structural shards, each providing a unique lens of study. Classical logic was rejected in computer science because the non-constructive nature made it inappropriate for an ostensibly constructive domain. Theoretical mathematics has plenty of uses to prove existences and then do nothing with the relevant object. A computer, generally, is more interested in performing operations over objects, which requires more than proving the object exists. Additionally, while you can implement evaluation of classical logic with a machine, it's extremely unwieldy and inefficient, and allows for a level of non-rigor that proves to be a massive footgun.
- zozbot234 6mo ago
  But proving the object exists is still useful, of course: it effectively means you can assume an oracle that constructs this object without hitting any contradiction. Talking about oracles is useful in turn since it's a very general way of talking about side-conditions that might make something easier to construct.
  - ux266478 6mo ago
    Of course. Though it's also important to note: whether or not an object exists is dependent on the logic being utilized itself, which is to say nothing of how even if the object holds some structural equivalent in the given logic of attention, it might not have all provable structure shared between the two, and that's before we get into how the chosen axioms on top of the logical system also mutate all of this. It's not that classical logic is useless, it's just that it's not particularly appropriate to choose as the basis for a system built on algorithms. This goes both ways. Set theory was taken as the foundation of arithmetic, et al. because type theory was simply too unwieldy for human beings scrawling algebras on blackboards.

Chinjut 6mo ago

You mean intuitionistic logic, not "intuitive logic".

smj-edison 6mo ago
Oops, just edited. I'm still fairly new to this area, so I keep mixing up my terms :)

thaumasiotes 6mo ago

> 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.

smj-edison 6mo ago
So proof by contradiction proves ¬p, but it requires the law of excluded middle to prove p (in the case of ¬p -> F)? I didn't realize that was constructive in the first case.
- thaumasiotes 6mo ago
  Well, at some point you have to define what you mean by "proof by contradiction". I was responding to your statement, "prove something by showing that the alternative is unsound". You can prove that something is false that way without needing classical logic. Mathlib defines `by_contradiction` as a theorem proving `(¬p → False) → p` for any proposition p. ( https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Basic.html#by_contradiction https://leanprover-community.github.io/mathlib4_docs/Mathlib... ) This does require classical logic. For what's happening with `¬p -> F`, recall that this is by definition the statement `¬¬p`; classical logic will let you conclude `p` from `¬¬p`, or it will let you apply the law of the excluded middle to conclude that either `p` or `¬p` must be the case, and then show that since it isn't `¬p`, it must be `p`. (Again, not really different approaches, but perhaps different in someone's mental model.) On the other hand, if you have `p -> F`, that is by definition the statement `¬p`, and if you've established `¬p`, you've already finished proving that p is false. Something that I find particularly absurd about the hypothetical distinction between intuitionistic and classical logic is that intuitionistic logic is sufficient to prove `¬p` from `¬¬¬p`. (This is quite similar to how 'proof by contradiction' is constructive if you're proving a negative but not if you're proving a positive; it might be the same result.) So for any proposition that can be restated in a "negative" way, the law of the excluded middle remains true in intuitionistic logic. The difference lies only in "fundamentally positive" propositions. (You can do that proof yourself at https://incredible.pm/ https://incredible.pm/ ; it's in section 4, `((A→⊥)→⊥)→⊥` -> `A→⊥`.) There's a fun article on this very blog telling a similar story: https://lawrencecpaulson.github.io/2021/11/24/Intuitionism.html https://lawrencecpaulson.github.io/2021/11/24/Intuitionism.h... > Martin-Löf designed his type theory with the aim that AC should be provable and in his landmark Constructive mathematics and computer programming presented a detailed derivation of it as his only example. Briefly, if (∀x : A)(∃y :B) C(x,y) then (∃f : A → B)(∀x : A) C(x, f(x)). > Spoiling the party was Diaconescu’s proof in 1975 that in a certain category-theoretic setting, the axiom of choice implied LEM and therefore classical logic. His proof is reproducible in the setting of intuitionistic set theory and seems to have driven today’s intuitionists to oppose AC. > It’s striking that AC was seen not merely as acceptable but clear by the likes of Bishop, Bridges and Dummett. Now it is being rejected and the various arguments against it have the look of post-hoc rationalisations. Of course, the alternative would be to reject intuitionism altogether. This is certainly what mathematicians have done: in my experience, the overwhelming majority of constructive mathematicians are not mathematicians at all. They are computer scientists.

cubefox 6mo ago

> 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.

zozbot234 6mo ago

> 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.cslib.io https://www.github.com/leanprover/cslib 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.

deleted 6mo ago

[deleted]

hackandthink 6mo ago

>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 https://en.wikipedia.org/wiki/Law_of_noncontradiction

leonidasrup 6mo ago

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. https://www.youtube.com/watch?v=21qPOReu4FI https://www.youtube.com/watch?v=21qPOReu4FI http://dx.doi.org/10.1090/bull/1556 http://dx.doi.org/10.1090/bull/1556