5 ms·

Honestly, the entire part of the post before getting to categories is what I think is most useful for the broadest range of people. We often look at "logic" and

Honestly, the entire part of the post before getting to categories is what I think is most useful for the broadest range of people. We often look at "logic" and "mathematics" as one thing, and even more than that, we look at them as absolutes - if something is mathematically proven, it is certainly a fact, no? Well, it turns out even here there are still shades of gray, and the difference between classical and intuitionistic logic is the perfect example. Not everyone even agrees on the foundation of what logic and math are. And, each has their own benefits and strengths (intuitionistic logic tends to go hand in hand with type theory as the basis for theorem provers / proof assistants for mostly practical reasons). Classical logic has always made the most sense to me, because accepting the law of excluded middle leads to a neater world of arguments to me. If you can't prove something, it is treated as false. Might be harsh, but that harshness yields simplicity. I have come to at least understand the intuitionistic perspective though, because of how prevalent it is in the verification space - I have been super into F* recently (https://www.fstar-lang.org/ https://www.fstar-lang.org/), and this comes from a line of logics and programming languages that owe their life to intuitionistic logic. I like Andrej Bauer's position of being a "mathematical relavist," where he says "we cannot ignore the many worlds of mathematics" (http://math.andrej.com/2012/10/03/am-i-a-constructive-mathematician/ http://math.andrej.com/2012/10/03/am-i-a-constructive-mathem...). Math and logic are vast spaces with different systems and perspectives, and rather than treat one as universal truth, it is practically more beneficial to be familiar with the different systems and their perspectives, and to be able to switch between them when practical.

drdeca 5y ago
> If you can't prove something, it is treated as false. Maybe I'm being excessively literal in interpreting the phrasing here, but that doesn't seem like how I would describe classical logic? There are plenty of cases where neither a thing nor its negation can be shown in some system which is based on classical logic (I'm sure you are well aware of this fact, so I'm probably just misinterpreting you by being too literal). But yes, I also share the sentiment that, for ordinary/day-to-day reasoning, classical logic is substantially more intuitive than intuitionistic logic, and makes things simpler. Can I think of a precise way to say the thing that I imagine you must have meant by that? In both classical logic and intuitionistic logic, if by assuming something you can derive False, then you can prove the negation of the thing. So that's not the distinguishing thing. If by assuming the falsehood of something you can derive False, in classical logic you can use that as a proof of the thing. (double negation elimination), while in intuitionistic logic you only get the double negation. This, I think at least mostly describes the difference (though not all the like, implications of it), but I'm not sure how to make it into something similar to "If you can't prove something, it is treated as false." Though, that statement does remind me of the idea of a/the Constructible universe in set theory..
- amw-zero 5y ago
  Yea, I think putting it that way is an overreach of the law of excluded middle / bivalence.
- leoc 5y ago
  Yes, knowing that ~P and not knowing P are clearly and fundamentally different things in the world of classical logic. (I'm not an expert, but I know this much.) It's hacky computing systems like Prolog and the relational model and/or SQL which erase the distinction. https://en.wikipedia.org/wiki/Closed-world_assumption https://en.wikipedia.org/wiki/Closed-world_assumption The law of the excluded middle only says that at least one of P and ~P must be true, and doesn't at all promise that we will necessarily be able to conclude which one.
pphysch 5y ago
> Classical logic has always made the most sense to me, because accepting the law of excluded middle leads to a neater world of arguments to me. What use is a neat argument if it is divorced from reality? LoEM tricks us into viewing ontologies as static, leading to subtle but drastic errors in thinking. LoEM/classical logic should always be employed as a conscious assumption, with awareness of its drawbacks. Leave room for dialectical reasoning as well.
- amw-zero 5y ago
  It is very fair to say that this is: a) far too extreme of a position to be useful to anyone b) not true in any sense of the word Classical logic has been behind the bulk of mathematical results in the last 100 years or so. It may not be perfect, but no system is.
  - pphysch 5y ago
    By far the bulk of pure mathematical results in the last 100 years have no demonstrated real world function. They are logically sound--and utterly divorced from reality. And any useful innovations tend to come about from dialectical reasoning, because classical logic is incapable of genuine ontological generation. For example, infinitesimal calculus was not "embedded" somewhere in the existing mathematics, waiting to be logically deduced by an expert logician; Newton developed new methods of mathematically modeling unquantifiable quantities to address contradictions in the application of traditional mathematics to physical systems.
    - amw-zero 5y ago
      > By far the bulk of mathematical results in the last 100 years have demonstrated no real world function How absolutely arrogant and unappreciative of you to say. You are very divorced from reality. That much is clear - normally I don’t like to get personal, but really. I’m sure you hear this all the time which ferments your bitterness. “It is not the critic who counts”
      - 5y ago
