I gave a few talks this past summer about Kit Fine’s Semantics for Quantified Relevance Logics. I mentioned a few times that the models in Fine’s semantics are pretty “sheafy”. For a variety of reasons, I’ve finally decided to work out the details of how this goes. Since a sheaf is a special type of presheaf and a presheaf is a type of contravariant functor and contravariant functors are ways of hooking together two categories, a natural starting point is figuring out which categories we need to look at.
If you comb through the details of the completeness proof Fine gives while keeping the general idea of what a sheaf is at the front of your mind, one of the categories yells its identity at you and the other whispers a few hints. The one that yells at you is the category whose objects are finite sets of variables and whose arrows are inclusions among these. (Aside: Fine’s definition allows us to use something more general that, interestingly, has (to me) a Grothendieck-y smell; I’m ignoring this for simplicity.) The presheaves we’re interested in will be contravariant functors from this category (let’s call it Fin) to the aforementioned category-that-whispers.
What’s clear about the whisperer is that its objects should be models for a polyadic unquantified language. What’s unclear is what the arrows in this category should be. But this morning I think I saw what the answer is, so today I’ll try to work out the details and then tomorrow, I’ll say things about what I learn.