7 ms·

Author here, let me know what you think.

Bost 5y ago
I started to read the first chapter of your book, it looks nice. If I may ask you, could you also provide answers to the questions you ask? Somewhat hidden, e.g. behind a button "Show me the answer". I often I think I know the answer, but A) my answer may be wrong or B) I'm right but my reasoning is wrong. (So I'd like to compare my answer with yours.) Thanks.
- boris_m 5y ago
  Thanks for the suggestion
unknown_apostle 5y ago
What are good introductory books for logic (classical and intuitionistic)? For category theory? Do you know any similar representation of paraconsistent logic?
- boris_m 5y ago
  For category theory, I like Spivak's books. For logic, it really depends of what you are searching for, for classical logic you can read the the classics, for example Russell and Tarski. For constructive logic I cannot think of a good introduction (besides mine ;) ), I personally picked it up from books about category theory and computer science.
- bitdiddle 5y ago
  I think the general program of categorical logic, the work of Lambek and Scott, and J. Bell on topos theory and local set theory really make clear the relationship between category theory and logic, as well as lambda calculus. A topos is essentially a cartesian closed category with a subject classifier. In Set this is the two element set of 1/0 which is a Boolean algebra and thus the internal logic of the category Set is classical. In general though the subobject classifier is a heyting algebra which expresses the semantics of intuitionistic logic. There is also a very good, but introductory, book by Goldblatt on Topoi that covers this logical aspect So in terms of logics the category of Sets is the exception. By internal logic I mean that for every topos one builds up a theory using it's objects and function between them. An equivalence theorem (see J. Bell) states that a given topos is essentially equal to the category generated by this internal theory. This program began with Lawvere who noticed that conjunction and implication were really adjoints, the same one as between the product and hom functors in a cartesian closed category.
deleted 5y ago
[deleted]
amelius 5y ago
There's a typo in this section header: > Axiom schemas/Rules of inferene
- boris_m 5y ago
  Thanks
atsmyles 5y ago
I'm still learning Cat theory myself (through the Category for Programmers book). I have a couple of questions/observations (that I would love your opinion on). First observation: True and False are the limit and co-limit of the Bool Category. Question 1: About ordering, would you say that ordering is a requirement (as in a necessary property) of Cat Theory? It was mentioned in Bartosz Milewski's book but it wasn't as strongly emphasized as in your article. Question 2: You mention how you can't express "A or not A" using intuistic logic. Since it is expressible in Set Theory, could we not use an Adjoint between the Bool and Set Categories respectively? Specifically Kan extensions?
- boris_m 5y ago
  The bool category is not involved in this. True and False are the initial and terminal object (related to limit and colimit, but not the same thing) of all logical categories as I call them, of which there are many (one for each set of axioms that you might construct). 1. Ordering is not required for a category to be a category, the necessary requirements are just the ones listed in the beginning of the book. It is just that orders can be seen as categories. 2. You can express "A or not A" in intuitionistic logic it is just that it is not necessarily true. Also, not sure how would you express that or any logical relation in set theory.
still_grokking 5y ago
What an amazing write-up! I've picked up those things peace by peace form Wikipedia to be able to understand the slang in Haskell land. But it was a long and puzzling process. This great summary offered here will hopefully help other people in the future get a coherent picture more quickly. (I hope the SEO is good so people will find it. I'm at least going to recommend it form now on whenever someone asks related questions). It could be extended with type-theory I guess. Also I would be interested to know more about the relation of those things described with abstract geometry and/or topology. But it's fantastic already as it stands!
smusamashah 5y ago
Hi, would it using different shapes altogether, instead same circle with different colors, be a better choice? Colors are soft too which makes the contrast between any two circles very low and hard to differentiate.
crawfordcomeaux 5y ago
Thank you for all of this and the large type, too! Would you do uncertainty logic next? https://arxiv.org/abs/1506.03123 https://arxiv.org/abs/1506.03123 https://arxiv.org/abs/1810.01310 https://arxiv.org/abs/1810.01310
- boris_m 5y ago
  In this book I am focused on category theory, but I may write some more about logic in other places.
  - crawfordcomeaux 5y ago
    I've really been wanting a friendly-like-what-you've-made category theory treatment of those two papers is what I'm trying to say. I've been assuming most/all things in life are uncertain. It's had a profoundly helpful impact on my life, so I'm trying to come to a deeper understanding of how to reason about an uncertain universe, which I think may be something a lot of people are needing these days. The first paper helped a bit, but I haven't really dug into and understood most of it.
