[HN Gopher] Category Theory Illustrated - Logic
___________________________________________________________________
Category Theory Illustrated - Logic
Author : todsacerdoti
Score : 233 points
Date : 2021-09-26 11:57 UTC (11 hours ago)
(HTM) web link (boris-marinov.github.io)
(TXT) w3m dump (boris-marinov.github.io)
| boris_m wrote:
| Author here, let me know what you think.
| atsmyles wrote:
| 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 wrote:
| 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.
| Bost wrote:
| 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 wrote:
| Thanks for the suggestion
| unknown_apostle wrote:
| What are good introductory books for logic (classical and
| intuitionistic)? For category theory? Do you know any similar
| representation of paraconsistent logic?
| bitdiddle wrote:
| 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.
| boris_m wrote:
| 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.
| crawfordcomeaux wrote:
| 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/1810.01310
| boris_m wrote:
| In this book I am focused on category theory, but I may write
| some more about logic in other places.
| [deleted]
| amelius wrote:
| There's a typo in this section header:
|
| > Axiom schemas/Rules of inferene
| boris_m wrote:
| Thanks
| still_grokking wrote:
| 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 wrote:
| 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.
| tunesmith wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| "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 wrote:
| > "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?
| hidden-spyder wrote:
| How did _this_ repost survive even though the author had already
| posted it a few minutes before?
|
| Original: https://news.ycombinator.com/item?id=28660131
| ivalm wrote:
| > Logic is the science of the possible. As such, it is at the
| root of all other sciences, all of which are sciences of the
| actual, i.e. that which really exists
|
| I really don't think this is right. Logic is a discipline of
| consistent re-writing of expressions. However, there may be (even
| existing) things that are not expressable to sufficient degree in
| finite (or even countably infinite) strings, which I think means
| they are outside of logic. There are definitely "possible" things
| that are outside of logic (because not expressable).
| deltasixeight wrote:
| No. You are both wrong.
|
| Logic is one of the fundamental axioms of the universe. We
| assume logic is true and consistently applies everywhere
| throughout the universe. This "rewriting expressions" thing is
| just a symbolic representation of logic. It is not logic in
| itself. The symbolic representation of logic by writing down
| "expressions" works because logic is a inherit property of our
| universe and since you are writing those "expressions" in that
| same universe, it works.
|
| There is no way to prove or verify logic is consistently real.
| We just recursively assume logic is real. We observe it to be
| real and assume that the observation will consistently apply
| across all time and space.
|
| Another thing that I should mention that is an axiom of our
| universe is probability. WE have no way of knowing why rolling
| dice or random variables follow the rules of probability. These
| are just arbitrary rules and we assume that they're
| consistently true about our universe. Logic along with
| probability are two things that we have zero methodology of
| verifying the veracity of but we just assume these two things
| are fundamental properties of the universe.
|
| A more elegant way to look at it is to just assume probability
| is the foundational axiom of our universe. Logic is just a
| special case of probability where all causal connections are
| 100%. Of course given inherit unreliability and limited
| knowledge of all things we never actually see or can verify
| 100% causality on anything. This effectively limits logic to
| mathematical and axiomatic games while science is the only
| available tool for the real world.
|
| Science is a whole different beast. Given the assumptions that
| probability is real and that logic is real, science is an
| attempted methodology to verify theorems or statements about
| the universe using the axioms of probability and logic.
|
| For example Newton guesses that a ball should travel a certain
| distance according to his made up laws of motion. Using science
| we perform several experimental observations of moving a ball
| and statistically correlate to a certain degree that yes the
| ball does indeed move according to newtons laws of motion. This
| is what science is. It is making a hypothesis and using
| statistics to sort of verify it. The term "sort of" is key here
| because science is limited to the fact that it can never prove
| anything.
|
| One thing to note here is that EVEN when we assume logic and
| probability is true, science is unable to prove anything is
| true. You can make 10,000 observations about newtons law, it
| proves nothing because at any point in time a new observation
| can render the entire hypothesis as false. Thus falsification
| is possible with science [1] but proof is impossible. Proof is
| the domain of mathematics and logic games and cannot exist in
| the real world due to limited knowledge.
|
| This is not some pedantic philosophy I'm making up. This is
| foundational to a true understanding of what science and logic
| is. To quote Einstein:
|
| "No amount of experimentation can ever prove me right; a single
| experiment can prove me wrong."
|
| There are a lot of intelligent people who don't understand the
| true depth of the above quote. But if you get it, then you
| truly understand what science is, and the differences between
| science and logic. Obviously both the OP and the parent poster
| don't fully get it... by combining logic and science into one
| thing and calling it the "science of the possible" it shows
| that they don't have a clear delineation of the two terms. Most
| people think of science as some kind of fuzzy "technical study"
| of a topic. No. This is wrong. There is a clearer definition of
| science that separates it from logic and mathematics.
|
| [1] Note that technically total falsification is also
| impossible. Inherit unreliability of observation tools and
| limited knowledge makes it so that no observation can be 100%
| reliable. Thus even falsification is technically limited to the
| domain of logic and mathematical games.
| ivalm wrote:
| > Logic is one of the fundamental axioms of the universe
|
| This definitely a very opinionated view on what is logic.
| There is no reason to embed anything in universe/anything
| else. If you remove expressability, I'm not sure what
| properties remain. At the same time you can have rules
| outside of anything physical (in a sense of denoting
| something that subsists). Consistency of re-writing rules (in
| a sense that one can always write a propositional string that
| cannot be reduced to true or false), is an entirely separate
| beast.
|
| > Logic is just a special case of probability
|
| This is factually false. Probability is embeddable into
| predicate logic, but predicate logic is not embeddable into
| (Bayesian) probability. This is actually an open problem (how
| to define a probability theory that is equivalent to
| predicate logic).
|
| > Science is a whole different beast
|
| On this I do agree, I wouldn't call logic a "science."
| systemvoltage wrote:
| > This definitely a very opinionated view on what is logic.
|
| It is by definition, not opinion.
| Koshkin wrote:
| > _Logic is one of the fundamental axioms of the universe._
|
| Is it the classical logic of the quantum logic you are
| talking about?
| deltasixeight wrote:
| Hard to say which came first. Probability can be defined in
| terms of axioms and classical logic just read any
| probability book. Classical logic can also be defined in
| terms of probability by setting all causal relations to be
| 100% (See bayes theorem).
|
| I'm making a vague sweeping statement here that eventually
| gets a bit more cleared up later in my writeup.
| roenxi wrote:
| > Logic is the science of the possible. As such, it is at the
| root of all other sciences, all of which are sciences of the
| actual, i.e. that which really exists.
|
| Not the focus of the article, but a good view of logic is that it
| is the art of consistency. A powerful, single-purpose tool to
| tell its user if they hold mutually inconsistent beliefs. I can
| believe that the sky is blue, the sky is green and that the sky
| is exactly one colour - but if I use logic I can detect that
| something in my worldview is woefully broken.
| appleflaxen wrote:
| Great formulation.
|
| One could also say that logic is the study of what is not
| disproven.
| boris_m wrote:
| Also a good formulation. It's amazing how little has been
| written on the subject (of what logic is.)
| bmitc wrote:
| > It's amazing how little has been written on the subject (of
| what logic is.)
|
| I'm not sure that's the case. Just searching "philosophy of
| logic" yields oodles of resources. It's an entire field of
| study.
| boris_m wrote:
| I meant at a higher lever.
| bmitc wrote:
| I'm not really sure what you mean by higher level, but
| I'm still not sure that's the case if one is assuming you
| mean works that are more introductory in nature.
|
| For example, from the introduction in the first chapter,
| titled "Consistency", in Wilfred Hodge's _Logic_ :
|
| > Logic can be defined as the study of consistent sets of
| beliefs; this will be our starting-point. Some people
| prefer to define logic as the study of valid arguments.
| Between them and us there is no real disagreement, as
| section 11 will show. But consistency makes an easier
| beginning.
|
| > Logic is about consistency - but not about all types of
| consistency. ...
|
| > The type of consistency which concerns logicians is not
| loyalty or justice or sincerity; it is compatibility of
| beliefs. A set of beliefs is consistent if the beliefs
| are compatible with each other. To give a slightly more
| precise definition, which will guide us through the rest
| of this book: a set of beliefs is called consistent if
| these beliefs could all be true together in some possible
| situation. The set of beliefs is called inconsistent if
| there is no possible situation in which all the beliefs
| are true.
|
| Note that this is identical to the parent comment, and
| this book is originally from the 1970s.
| boris_m wrote:
| By higher level, I mean big picture. Not necessarily
| introductory, but ones that don't employ logical concepts
| such as "proof", "formal" etc, because you cannot define
| a field of study using concepts from that field. This
| example is good, but not sure what are you trying to say
| by posting it (I didn't say that noone ever wrote
| anything on what logic is.)
| drdeca wrote:
| > because you cannot define a field of study using
| concepts from that field.
|
| Why not?
| boris_m wrote:
| Because the definition would be circular.
| drdeca wrote:
| Does a field of study have to be defined in order for the
| concepts in it to be defined? I don't see why.
|
| Can't you define concepts x,y,z, and then define the
| field of study as being "about x,y,z and the things
| related to them"?
|
| I'm guessing you mean something different by "defining a
| field of study" (different from my default/initial
| interpretation of the phrase I mean), but I'm not sure
| what else you mean by it.
| [deleted]
| guerrilla wrote:
| Very much has been written at a higher level. There are
| thousands of advanceds books and dozens of specialized
| journals.
| pfortuny wrote:
| Well, Aristotle's studies on logic are called the "organon"
| (meaning "tool") exactly because of that.
| travisgriggs wrote:
| It is the set of all things not found under the category of
| illogical.
| Reflecticon wrote:
| How would you do that?
| IncRnd wrote:
| The assumption in what you wrote is that logic is Boolean,
| which is not always the case. There are other logics.
| rini17 wrote:
| Other logics need to have their own consistency rules too.
| Torwald wrote:
| > As such, it is at the root of all other sciences, all of which
| are sciences of the actual, i.e. that which really exists.
|
| I once read somewhere that theology is the science of the
| unknowable. So for how much theology is a science then is
| discussed within theology itself ie one cannot know how much of
| the unknowable is existing in an ontological sense.
| Koshkin wrote:
| I once read that philosophy and theology are similar to each
| other, in that "philosophy is seeking answers to questions that
| do not have answers; theology studies that which does not
| exist."
|
| (Incidentally, "science of the unknowable" seems like an
| oxymoron, because "science" means "knowledge"...)
| bmitc wrote:
| In my personal opinion, philosophy is about understanding
| what the questions even are and creating the tools needed for
| this understanding. So philosophy seeks to codify the
| questions and provide frameworks for answers to be framed in.
|
| All the sciences have questions that do not have answers.
|
| A good book that actually knows what it is talking about is
| _The Logic of Information_.
|
| https://www.amazon.com/Logic-Information-Theory-
| Philosophy-C...
| echopurity wrote:
| The epistemology in that logic section is terrible enough for HN
| to love this article.
| jerome-jh wrote:
| The definition of logic I retain comes from "Logique
| mathematique" from Rene Cori and Daniel Lascar, a pretty good
| book I have yet to finish ;)
|
| Logic models the mathematical reasoning itself, like vector
| spaces model our world and differential equations model most of
| physics. At no point however we should confuse the model with the
| studied object. As such logic is a field of mathematics and not
| mathematics itself. The best illustration of this is that
| theorems in the field of logic use results from e.g. set theory.
|
| Of course using a formal logic to prove theorems is valid. Still
| the formal logic has to be studied with "intuitive" mathematics.
| The book uses the metaphor of spiraling downstairs to illustrate
| this.
| amw-zero wrote:
| 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/), 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-
| 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 wrote:
| > 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..
| pphysch wrote:
| > 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.
| antonzabirko wrote:
| > Logic is the science of the possible. As such, it is at the
| root of all other sciences, all of which are sciences of the
| actual, i.e. that which really exists.
|
| Logic describes our universe well but even here it starts falling
| apart pretty fast. The idea of axiomatic systems as we know them
| is flawed. Mainly due to Godel's and partly from what we know of
| the psyche.
| amw-zero wrote:
| Godel's incompleteness theorem is very similar to the halting
| problem, in that they are both really profound results, but
| they have almost no bearing on the practical benefits of logic
| / computation.
|
| In the halting problem example, how often do you create
| infinite loops as a programmer? Even in the software
| verification space, proving termination of an algorithm is
| fairly simple. So, the halting problem doesn't really affect us
| in daily programming.
|
| The same with the incompleteness theorem. The fact that we
| can't say _every single thing possible_ (completeness) has no
| bearing on our ability to say _an innumerable amount of very
| practical things._
|
| The amount of things that formal logic can express is so vast
| and useful that, to call it "flawed" is a pretty big
| misunderstanding on the incompleteness theorem.
| guerby wrote:
| The halting problem is intractable only with infinite memory
| (infinite tape for turing machines).
|
| Our current computers all have finite memory and so a trivial
| algorithm can tell if a real program on a real computer will
| halt (terminate) or not.
|
| Of course the trivial algorithm has huge (but finite) memory
| requirement :)
| boris_m wrote:
| Well, it has it's limits, but wouldn't call it "flawed".
|
| Regarding the psyche part, I have actually written an article
| about that which might change your opinion https://boris-
| marinov.github.io/logic-thought/
| vcxy wrote:
| The incompleteness theorems don't imply a flaw. It's just a
| property of sufficiently rich systems.
| nafizh wrote:
| Category theory for programmers by Bartosz Milewski [0] is
| another great resource geared more towards how programmers can
| leverage it in their work.
|
| 0. https://bartoszmilewski.com/2014/10/28/category-theory-
| for-p...
| mushishi wrote:
| Milewski is almost my sole resource for category theory so far.
| I watched his lectures on youtube, and ordered that book as
| printed from here: https://www.blurb.com/b/9621951-category-
| theory-for-programm...
| jasperry wrote:
| Question about a claim in the article: "If classical logic is
| based on set theory, intuitionistic logic is based on category
| theory and its related theories."
|
| I'm no expert, but as I understood it, category theory can be
| used to construct a semantics for certain constructive logics,
| such as type theory, but to claim that intuitionistic logic is
| "based on" category theory seems off. A logic can exist all by
| itself, regardless of which theory is used to give semantics for
| it. Right?
| Koshkin wrote:
| Well, "classical logic is based on set theory" seems off too...
|
| In fact, a theory can always be formulated using a minimum
| number of axioms, so none requires some other theory as its
| base. For example, the system of real numbers can be built
| starting from the natural numbers, but what this achieves is,
| this just gives a "proof of existence" of the reals, i.e of
| consistency of the definition of the reals as a complete
| ordered field.
| foldr wrote:
| Yes, this seems completely off to me too. It's perhaps worth
| noting in this connection that intuitionistic logics predate
| anything that could reasonably be called "category theory".
| Ericson2314 wrote:
| Orthodox Set theory is a "standard library" for classical
| logic.
|
| It just so happens that the people who like one tend to like
| the other, and so explorations of the semantics of classical
| logic (mostly, model theory) use Set theory.
|
| The Tarski-style algebrization of logic which is "logics as
| orders" stuff from this article is an alternative to that one
| can do without category theory. Heyting algebra vs boolean
| algebra is sufficient to distinguish classical and
| intuitionistic logic.
|
| Category theory is this not necessary for intuitionism, but is
| nicer, because the point is to _compute_ things. Otherwise we
| just speak abstractly of what can be computed, which is like a
| pessimist compromise between realism and idealism.
|
| So
|
| Logic : order :: type theory : category
|
| Roughly, and the right side makes intuitionism a lot more
| exciting and applicable.
| boris_m wrote:
| Author here. Yes. Texts says " _If_ classical logic is based on
| set theory ", that is I am comparing the relations to set
| theory and category theory to that between classical logic and
| intuitionistic logic. I will try to fix the ambiguity.
| boris_m wrote:
| Corrected the sentence:
|
| "If we view classical logic as based on set theory, then
| intuitionistic logic would be based on category theory and
| its related theories."
|
| And regarding the fact that CT is not "needed" for algebraic
| logic what I say is "category theory _and its related
| theories_. " where I consider orders related to categories.
| gus_massa wrote:
| What software are you using for the graphics? Is it an
| specialized program or package, or just a generic graphic program
| like Inkscape?
| boris_m wrote:
| Inkscape.
| Koshkin wrote:
| Some believe that the two-valued logic is not sufficient and that
| you need the whole range of values from 0 to 1.
|
| https://bayes.wustl.edu/etj/prob/book.pdf
| mathgenius wrote:
| Bart Jacobs is working on a book that uses the language of
| category theory to develop probability theory:
|
| https://www.cs.ru.nl/B.Jacobs/PAPERS/ProbabilisticReasoning....
| crawfordcomeaux wrote:
| And some believe we need uncertainty to be accounted for, too!
|
| https://arxiv.org/abs/1506.03123
| https://arxiv.org/abs/1810.01310
| Koshkin wrote:
| > _Illustrated_
|
| Curiously, Category Theory appears to be the most "illustrated"
| mathematical theory by its very nature (because of the wide use
| of diagrams in any text on it) and, at the same time, the most
| misunderstood one (or, often, not understood at all) - because
| its _conceptual_ content and the patterns it considers are so
| deep that no amount of illustration could convey that depth, to
| the point that even drawing diagrams, however complex, is a skill
| comparable to being able to write numbers on a piece of paper -
| which is just as far from what we think what the understanding of
| the subject is.
| fn-mote wrote:
| > conceptual content and the patterns it considers are so deep
| that no amount of illustration could convey that depth
|
| My experience is different - for me category theory abstracts /
| generalizes / encodes ideas that we understand well in a
| particular setting. Intuition comes from particular examples
| and is then "categorified" to make more general arguments. Of
| course some times it goes the other way ("hey you really need
| to do X because the category you are working with doesn't have
| property Y").
|
| And sometimes the imported understanding is not quite accurate,
| like always there are issues. I don't think that impacts the
| main line of this argument, though it may be an example of the
| depth that category theory brings.
| pfortuny wrote:
| The moment limits appear, illustrations stop.
|
| Not to speak about "derived" concepts...
| fn-mote wrote:
| I guess you are talking about limits like in analysis, but
| even then I don't think this is really true. I'm not really
| sure if you intend to distinguish between limits and
| colimits; I'll assume not, but I would certainly agree that
| infinite (inverse) limits are harder to understand with
| diagrams.
|
| On a simple level, limits in category theory don't need to
| involve infinite things at all, you can take the limit over a
| small category like (x --> x <-- x).
|
| With regard to derived concepts, one can draw pictures of
| "projective resolutions" or draw level by level pictures of
| the nerve of the category you want to work with. So I think
| you can in fact make useful pictures even in this case.
| [deleted]
| pvg wrote:
| Plane geometry, arguably the OG mathematical theory, would
| probably take issue with who gets to be called 'most
| illustrated'.
| smusamashah wrote:
| These should have been shapes instead of all circles. Colors are
| soft too and it's hard to see the difference.
| mathgenius wrote:
| Yeah, I don't see how the colours are helping. It does make it
| look friendly and inviting, but switching back and forth
| between coloured balls and the usual symbolic mathematics
| (algebra notation) is jarring and confusing to me. Using
| colours instead of letters is a superficial trick and basically
| a step backwards. It's like those algebra memes where they use
| fruit instead of x, y, z etc. What's the point? But anyway I
| don't want to sound too dismissive because the mathematics
| literature definitely needs more of this kind of creativity!
| unknown_apostle wrote:
| At first sight, this looks like an absolutely great resource for
| a friendly introduction to this stuff. Thanks HN (and author).
___________________________________________________________________
(page generated 2021-09-26 23:00 UTC)