Worrying About 2-Logic
Posted by David Corfield
Here’s a possible problem for the idea of modal logic as 2-logic.
In ordinary first order logic a model of a theory is a set . To an -ary predicate of the theory we assign a subset of , to a constant an element of , and so on.
For a given , we can derive a Galois correspondence between theories modelled on and subgroups of , the permutations of , as Todd shows.
Now, in first order modal logic (FoS4) a model of a theory is a sheaf. To show completeness we can stick with bog standard sheaves on topological spaces, as Awodey and Kishida show in their paper Topology and Modality. This combines the topological semantics of propositional modal logic with the set-valued semantics of first-order logic. Necessity relates to taking the interior of subsets of the base space.
So here’s the problem: if groups measured the symmetries of a model of first order logic, we want 2-groups to measure the symmetries of a model of 2-logic. But what are the symmetries of a sheaf? Well a sheaf is a functor, so we’d expect the symmetries to be the group of invertible natural transformations from the functor to itself, or sheaf automorphisms. Where’s the 2-group?
[Where do sheaves of groups fit in?]
Or is this the wrong way to think of it? Is it possible that we should be ‘permuting’ the base space too, as was suggested at some point in the Klein 2-geometry programme.
But why not look more directly for the kind of theory which has a category/groupoid as a model? And which interprets an -ary predicate as a functor from to Set, and so on.
I’m not sure why but the question popped into my head as to whether there’s any interest in the symmetries of a topos. E.g., what’s AUT(Set) and AUT(Sh())?
Re: Worrying about 2-logic
I think AUT(Set) is trivial. More precisely, if we define AUT(Set) as the category whose objects are equivalences and whose maps are natural transformations, then I think AUT(Set) is equivalent to the terminal category.
I haven’t gone through this in detail, but the idea is as follows. Any automorphism (i.e. self-equivalence) of preserves both terminal objects and sums. Since every object of is a sum of copies of the terminal object, for all sets . Moreover, there’s a canonical choice of such an isomorphism for each . “And so on.”
I don’t think it’s going to make much difference if you consider geometric morphisms rather than functors — after all, these are equivalences.
The 2-functor Sh from locales to toposes embeds Locales as a reflective sub-2-category of Toposes. (The reflector is: take subobjects of the terminal object.) In particular, it’s a full embedding. So for locales and , there’s an equivalence of categories So I reckon .