tunesmith 5y ago
I'm curious in intuitionist logic what is the concept for "not proven", like neither true nor false? It's not "not-true" because going by your article it seems that would be "disproven" or bottom. Is it literally "not-false" ? For a side project of mine, I've started to use "True" to mean proven and "False" to mean not-proven, under the argument that if it were disproven, that's the same as a true proof for a counterargument.
- boris_m 5y ago
  There is no equivalent to "neither true nor false" in classical logic, because in classical logic there are no propositions that are neither true or false. Actually, there is no "neither true nor false" in intuitionistic logic as well, because there is no True and False in a first place. There is only Proven and not Proven. Don't think in terms of true and false, think in terms of proofs
  - tunesmith 5y ago
    But in intuitionist logic, "not proven" is bottom or disproven. So what is the concept for "neither proven nor disproven"? Is that literally "not disproven"?
    - drdeca 5y ago
      “Not proven” isn’t the same as implies bottom/Falsum? As I understand it, one can have a proof, or one can have a disproof (I.e. a machine that takes as input a proof of the statement and produces a proof of Falsum), or one can just, not have either of those things. You never have a “I don’t have a proof” with which to do things with, even if you don’t have a proof. Regarding the truth of a given statement, you can either say that there is a proof of it, or you can stay silent about it (while possibly saying something about another statement, e.g. saying that there is a proof of the negation of the original statement).
      - tunesmith 5y ago
        > "Not proven" isn't the same as implies bottom/Falsum? The article states: ¬A is A → ⊥. But how would you logically express "A is neither proven nor disproven"? It seems to me that if "A" is proven, and "~A" is disproven, then maybe "~~A" is neither proven nor disproven. Is that right? Since intuitionist logic doesn't have the double negation elimination axiom?

Bost 5y ago

I started to read the first chapter of your book, it looks nice. If I may ask you, could you also provide answers to the questions you ask? Somewhat hidden, e.g. behind a button "Show me the answer". I often I think I know the answer, but A) my answer may be wrong or B) I'm right but my reasoning is wrong. (So I'd like to compare my answer with yours.) Thanks.

boris_m 5y ago
Thanks for the suggestion

unknown_apostle 5y ago

What are good introductory books for logic (classical and intuitionistic)? For category theory? Do you know any similar representation of paraconsistent logic?

boris_m 5y ago
For category theory, I like Spivak's books. For logic, it really depends of what you are searching for, for classical logic you can read the the classics, for example Russell and Tarski. For constructive logic I cannot think of a good introduction (besides mine ;) ), I personally picked it up from books about category theory and computer science.
bitdiddle 5y ago
I think the general program of categorical logic, the work of Lambek and Scott, and J. Bell on topos theory and local set theory really make clear the relationship between category theory and logic, as well as lambda calculus. A topos is essentially a cartesian closed category with a subject classifier. In Set this is the two element set of 1/0 which is a Boolean algebra and thus the internal logic of the category Set is classical. In general though the subobject classifier is a heyting algebra which expresses the semantics of intuitionistic logic. There is also a very good, but introductory, book by Goldblatt on Topoi that covers this logical aspect So in terms of logics the category of Sets is the exception. By internal logic I mean that for every topos one builds up a theory using it's objects and function between them. An equivalence theorem (see J. Bell) states that a given topos is essentially equal to the category generated by this internal theory. This program began with Lawvere who noticed that conjunction and implication were really adjoints, the same one as between the product and hom functors in a cartesian closed category.

deleted 5y ago

[deleted]

amelius 5y ago

There's a typo in this section header: > Axiom schemas/Rules of inferene

boris_m 5y ago
Thanks

atsmyles 5y ago

