Why Rationalists Shouldn't be Interested in Topos Theory
post by jollybard · 2020-05-25T05:35:03.193Z · LW · GW · 15 commentsContents
Topoï and toposes Topoï-logical Where's my Bayesian topos? (Geometric) topoï aren't reflective What now? None 15 comments
I spent a lot of the last two years getting really into categorical logic (as in, using category theory [LW · GW] to study logic), because I'm really into logic, and category theory seemed to be able to provide cool alternate foundations of mathematics.
Turns out it doesn't really.
Don't get me wrong, I still think it's interesting and useful, and it did provide me with a very cosmopolitan view of logical systems (more on that later). But category theory is not suitable for foundations or even meant to be foundational. Most category theorists use an extended version of set theory as foundations!
In fact, its purpose is best seen as exactly dual to that of foundations: while set theory allows you to build things from the ground up, category theory allows you to organize things from high above. A category by itself is not so interesting; one often studies a category in terms of how it maps from and into other categories (including itself!), with functors, and, most usefully, adjunctions.
Ahem. This wasn't even on topic.
I want to talk about a particular subject in categorical logic, perhaps the most well-studied one, which is topos theory, and why I believe it be to useless for rationality, so that others may avoid retreading my path. The thesis of this post is that probabilities aren't (intuitionistic) truth values.
Topoï and toposes
A topos is perhaps best seen not even as category, but as an alternate mathematical universe. They are, essentially, "weird set theories". Case in point: itself is a topos, and other toposes are often constructed as categories of functors , for an arbitrary category.
(Functors assemble into categories if you take natural transformations between them. That basically means that you have maps , such that if you compare the images of a path under and , all the little squares commute.)
Consider that natural numbers, with their usual ordering like , can form a category if you take instead So one simple example is to consider the category of all functors , which are really just sequences of sets, like
where the arrows are regular set theoretic functions. You can do practically any kind of mathematical reasoning using sequences of sets! (as long as it is constructive) For example, you have
- an "empty set", which is just a sequence of empty sets;
- a "point" given by a sequence of points;
- "products" of sequences given by
and so on. Most interestingly, you have truth values given by subobjects of the point; accordingly, in those are the empty set and the point itself, since , corresponding to true and false. Notice that ; in fact the truth values in general will have the structure of a partially ordered set.
What are our truth values here? What is a subobject of a sequence of points? For one, each has to be a subset of . And there are no maps ; so each "truth value" will look like
a bunch of empty sets and, at some position , all points, meaning that we have as many truth values as natural numbers. This is our first glance into the cosmopolitan nature of topos theory: weird truth values! Notice, however, that if , their corresponding subobjects will have this ordering reversed (an exercise left for the already knowledgeable reader); so in the end it might have been better to use functors on , natural numbers with their order reversed.
To sum up, we made the category of sequences of sets, and realized that it was a topos with truth values . Isn't it that interesting...
Topoï-logical
Turns out there's a big connection between toposes and topological spaces.
The open sets of a topological space have the structure of a partially ordered set, if you set whenever . Moreover, in that poset, you can describe as the greatest lower bound of and , and as their least upper bound.
This is in fact (almost) exactly the structure we want of our topos-theoretic poset of truth values: the greatest lower bound corresponds to conjunction and least upper bound is the disjunction . So we can use topological spaces as spaces of truth values, and this is in fact the approach used in Heyting semantics of intuitionistic logic.
(so each open set, and not point, corresponds to a truth value; you take the AND of two open sets to be their intersection and the OR to be their union)
Alright, so as with , the poset of open sets can define a category if you set whenever . So take a topological space and its category of open sets. We'll define a new category of functors , except that they won't be all of the functors, only those that preserve the topo/logical structure (sheaves).
Guess what? Not only is a topos, turns out that its truth values are isomorphic to ! And since the truth values are the subobjects of the point, that means that the points of the topos are in fact shaped like ...
Now we have a fuller view of the logically cosmopolitan view that topos theory can bring us. You can create, just like that, a whole parallel mathematical universe of bizarro sets where everything is made up of, say, donuts. Or coffee cups. It is as you wish.
Where's my Bayesian topos?
Since I am at heart a LessWronger, and since I care deeply about problems of logical induction and logical counterfactuals and whatnot, I spent a while trying to design a topos that would behave like manipulating probabilities. Or distributions. Or something. With the objective of making something that would represent beliefs.
Well, I'm sorry, but it doesn't work.
At minimum, we would expect that the truth values of this topos be probabilities, yeah? And with the cosmopolitan principle above, we could then just take the sheaves on this poset of probabilistic truth values.
So these truth-values would be order-isomorphic to [0,1]. But for them to actually represent probabilities, we'd want that , and yet the order on already prescribes that , and we are doomed from the start.
Furthermore, even in an intuitionistic logic, the provable statements all have the maximal truth value (which here would be 1); but we all know that 0 and 1 are not probabilities [LW · GW], and so nothing should be provable... which seems like it wouldn't be very useful.
All in all, I'm truly sorry you had to bear through all of the math above just for this conclusion. It's still pretty cool, though, right?
(Geometric) topoï aren't reflective
In order to legitimately use topos theory for rationality, we should have a way for the topos to "think about itself". Analogously to the situation in Peano arithmetic [LW · GW], for a topos , we'd want some object (specifically, an internal category) to be isomorphic to in some sense.
We can define an "element" of an object as being an arrow . So the objects of the internal category are given by the set , and in fact the functor respects the structure of the internal category enough that it becomes a category internal to , which is just a small category.
But wait. The toposes generated by sheaves on a topological space are at least as big as , but the collection of all sets is too big to be a set, and thus we run into size issues.
It should in principle be possible to do so in small toposes, such as the free (as in syntactic) topos, but I am not sure and will refrain from claiming so. It is however certainly possible to do so in list-arithmetic pretoposes (yes it's a mouthful), as shown by André Joyal in his as of yet unpublished categorical proof of Gödel's incompleteness theorems, which I have studied with him last year.
What now?
It now seems to me that linear logic might be the "right" weakening of classical logic into something probabilistic. I still need to figure out some of the details, but let's say that the work has already been done, and one need only piece it together into something relevant to rationality and agent foundations. Particularly promising is that some claim that linear logic is a good setting for "paraconsistent" logic (logic that deals gracefully with contradictions), which could make it work for logical counterfactuals.
All this and more in my next post, pretentiously monikered "Probability Monads".
15 comments
Comments sorted by top scores.
comment by Vanessa Kosoy (vanessa-kosoy) · 2020-05-25T08:42:12.932Z · LW(p) · GW(p)
I spent a lot of the last two years getting really into categorical logic (as in, using category theory to study logic), because I'm really into logic, and category theory seemed to be able to provide cool alternate foundations of mathematics.
Turns out it doesn't really.
Category thing doesn't. But, (the closely related) homotopy type theory does.
Replies from: jollybard↑ comment by jollybard · 2020-05-25T08:47:19.083Z · LW(p) · GW(p)
Indeed, and -categories can provide semantics of homotopy type theory. But -categories are ultimately based on sets. At some point though maybe we'll use HoTT to "provide semantics" to set theories, who knows.
In general, there's a close syntax-semantics relationship between category theory and type theory. I was expecting to touch on that in my next post, though!
EDIT: Just to be clear, type theory is a good alternate foundation, and type theory is the internal language of categories.
comment by Adele Lopez (adele-lopez-1) · 2020-05-26T00:14:18.312Z · LW(p) · GW(p)
I've ran into this too, and I think that quasitopoi are also a dead-end for this sort of thing. I'm currently interested in linear logic as well!
comment by MrMind · 2020-05-25T10:50:52.460Z · LW(p) · GW(p)
I've also dabbled into the matter, and I have two observation:
- I'm not sure that probabilities should be understood as truth values. I cannot prove it, but my gut feeling is telling me that they are two different things altogether. Sure, operations on truth values should turn into operations on probabilities, but their underlying logic is different (probabilities after all should be measures, while truth values are algebras)
- While 0 and 1 are not (good) epistemic probabilities, they are of paramount importance in any model of probability. For example, P(X|X) = 1, so 0/1 should be included in any model of probability
↑ comment by jollybard · 2020-05-25T19:49:01.406Z · LW(p) · GW(p)
I'm not sure that probabilities should be understood as truth values. I cannot prove it, but my gut feeling is telling me that they are two different things altogether.
My feeling is that the arguments I give above are pretty decent reasons to think that they're not truth values! As I wrote: "The thesis of this post is that probabilities aren't (intuitionistic) truth values."
Replies from: MrMindcomment by Morgan_Rogers · 2022-03-12T15:37:49.548Z · LW(p) · GW(p)
[0,1] is a commutative quantale when equipped with its usual multiplication. You can lift the monoidal product structure to sheaves on [0,1] (viewed as a frame) via Day convolution. So we recover a topos where the truth values are probabilities.
People who have attempted to build toposes with probabilities as truth values have also failed to notice this. Take Isham and Doering's paper, for example, (which I personally am quite averse to because they bullishly follow through on constructing toposes with certain properties which are barely justified). They don't even think about products of probabilities.
I think the monoidal topos on the unit interval merits some serious investigation.
comment by Krow · 2020-05-25T12:25:26.050Z · LW(p) · GW(p)
- Here is a list of various notions of probability measures developed in category theory, might be useful (with lots of references). I have no idea if any of these notions somehow fit well with linear logic though.
That being said if you are aiming to create a language for bayesian probabilities, I think it would be interesting to look in particular into continuous valuations on dcpos (see previous link), and try to somehow apply this stuff to the framework developed by Paul Taylor , which gives a constructive account of topology. Plus he's quite opinionated and fun to read too. - And an aside on reflectivity. In general any sufficiently general logical construct does not have this property: set universes are not reflective; types of types in type theories are not either; NF is the one exception I know of but suffers from some pathologies such as not allowing currying. So overall I do not think this is a reasonable expectation to have.
However toposes are partially reflective: their (impoverished) internal version of themselves is their set of truth values. A way to see this is that you get back the poset of truth values if you collapse all hom-sets of your topos into singletons (which is like seing all objects as propositions instead of sets).
This is related to Lawvere-Tierney topologies , which give a way of "modifying" your topos through an operation on its set of truth values only (and this is equivalent to taking sheaves on a site in a presheaf topos, so pretty much all "nice" toposes arise in this way).
I would use this as a guideline for what to expect of a reflective operation in a good enough probabilistic universe.
comment by Keith L (keith-l) · 2024-06-02T18:58:01.198Z · LW(p) · GW(p)
You don't NEED to build CT on set theory. Like most math, the ideas are mostly independent of the foundations built under them. ZFC or whatever is just the default.
comment by Clamwinds · 2020-05-25T06:28:26.491Z · LW(p) · GW(p)
Interesting. Ever hear of the work of Jean-Yves-Girard? (You mentioned mathematical logic) I hear his book "The Blind Spot" is an excellent lecture on the nature of mathematical truth by a seasoned veteran of such difficult affairs.
Replies from: rhollerith_dot_com, jollybard↑ comment by RHollerith (rhollerith_dot_com) · 2020-05-25T13:36:46.750Z · LW(p) · GW(p)
I like Girard. The Rust programming language's borrow checker probably wouldn't've been invented yet if it weren't for Girard's 1987 paper, "Linear logic". (The paper got sustained attention from numerous programming-languages researchers; I read many thousands of papers on programming-language design before the appearance of Girard 1987 and I can recall no exploration of the use of linear types, use-once variables or whatever you want to call them before Girard 1987.)
↑ comment by jollybard · 2020-05-25T06:37:16.854Z · LW(p) · GW(p)
Yes, I have! Girard is very... opinionated, he is fun to read for that reason. That is, Jean-Yves has some spicy takes:
Quantum logic is indeed a sort of punishment inflicted on nature, guilty of not yielding to the prejudices of logicians… just like Xerxes had the Hellespont – which had destroyed a boat bridge – whipped.
I enjoyed his book "Proofs and Types" as an introduction to type theory and the Curry-Howard correspondence. I've looked through "The Blind Spot" a bit and it also seemed like a fun read. Of course, you can't avoid his name if you're interested in linear logic (as I currently am), since the guy invented it.
comment by dsatan · 2020-06-19T23:33:41.076Z · LW(p) · GW(p)
If you're so interested in logical induction, aren't you already assuming that classical mathematics is The One True Logic? Why is that? Why not look at ordinary mathematics internal to a topos and then ask what logical induction looks like for that?
And as for reflection, a topos with a NNO has (higher order) primitive recursion so your claim about not having reflection is confusing.
And lastly, your title doesn't match your thesis. All you show is that you can't directly do probability in toposes. Category theory is extraordinarily useful for many areas of mathematics in general, and is more than just a language. See Beck's monadicity theorem, the adjoint functor theorem, the small object argument, Gabriel Ulmer duality, and so on for nontrivial results in category theory.
Maybe you shouldn't base your entire identity around doing probability theory. At the very least, epistemology spills far beyond the purview of probability theory.