The n-Category Café

First, we have the coalgebraic approach to modal logic, where we build on the duality between Stone spaces and Boolean algebras. As described in Stone coalgebras we can derive an endofunctor on the category of Boolean algebras, $BA$, from a modal operator, algebras for which are modal algebras (think Lindenbaum algebra of a propositional logic having the necessary operator $\Box$ applied). On the other side of the duality, we have the Vietoris functor on Stone spaces, and coalgebras for this functor are descriptive general frames. So we have modal algebras and descriptive general frames in duality. Kripke frames are a particular case of these general frames.

Now for the first-order case, we might use hyperdoctrines. In one form of these, typed classical first-order hyperdoctrines, we have a functor from $B^{op}$ to $BA$ with certain properties, where $B$ is a category with finite products corresponding to the types of the theory. The extension to modal logic should then involve a modal hyperdoctrine, a functor $B^{op}$ to $MA$, the category of modal algebras. Such a modal hyperdoctrine is described in Logically Possible Worlds and Counterpart Semantics for Modal Logic in the special case where $B^{op}$ is the category of natural numbers and functions. It also crops up in the paper First-order modal logic, but I don’t have access to that at the moment.

Over on the semantics side, Dion Coumans’ slides describe duals for Boolean hyperdoctrines as indexed Stone Spaces, certain functors from $B$ to $Stone \cong BA^{op}$. One might imagine then that in the passage to modal semantics we would have functors $H: B \to DGF \cong MA^{op}$, which we might call indexed descriptive general frames. Now, there exists something like this already in the literature in the particular case where $B$ is the opposite of natural numbers with functions. These are called metaframes.

In this case where $B^{op}$ is the natural numbers with mappings, on the syntax side, sitting above $n$ there is the Boolean or modal algebra of logically equivalent formulas whose free variables are contained in the set $\{x_1, ..., x_n\}$. Then on the dual semantic side, above $0$ we have a Stone space of worlds, $H(0)$, and above $1$ a space of individuals, $H(1)$. The map $1 \to 0$ gives a fibring of individuals onto worlds. $H(n)$ are similarly fibred over worlds. Particular attention has been paid to cases where a fibre of $H(n)$ is the $n$-fold product of the fibre of $H(1)$. These metaframes are called cartesian, and it is known, according to Kracht and Kutz, that

all modal predicate logics are complete with respect to cartesian metaframes.

Using different categories for $B$ would allow for typed modal logics.

The frame aspect of first-order modal logic captures ‘counterpart’ relations between individuals. This is a notion due to the philosopher David Lewis, who took possible world talk very seriously. If ‘I might have had eggs for breakfast’ is true in this world, it is made true by the existence of a close world in which my counterpart did have eggs for breakfast. The sorts of complexity one would need to capture include an individual in this world having no counterparts or many of them in an accessible world. With some homotopic nontriviality thrown in, one could imagine a loop in the space of possible worlds along which taking the counterpart relation permutes individuals.

In this ‘cartesian’ case where $H(1)$ determines $H(n)$, all of the information is presumably encoded in the ‘bundle’ $H(1) \to H(0)$, where the image of the counterpart relation for individuals is the accessibility relation for worlds. This would explain interest in Kripke sheaves.

According to the Kracht and Kutz paper (p. 26), Hyperdoctrinal Semantics and General Metaframes for modal logic are treated in Hiroyuki Shirasu, Duality in Superintuitionistic and Modal Predicate Logics, Advances in Modal Logic, volume 1 (Marcus Kracht et. al., editor), CSLI Publications, Stanford, 1998, pp. 223-236. Again I don’t have access to that.

Now, what about models?

Qu. 1: Do you typically characterise the models of hyperdoctrines via maps to a special hyperdoctrine, e.g., in the case of Boolean ones to the hyperdoctrine $P: Set^{op} \to BA$, where $P$ is power set?

You would think that you could also address models for first-order modal logic via the syntactic category route. Mike gave me a hint as to the relation between hyperdoctrines and syntactic categories here. But I’d like to know the answer to

Qu. 2: Is there a systematic way of translating between hyperdoctrines and syntactic categories for classical first-order logic?

As far as classical first-order theories go, syntactic categories are Boolean coherent. So, then, Awodey and Forssell’s duality between the category of ($\kappa$-small) Boolean pretoposes and Stone topological groupoids might possibly provide the equivalent of Stone duality for the coalgebraic approach.

Somehow I feel all this ought to tie in with the other approach to the semantics of first-order modal logic, I have mentioned in earlier posts, Awodey and Kishida’s sheaf semantics. Here the modal logic is S4. Were there to be a connection to the coalgebraic approach above, we might need a notion of interior hyperdoctrine, $B^{op}$ to $IA$, the category of interior algebras.

Anyway, Awodey and Kishida explain how what they are doing can be thought to be extending from Kripke sheaves to sheaves over general topological spaces, rather than merely those generated using the Alexandroff topology from a preorder.

Noticing that they are dealing with a sort of interior endofunctor on $Set^X$, for some set $X$, it struck me that there was a strong resemblance to Richard Garner’s paper on ionads, with his comonads on $Set^X$, although his paper doesn’t mention modal logic. [EDIT: See below.] Interestingly, one of Garner’s examples of an ionad ((5) from p. 8) deals with sets (of isomorphism classes) of models for a coherent theory.

Hmm, I see how muddled is my mind on all this, so

Qu 3: Am I glimpsing anything worthwhile here?