I'm still learning Cat theory myself (through the Category for Programmers book). I have a couple of questions/observations (that I would love your opinion on). First observation: True and False are the limit and co-limit of the Bool Category. Question 1: About ordering, would you say that ordering is a requirement (as in a necessary property) of Cat Theory? It was mentioned in Bartosz Milewski's book but it wasn't as strongly emphasized as in your article. Question 2: You mention how you can't express "A or not A" using intuistic logic. Since it is expressible in Set Theory, could we not use an Adjoint between the Bool and Set Categories respectively? Specifically Kan extensions?

boris_m 5y ago
The bool category is not involved in this. True and False are the initial and terminal object (related to limit and colimit, but not the same thing) of all logical categories as I call them, of which there are many (one for each set of axioms that you might construct). 1. Ordering is not required for a category to be a category, the necessary requirements are just the ones listed in the beginning of the book. It is just that orders can be seen as categories. 2. You can express "A or not A" in intuitionistic logic it is just that it is not necessarily true. Also, not sure how would you express that or any logical relation in set theory.

still_grokking 5y ago

What an amazing write-up! I've picked up those things peace by peace form Wikipedia to be able to understand the slang in Haskell land. But it was a long and puzzling process. This great summary offered here will hopefully help other people in the future get a coherent picture more quickly. (I hope the SEO is good so people will find it. I'm at least going to recommend it form now on whenever someone asks related questions). It could be extended with type-theory I guess. Also I would be interested to know more about the relation of those things described with abstract geometry and/or topology. But it's fantastic already as it stands!

smusamashah 5y ago

Hi, would it using different shapes altogether, instead same circle with different colors, be a better choice? Colors are soft too which makes the contrast between any two circles very low and hard to differentiate.

crawfordcomeaux 5y ago

Thank you for all of this and the large type, too! Would you do uncertainty logic next? https://arxiv.org/abs/1506.03123 https://arxiv.org/abs/1506.03123 https://arxiv.org/abs/1810.01310 https://arxiv.org/abs/1810.01310

boris_m 5y ago
In this book I am focused on category theory, but I may write some more about logic in other places.
- crawfordcomeaux 5y ago
  I've really been wanting a friendly-like-what-you've-made category theory treatment of those two papers is what I'm trying to say. I've been assuming most/all things in life are uncertain. It's had a profoundly helpful impact on my life, so I'm trying to come to a deeper understanding of how to reason about an uncertain universe, which I think may be something a lot of people are needing these days. The first paper helped a bit, but I haven't really dug into and understood most of it.

tunesmith 5y ago

I'm curious in intuitionist logic what is the concept for "not proven", like neither true nor false? It's not "not-true" because going by your article it seems that would be "disproven" or bottom. Is it literally "not-false" ? For a side project of mine, I've started to use "True" to mean proven and "False" to mean not-proven, under the argument that if it were disproven, that's the same as a true proof for a counterargument.

boris_m 5y ago
There is no equivalent to "neither true nor false" in classical logic, because in classical logic there are no propositions that are neither true or false. Actually, there is no "neither true nor false" in intuitionistic logic as well, because there is no True and False in a first place. There is only Proven and not Proven. Don't think in terms of true and false, think in terms of proofs
- tunesmith 5y ago
  But in intuitionist logic, "not proven" is bottom or disproven. So what is the concept for "neither proven nor disproven"? Is that literally "not disproven"?
  - drdeca 5y ago
    “Not proven” isn’t the same as implies bottom/Falsum? As I understand it, one can have a proof, or one can have a disproof (I.e. a machine that takes as input a proof of the statement and produces a proof of Falsum), or one can just, not have either of those things. You never have a “I don’t have a proof” with which to do things with, even if you don’t have a proof. Regarding the truth of a given statement, you can either say that there is a proof of it, or you can stay silent about it (while possibly saying something about another statement, e.g. saying that there is a proof of the negation of the original statement).
    - tunesmith 5y ago
      > "Not proven" isn't the same as implies bottom/Falsum? The article states: ¬A is A → ⊥. But how would you logically express "A is neither proven nor disproven"? It seems to me that if "A" is proven, and "~A" is disproven, then maybe "~~A" is neither proven nor disproven. Is that right? Since intuitionist logic doesn't have the double negation elimination axiom?