Author here, let me know what you think.
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?
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.
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!
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.
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
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).
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?
Indeed, that is what ¬A means. "¬A" does not mean "not proven". It means that A implies a contradiction. I.e. It means not A. To have a proof of ¬A is to have a disproof of A.
"A is not proven" is not a statement in the language. You can't express it in the language. (if you want to add on some provability logic on top of intuitionistic logic, you can do that, but the basic language of intuitionistic logic does not have any way of expressing "it hasn't been proven that A".)
The "either it has been proven, or it hasn't been proven" isn't a statement made in the language, but a statement about, how to reason using the language.
"~~A" does not mean "neither proven nor disproven", it means -- -- well, it means what it says. It means not(not(A)) .
If you have a proof of A, you can use that to produce a proof of ~~A , but not the other way around. A proof of ~~A is, a disproof of ~A, essentially saying "if it could be shown that A implied a contradiction, that implication itself would imply a contradiction".
Would you do uncertainty logic next?
https://arxiv.org/abs/1506.03123 https://arxiv.org/abs/1810.01310
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.
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.
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.
> Axiom schemas/Rules of inferene