3

I've been reading through the extremely useful discussion of First-Order Categorial Logic that recently popped up over at The Diagonal Argument. But when I compare Baez and Weiss's construction to what's found over at the nLab, one striking difference is that where B&W build a covariant functor from FinSet (the category of finite sets with functions between them) to Bool (the category of boolean algebras) the nLab suggests hyperdoctrines will in general be contravariant functors.

Here are five ways I might explain this difference:

  1. B&W messed something up.
  2. the nLab folks have messed something up
  3. this is one of those weird facts that make classical logic funky, and it wouldn't matter if we used FinSet or FinSet$^{op}$, the result would be the same.
  4. B&W simplified some things, and this is one of the consequences of the simplification
  5. Something else entirely.

My question: which of these is to blame and, if it's number 5, can you elaborate at all? (2) seems unlikely, since all the publications cited by the nLab folks also assume contravariance. But I felt obligated to include it for completeness sake.

Tom
  • 33
  • 4

3 Answers3

2

(This answer is basically the same as Dan Doel's. We wrote them in parallel, but he posted first. I decided this may still be helpful.)

Unsurprisingly, no one's wrong.

In the nLab article for hyperdoctrines, it talks about "contexts" and classical logic being the case where $T$ is a "category of contexts". For something like first-order logic, what we call the "context" has two parts, usually left implicit. There's a variable context that tells us which free variables are allowed and what their sorts are, and then there are the assumptions. I'm going to focus on the variable contexts, though in some cases these things mix together. As an example, imagine a multi-sorted theory of vector spaces. If we want to say $r(\mathbf v+\mathbf u)=r\mathbf v+r\mathbf u$ we need to specify that $r$ is a scalar, and $\mathbf v$ and $\mathbf u$ are vectors. We could write this like: $r:S,\mathbf v:V,\mathbf u:V\vdash r(\mathbf v+\mathbf u)=r\mathbf v+r\mathbf u$, where $S$ and $V$ are the two sorts of our theory.

The question now is how do we represent variable contexts. The most obvious choice is to think of them like tuples of sorts. We can drop the variable names and just use their positions, giving us something like an object like $S\times V\times V$ identifying the variable context for the above formula. If we want to "forget" the scalar, we can use the projection $S\times V\times V\to V\times V$. When we use a functor to map this category, which we can define to be the category with finite products freely generated by a set of objects (which represent the sorts), we find that it should be contravariant. It's not clear how to turn a formula like $r(\mathbf v+\mathbf u)=r\mathbf v+r\mathbf u$ into one that doesn't have $r$ free, but it's clear how to turn a formula like $\mathbf u+\mathbf v=\mathbf v+\mathbf u$ into one that does have $r$ free. As another example, given the diagonal $V\to V\times V$, we can turn a formula with two variables free, e.g. $\mathbf u-\mathbf v = 0$, into a formula with one variable free, i.e. $\mathbf u-\mathbf u=0$.

Now, in the single-sorted case, we can simplify notation by writing $S\times S$ as $S^2$ and so forth. The diagonal arrow $S\to S^2$ can then be described via $S^{!_2}$ which is the pre-composition of $S$ with $!_2 : 2\to 1$ in the category $\mathbf{FinOrd}$. ($\mathbf{FinOrd}$ is the skeleton of $\mathbf{FinSet}$ and thus they are equivalent.) In other words, we have a contravariant functor $\mathbf{FinOrd}$ to $T$. In fact, $\mathbf{FinOrd}$ is the category with finite coproducts freely generated by a single object. In other words, if we define $T$ to be, in the single-sorted case, the category with finite products freely generated by a single object, then $T\simeq\mathbf{FinOrd}^{op}$. This is basically what Baez is doing. He chooses $T=\mathbf{FinSet}^{op}$ producing $T^{op}\to\mathbf C$ or $\mathbf{FinSet}\to\mathbf C$.

Derek Elkins left SE
  • 24,967
  • The last three sentences here are supremely useful in making the categorical perspective on what’s going on apparent. I love it when that happens. Reading along like yeah ok yeah ok, then suddenly, BLAM!! Ah! That’s what’s happening. Awesome. – Tom Jul 13 '19 at 14:27
2

Baez and Weiss are talking about something Baez is calling "polyadic Boolean algebras", which are functors from $\mathbf{FinSet}\to\mathbf{Bool}$, for instance, $n\mapsto \mathcal{P}(V^n)=\mathbf{Set}(V^n,\{0,1\})$ for a fixed set $V$. This is covariant since a function $f:n\to m$ induces a function $V^f:V^m\to V^n$, which then induces the pullback function $\mathcal{P}(V^f):\mathcal{P}(V^n)\to \mathcal{P}(V^m)$. There is a closely related hyperdoctrine $\mathcal P:\mathbf{Set}^{\mathrm{op}}\to \mathbf{Bool}$ which is just $\mathcal P$ itself, but these aren't trying to talk about quite the same thing.

Kevin Carlson
  • 52,457
  • 4
  • 59
  • 113
  • Could you help me with this please https://math.stackexchange.com/questions/3292324/show-the-quotient-space-of-a-finite-collection-of-disjoint-2-simplices-obtained? Thank you! – Nash Jul 15 '19 at 19:38
2

I'm sure Kevin's answer is correct, but here's some additional stuff to chew on from someone whose understanding of this is more about type theory and computer science.

I think the answer is that it's actually a hyperdoctrine on $\mathbf{FinSet}^{op}$. A reason this might be the case is that this category arises naturally when modelling variable binding, which is something you might want to study categorically in the fields above. The way you might go about this is as follows:

We want a category for talking about variables bound in a context. The variables will all just range over a single universe of discourse, rather than having possibly distinct types. So, we will accomplish this by taking a Cartesian category freely generated by one object $U$. $1$ is the empty context, $U$ is a 1-variable context, $U×U$ is a 2-variable context, and $U^n$ is an $n$-variable context. A map $U^m → U^n$ decomposes into $n$ projections from $U^m$, saying how each of the $n$ variables in the result is bound in the $U^m$ context. You can think of this like:

$$x_1, x_2, ..., x_n ⊢ x_i, x_j, x_j,...,x_k$$

expressing some kind of simultaneous substitution of variables with contraction, weakening and exchange. Now, presheaves on this category can be used for talking about algebras with variable binding.

But, consider what I mentioned about the maps. A map $f : U^m → U^n$ is equivalent to for each $i < n$ a specification of which projection $π_j : U^m → U$ is used. Another way to look at this is that we have a function $[n] → [m]$ specifying this information ($[n]$ being a finite set of size $n$). So, the context category we built is equivalent to $\mathbf{FinSet}^{op}$, and presheaves/hyperdoctrines on it are functors out of $\mathbf{FinSet}$.

If you want a more thorough explanation of the variable binding stuff, see here.

Dan Doel
  • 3,715
  • This is aggravatingly close to being an explanation I understand. But I think you and I have different understandings of what “context” and “variable binding” mean, and I keep tripping over my understanding of these terms when I try to understand your answer. I think that you are using “context” to mean something like “a specification of what values some of the variables take” and “bound in a context” to mean “given a value in said context”. But if so I don’t see why maps $U^m\to U^n$ decompose on the way you say they do. – Tom Jul 13 '19 at 14:08
  • Hang on, maybe I’ve got it: a map $U^m\to U^n$ should be a way of taking an assignment of values to these variables and turning it into an assignment of values to those variables. We do this by specifying, for each of those variables, which of these variables it should behave like. I think that lines up with what you’ve said. – Tom Jul 13 '19 at 14:16
  • I think you have it in the second comment. That the maps decompose that way is a consequence of the way the category is defined, though. Maps into a product $f : A → U^n$ correspond to $n$ maps $f_i : A → U$. And every map $U^m → U$ is a projection of some sort, because there are no other maps in 'the free cartesian category with one object $U$'. However, this structure acts similarly to structural rules for keeping track of variables. It's similar to de Bruijn indices. $m$ says how many variables are available, and $π_i : U^m → U$ says to reference the $i$-th variable. – Dan Doel Jul 13 '19 at 17:14
  • When we go to presheaves $F : \mathsf{Ctx}^{\mathsf{op}} → \mathsf{Set}$, $F(U^n)$ can be thought of as like a set of terms valid in an $n$-variable context. Then if we have $σ : U^m → U^n$, which is a substitution for $n$ variables in an $m$-variable context, $F(σ) : F(U^n) → F(U^m)$ tells us how to get the $m$-variable equivalent of an $n$-variable term by performing the substitution $σ$. If you were doing this with de Bruijn indices, you might use σ : Vec n (Fin m), if that's meaningful to you. – Dan Doel Jul 13 '19 at 17:29