Arrows for Real

I want to preface this post by saying that there is almost certainly a more categorial way to say everything I'm going to say today. It would probably also be a worthwhile exercise to say things in the more categorial way. But I'll leave that to either a future post or to someone else. If you have thoughts on how to categorify the construction here, though, do let me know either via email or (better!) in the comments.

Recall from last time that a frame is a model without the domain or the valuation. So a frame has six pieces: a set of theories, a subset of which are the normal theories, a designated base theory, a binary closure operation acting on the theories, a binary containment relation holding among the theories, and a complementation function. A frame morphism is a function from the theories in one frame to the theories in another frame that (a) is monotonic, (b) is unital, and (c) commutes with reciprocation. More explicitly, we require first that if u extends t, then the image of u extends the image of t; second that the image of the base theory in the first frame be the base theory in the second frame; and third that the reciprocal of the image of a theory t is the image of the reciprocal of t. We say that a frame morphism is normal when the image of the set of prime theories in the first frame is exactly the set of prime theories in the second frame. We say a frame morphism is exact when the image of the closure of t under u is the closure of the image of t under the image of u.

One of the more intimidating aspects of Fine's paper is all the uparrows and downarrows running around in it. Here's an excerpt to illustrate the point:

OMGarrows.png

What these are, it turns out, is two whole famlies of functions. And, as the arrows suggest, they go in opposite directions: where the downarrow-functions might go from this to that, the uparrow functions will go from that to this. The fact that we need both families is what makes most straightforward categorifications either impossible or unwieldy.

The key to getting things to work nicely is to work in a category where arrows just are pairs of functions going in opposite directsion. To say more about this, we first need to bring valuations and domains back on the scene. We'll do so by thinking about models as being triples composed of a frame, a domain, and a valuation. First, define what it means for the pair consisting of the domain D1 and the valuation V1 to be a restriction of the pair [D2, V2] in the 'obvious' way: D1 is contained in D2 and V1 is what we get when we restrict V2 to D1. We only want arrows between models [F1,D1,V1] and [F2,D2,V2] when [D2,V2] is a restriction of [D1,V1]. When that does happen, an arrow is a pair of frame morphisms: a normal frame morphism from F1 to F2 and an exact frame morphism from F2 to F1.

Not just any old pair of this form will do, however. We require that they satisfy six conditions. But I'm not going to tell you what they are. Instead, I'm going to stop for today, because that was all technical stuff and no philosophical stuff. So in the next couple posts, I'm going to do philosophy instead. Eventually, we'll come back to the thread and actually give the conditions. After that, we'll check to make sure we've actually got a category on our hands. Of course, even then we're only halfway done -- the game is to build stratified models as some sort of presheaves, and all we'll have done is specified the categories we're interested in. So we'll still need to say something about which presheaves we want and why, and how to use them to do the whole semantics shtick. Then, if I'm feeling ambitious and things are going well, maybe I'll work through soundness and completeness proofs for the logic BQ with respect to this semantics. Or maybe I won't. Who knows? The world is a wild place.