Michael Shulman categorified logic

In talking about 2-toposes and classifying discrete opfibrations it is common to hear people talk about “the category of sets being a generalized object of truth values,” or more loosely of “treating sets as truth values.” (See, for instance, the discussion at this post.) The idea, of course, is that just as the functor

$$X\mapsto Sub(X)$$

from $Set$ (or any topos) to posets is representable by the set $\Omega$ of truth values, the functor

$$X\mapsto DOpf(X)$$

from $Cat$ (or, hypothetically, any 2-topos) to categories is representable by the category $Set$ of sets. Here $DOpf(X)$ means the category of discrete opfibrations over $X$.

My current opinion is that there already exists a “logic which treats sets as truth values,” without the need for any categorification, namely type theory (more precisely, dependent type theory). It is central to categorical logic (although not always presented in this way) that the internal logic of a category $C$ actually takes place in the fibration $X\mapsto Sub(X)$ of subobjects of objects of $C$. In particular:

• The Heyting algebra operations in each poset $Sub(X)$ correspond to the logical connectives $\wedge,\vee,\top,\bot,\Rightarrow,\neg$.
• The reindexing functors $f^*:Sub(Y)\to Sub(X)$ correspond to logical substitution, weakening, and contraction.
• Left adjoints to reindexing functors correspond to existential quantification.
• Right adjoints to reindexing functors correspond to universal quantification.

The fact that the resulting logic is a “logic of truth values,” or as I would say a “logic of (-1,0)-categories,” depends on each $Sub(X)$ being a poset; that is, a (0,1)-category. However, for an ordinary category $C$ we also have a fundamental fibration $X\mapsto C/X$ of 1-categories, which has a corresponding “logic of 0-categories,” that is, sets. If $C$ is (for instance) a locally cartesian closed category with finite colimits, then each $C/X$ is a cartesian closed category with finite colimits (the 1-categorical analogue of a Heyting algebra) and the reindexing functors have left and right adjoints.

Now, instead of interpreting these operations as acting on logical statements that are either true or false, we interpret them as acting on types which can be inhabited or empty, but if inhabited can contain many different elements. For instance, instead of constructing a new proposition $\varphi\wedge\psi$ from propositions $\varphi$ and $\psi$, we construct a new type $A\times B$ from types $A$ and $B$. And instead of constructing a new proposition $(\forall x\in A)\varphi(x)$ from a proposition $\varphi$ that depends on a variable $x$, we construct a new type $\Pi_{x\in A} B(x)$ (a “dependent product”) from a type $B(x)$ that depends on $x$.

There are several different ways of thinking about this. From one perspective, we can think of these types as merely “souped up” versions of propositions that record not only whether something is true, but all the “ways” in which it can be true or all the “proofs” that it is true. Thus, our real interest is in whether a given type is inhabited or not, which is a close generalization of whether a given proposition is true. I believe this is often called the propositions as types paradigm.

On the other hand, we can treat the types as sets whose different elements we may care about, and it is from this perspective that I want to view it. In this case, we may also want to say things about the elements of those sets, which is to say, we also need a logic (of propositions) on top of our type theory (the “logic of sets”). This construction of a “logic over a type theory” is very common in type theory, and seems to be the generally accepted way to develop the internal logic of a $\Pi$-pretopos. From an $n$-categorical point of view, what we have is a 1-category in which we have both a “logic of 0-categories” (type theory) that takes place in the slice categories $C/X$ and a “logic of (-1,0)-categories” (ordinary logic) that takes place in the slice posets $Sub_C(X)$.

It is now clear how to categorify this: in a 2-category $K$ we will have a “logic of 1-categories” that takes place in the slice 2-categories $K/X$, a “logic of 0-categories” that takes place in the slice 1-categories $disc(K/X)$, and a “logic of (-1,0)-categories” that takes place in the slice posets $Sub_K(X)$. (Actually, we could easily add logics of (1,0)-categories and (0,1)-categories taking place in $gpd(K/X)$ and $pos(K/X)$, respectively, but this doesn’t seem to be as useful.) The only possibly-unexpected wrinkle is that it turns out to be best to ues the fibrational slices $Fib_K(X)$ and $Opf_K(X)$ in place $K/X$ whenever possible.

From this perspective, it is evident that in “categorified logic” (at least as I conceive it) sets do not replace truth values. Rather, sets, and categories as well, have their own “logic” (aka “type theory”) which happens “underneath” the logic of truth values. The goal is that just as existing mathematical arguments involving sets can be formalized in the internal logic of a 1-topos, existing mathematical arguments involving categories should be formalizable in the internal logic of a 2-topos — and, empirically speaking, these arguments involving categories still use the same sort of (truth-valued) logic that arguments involving sets do. The only difference is that they involve categories (1-types) in addition to sets (0-types) and truth values ((-1)-types).

Something that would help me enormously (personally and convincing other philosophers) would be a concrete example to work with. It would be especially interesting if this could be in ‘natural language’, like my poodle example for 1-logic.

Perhaps an example from dependent type theory would do: During every month there exists a team for which there exists a day in that month on which every player on that team is fit.

It would be nicer though to have the meta-types be non-discrete categories.

You could try the following paper by Isar Stubbe: The canonical topology on a meet-semilattice which explicitly goes from Omega to Sets.