deleted 5y ago
[deleted]

drdeca 5y ago

> If you can't prove something, it is treated as false. Maybe I'm being excessively literal in interpreting the phrasing here, but that doesn't seem like how I would describe classical logic? There are plenty of cases where neither a thing nor its negation can be shown in some system which is based on classical logic (I'm sure you are well aware of this fact, so I'm probably just misinterpreting you by being too literal). But yes, I also share the sentiment that, for ordinary/day-to-day reasoning, classical logic is substantially more intuitive than intuitionistic logic, and makes things simpler. Can I think of a precise way to say the thing that I imagine you must have meant by that? In both classical logic and intuitionistic logic, if by assuming something you can derive False, then you can prove the negation of the thing. So that's not the distinguishing thing. If by assuming the falsehood of something you can derive False, in classical logic you can use that as a proof of the thing. (double negation elimination), while in intuitionistic logic you only get the double negation. This, I think at least mostly describes the difference (though not all the like, implications of it), but I'm not sure how to make it into something similar to "If you can't prove something, it is treated as false." Though, that statement does remind me of the idea of a/the Constructible universe in set theory..

amw-zero 5y ago
Yea, I think putting it that way is an overreach of the law of excluded middle / bivalence.
leoc 5y ago
Yes, knowing that ~P and not knowing P are clearly and fundamentally different things in the world of classical logic. (I'm not an expert, but I know this much.) It's hacky computing systems like Prolog and the relational model and/or SQL which erase the distinction. https://en.wikipedia.org/wiki/Closed-world_assumption https://en.wikipedia.org/wiki/Closed-world_assumption The law of the excluded middle only says that at least one of P and ~P must be true, and doesn't at all promise that we will necessarily be able to conclude which one.

pphysch 5y ago

> Classical logic has always made the most sense to me, because accepting the law of excluded middle leads to a neater world of arguments to me. What use is a neat argument if it is divorced from reality? LoEM tricks us into viewing ontologies as static, leading to subtle but drastic errors in thinking. LoEM/classical logic should always be employed as a conscious assumption, with awareness of its drawbacks. Leave room for dialectical reasoning as well.

amw-zero 5y ago
It is very fair to say that this is: a) far too extreme of a position to be useful to anyone b) not true in any sense of the word Classical logic has been behind the bulk of mathematical results in the last 100 years or so. It may not be perfect, but no system is.
- pphysch 5y ago
  By far the bulk of pure mathematical results in the last 100 years have no demonstrated real world function. They are logically sound--and utterly divorced from reality. And any useful innovations tend to come about from dialectical reasoning, because classical logic is incapable of genuine ontological generation. For example, infinitesimal calculus was not "embedded" somewhere in the existing mathematics, waiting to be logically deduced by an expert logician; Newton developed new methods of mathematically modeling unquantifiable quantities to address contradictions in the application of traditional mathematics to physical systems.
  - amw-zero 5y ago
    > By far the bulk of mathematical results in the last 100 years have demonstrated no real world function How absolutely arrogant and unappreciative of you to say. You are very divorced from reality. That much is clear - normally I don’t like to get personal, but really. I’m sure you hear this all the time which ferments your bitterness. “It is not the critic who counts”
    - 5y ago

deleted 5y ago

[deleted]