The n-Category Café

To relate all this to something perhaps familiar, when you introduce the necessity operator $\square$ into a propositional theory, semantically you start thinking about the accessibility of one world from another. So, $\square P$ (it is necessarily the case that $P$) holds in my world if $P$ holds in all worlds accessible from my world. This accessibility relation is thus a relation $R$ between worlds, or in other words a coalgebra for the powerset functor:

$$R: X \to P(X).$$

Properties of the modalities, such as $\square P \vdash \square \square P$, correspond to properties of the relation, here transitivity.

But there are many other modalities we might want to consider, as explained here:

One large class of logics is the vast and growing family of modal logics, which are characterised by having operators that qualify formulas as holding in a certain way, e.g. ‘necessarily’, ‘in the future’, ‘everywhere’, ‘probably’, ‘as everyone knows’, or ‘normally’. (p. 1)

All of these are needed to analyse typical statements:

In a seemingly simple piece of knowledge such as ‘Normally, the likelihood of road congestion is smaller on weekends’, one implicitly makes use of default logics (‘normally’), probabilistic reasoning (‘the likelihood’) and temporal knowledge (‘weekends’) under a quantitative regime (‘smaller’).

In the case of probabilistic modalities, we might want modal operators such as

it is at least $p \%$ probable that at the next step $\phi$.

On the semantic side of this operator, we will need to revist our old friend the Giry monad which sends a set to the set of subprobability distributions it supports. Coalgebras for this functor are Markov chains. The resulting logic is Probabilistic modal logic.

We can even consider the $\pi$-calculus as a modal logic:

we use the presheaf category $N$ of functors from finite sets (of channel names) with injective renamings to a certain category of domains (representing observable behaviour in the presence of recursion). (p. 5)

The endofunctor on the semantic side, i.e., on $N$ is

$$Pi(X) = \mathcal{P}(X + N \times X^N + N \times (N \times X) + N \times \delta X).$$

We read Pi as follows. The possible one-step behaviours of a process are non-deterministic (due to $\mathcal{P}$) and may be one of the following alternatives: A silent step (the $X$ component), an input of a name $(X^N)$ over a channel $(N)$, the output of a free name over a channel (due to $N \times N \times X$) or the allocation and sending of a fresh name (the $N \times \delta(X)$-part). (p. 5)

This results in a “new fully abstract, sound and complete modal logic for the $\pi$-calculus”. For more details see Pi-Calculus in Logical Form.

Perhaps we can now start to glimpse connections between two pieces of work out of Carnegie-Mellon that we have commented on before. On the one hand, there’s the syntax-semantics duality of first-order theories due to Forssell. Here the dualising object is no longer $2$ but rather the category $Set$. Just as $2$ can be taken as equipped with many structures, so with $Set$.

For example, $Set$ is a category with finite products, and an object in the category, $\mathcal{F} \mathcal{P}$, of such categories with finite product preserving functors. But it is also a category with all limits and colimits, and an object in the category, $\mathcal{G}$, of such categories with functors which preserve limits, filtered colimits, and regular epimorphisms. This allows for the following duality, as Forssell explains,

• Models = $Hom_{\mathcal{F} \mathcal{P}} (Algebraic theory, Set)$
• Algebraic theory = $Hom_{\mathcal{G}} (Models, Set)$.

He goes on to show the duality between Boolean coherent categories (corresponding to first-order theories) and topological groupoids (corresponding to their models). We might hope then for modalities acting on the first-order syntax and semantics to be functors (maybe 2-functors) of a certain kind on these Boolean coherent categories.

We can think of the transition systems between models or worlds of propositional theories as telling us which members of a set of worlds are close to one another. For any ordered pair can we move from the first to the second – Yes or No? Now with first-order theories we’re working in a category of worlds and we want to know for any objects not just whether we can get from one to another, but how.

The trivial choice of transition system for a set is where $a R b$ if and only if $a = b$. This corresponds to the coalgebra $\a \mapsto \{a\}$. The equivalent for categories is, I would guess, the Yoneda embedding as a 2-coalgebra. Here an object relates to another via the arrows in the category itself. But presumably there must be other transition systems to work with.

The second piece of Carnegie-Mellon work may give us a clue as to how to proceed. It’s Awodey and Kishida’s sheaf semantics for first order modal logic. Here we model first-order modal logic by a sheaf over a space of worlds. A fibre contains the individuals living in the world indexed by a point in the base space.

So the question is: can these sheaf models for a first-order modal theory be seen as (2)-coalgebras for some endofunctor on the category of models of the nonmodal first-order theory?

The thrust of the coalgebraic approach to modal propositional logic is summarised as:

First, the coalgebraic model is flexible. That is, it can incorporate many different types of behaviour and interaction, e.g. location awareness, mobility and quantitative uncertainty, to name but a few. Second, the coalgebraic model is compositional: both on the logical and the semantical level it allows us to combine computational features and reason about their interaction. Third, the coalgebraic model is uniform, i.e. all computational aspects of the model share the same meta-theory. This in particular leads to software tools that are easier to design, to maintain and to implement. Finally, the coalgebraic model is compatible in the sense that it subsumes nearly all existing formal notions of state based system as special cases. (p. 10)

It would fun to extend this to first-order theories. There must be quite a space of logics out there.