Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 4, 2011

Category Theoretic Modal Logic

Posted by David Corfield

I’ve mentioned before that it hasn’t been easy selling category theory to philosophers. At first glance this may be a little surprising when you consider what effects changes to the foundational language of mathematics circa 1900 had on philosophy over subsequent years via the influence of Bertrand Russell. Perhaps one of the most important factors was that predicate logic could be applied straightforwardly to natural language in a way that appeared to resolve certain metaphysical questions. Just look at the baldness of the present King of France.

Now something which is dearly beloved of analytic philosophers of the very purest kind is modal logic. So were category theory to become an indispensable tool in modal logic, we might be onto a winner. This has partially motivated a couple of posts of mine (here and here). Let me see if I can sum up the confused state of my mind at present. Even if you don’t want to think about modal logic, I’ve put in a couple of questions which I’d love to hear answers to.

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, BABA, 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 opB^{op} to BABA with certain properties, where BB 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 opB^{op} to MAMA, 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 opB^{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 BB to StoneBA opStone \cong BA^{op}. One might imagine then that in the passage to modal semantics we would have functors H:BDGFMA opH: 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 BB is the opposite of natural numbers with functions. These are called metaframes.

In this case where B opB^{op} is the natural numbers with mappings, on the syntax side, sitting above nn there is the Boolean or modal algebra of logically equivalent formulas whose free variables are contained in the set {x 1,...,x n}\{x_1, ..., x_n\}. Then on the dual semantic side, above 00 we have a Stone space of worlds, H(0)H(0), and above 11 a space of individuals, H(1)H(1). The map 101 \to 0 gives a fibring of individuals onto worlds. H(n)H(n) are similarly fibred over worlds. Particular attention has been paid to cases where a fibre of H(n)H(n) is the nn-fold product of the fibre of H(1)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 BB 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)H(1) determines H(n)H(n), all of the information is presumably encoded in the ‘bundle’ H(1)H(0)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 opBAP: Set^{op} \to BA, where PP 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 opB^{op} to IAIA, 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 XSet^X, for some set XX, it struck me that there was a strong resemblance to Richard Garner’s paper on ionads, with his comonads on Set XSet^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?

Posted at April 4, 2011 4:44 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2379

22 Comments & 0 Trackbacks

Re: Category Theoretic Modal Logic

I feel like the answer to questions 1 and 2 ought to be that there is an adjunction

Sem:hyperdoctrinescategories:Sub Sem : \text{hyperdoctrines} \;\rightleftarrows\; \text{categories} : Sub

in which the right adjoint SubSub sends a category to its hyperdoctrine of subobjects, and is probably fully faithful. Then a model of a hyperdoctrine DD in a category CC could equivalently be defined as a hyperdoctrine morphism DSub(C)D \to Sub(C) (the powerset hyperdoctrine Set opBASet^{op}\to BA being Sub(Set)Sub(Set)), or as a functor Sem(D)CSem(D) \to C; so Sem(D)Sem(D) is the “universal category containing a DD-model”. And if one starts with a more syntactically presented theory, one ought to be able to construct its syntactic category by first constructing its syntactic hyperdoctrine, then applying the left adjoint SemSem.

I don’t recall seeing anything quite like this written down anywhere, though. But I’m not that well up on the literature of hyperdoctrines, so it might be well known, or I suppose it might be false. I think I know one way to define the functor SemSem, though: first construct an allegory from the hyperdoctrine, then split its comonads (= coreflexives).

Posted by: Mike Shulman on April 5, 2011 6:11 AM | Permalink | PGP Sig | Reply to this

Re: Category Theoretic Modal Logic

Thanks, Mike.

Am I right to think hyperdoctrines fell out of favour relative to the syntactic category approach? I see these slides – Introduction to categorical logic – by Tom Hirschowitz mentions (p. 4) the triangle, hyperdoctrines/categories/allegories, treats the first two, and describes the hyperdoctrine approach as a “naive idea” (p. 6).

Hmm, I see on p. 86 an adjunction between the category of hyperdoctrines and that of first-order theories. I’ve no time right now to check how the latter is constructed.

Posted by: David Corfield on April 5, 2011 9:39 AM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

I wouldn’t presume to say for sure, but it does also seem to me that hyperdoctrines are sometimes ignored. The Elephant doesn’t mention them at all, for instance. It took me a while to find out about them.

Tom’s slides construct the adjunction

syntactic theorieshyperdoctrines \text{syntactic theories} \;\rightleftarrows\; \text{hyperdoctrines}

which fits on the left of the one I was proposing; the construction is, I think, fairly straightforward. And I just noticed that in appendix B of Categories, Allegories, the functor

syntactic theoriesallegories \text{syntactic theories} \to \text{allegories}

is constructed, which I am saying ought to factor through hyperdoctrines.

Posted by: Mike Shulman on April 5, 2011 4:49 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

A correspondent pointed out to me that hyperdoctrines have been subsumed by fibred categories.

Is there a general statement: hyperdoctrines are fibred categories satisfying such and such properties? And where do indexed categories fit in?

Posted by: David Corfield on April 6, 2011 10:41 AM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

That seems to me like an odd thing to say. Fibered categories are an equivalent way of describing indexed categories; which one you use is a matter of preference. A hyperdoctrine is a (fibered category or indexed category) with various additional properties; the notion of hyperdoctrine doesn’t seem to me to depend on whether you pick “fibered” or “indexed” to start with.

Posted by: Mike Shulman on April 6, 2011 4:46 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

That seems to me like an odd thing to say.

I’m not quite sure what is odd. My correspondent didn’t mention indexed categories. I only brought them up because I wanted to hear what their relationship is to fibred categories.

So now I know they’re equivalent. Good, one less thing to worry about.

Posted by: David Corfield on April 6, 2011 7:12 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

So now I know they’re equivalent.

…in the presence of Choice. :) Or using any of the standard methods to get around not having Choice, like profunctors/distributors, anafunctors.

Posted by: David Roberts on April 6, 2011 11:12 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

I just meant, since hyperdoctrines are a specific sort of fibered category, I don’t see how they could be “subsumed” by them. I guess maybe your correspondent meant that nowadays people prefer to say “fibered category satisfying X, Y, and Z” rather than “hyperdoctrine”, which is certainly reasonable.

Posted by: Mike Shulman on April 7, 2011 1:38 AM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

Thanks to David for reminding me of this thread here.

Meanwhile I had been collecting relevant material in an nnLab entry titled relation between type theory and category theory.

My impression is that the most comprehensive results for traditional theory here are due to Seely, who in two articles in 1987 establishes both an equivalence (not just an adjunction)

FirstOrderTheoriesHyperdoctrines FirstOrderTheories \simeq Hyperdoctrines

as well as

DependentTypeTheoriesLocallyCartesianClosedCategories. DependentTypeTheories \simeq LocallyCartesianClosedCategories \,.

Posted by: Urs Schreiber on May 16, 2012 12:18 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

Seely’s result apparently doesn’t deal sufficiently carefully with the coherence question: substitution in type theory is strict, but pullback in a category is not. This was rectified by Hoffmann, but perhaps the full equivalence was only proven in this recent paper.

Posted by: Mike Shulman on May 16, 2012 4:38 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

Thanks, yes, we overlapped with posting this. I have now tried to work it all into the entry.

But even given this flaw, now fixed, I am a bit puzzled by the status of the literature on this point.

For instance that, as David pointed out above, Tom Hirschowitz states fairly recently here an adjunction where more than two decades ago Seely claimed already an equivalence. This discrepancy cannot be due to the subtlety of categorical interpreation of substitution, unless I am missing something. What is going on here?

Posted by: Urs Schreiber on May 16, 2012 5:43 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

Concerning Q2 and Mike Shulman’s comment, I think what he denotes by “Sem: hyperdoctrines -> categories” is the tripos-to-topos construction, originally due to Hyland-Johnstone-Pitts.

The adjunction between triposes (hyperdoctrines with higher-order structures) and toposes is worked out in Frey’s recent preprint “A 2-Categorical Analysis of the Tripos-to-Topos Construction” in arXiv.

The construction works for first-order hyperdoctrines as well, and there is an adjunction between first-order hyperdoctrines and Heyting categories. But I do not know if it is worked out in the literature.

NB: these adjunctions do not form equivalences, since different hyperdoctrines can give rise to equivalent toposes (or Heyting categories). Sorry if I misunderstand anything.

Posted by: Yoshihiro Maruyama on May 22, 2013 10:05 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

Thanks for bringing up triposes! I must have forgotten about that school. I think you’re right.

Posted by: Mike Shulman on May 23, 2013 5:51 AM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

Interesting! So across the relevant ‘Stone’ duality, is there an analogous duality between some kind of indexed spaces and groupoids of models, the left hand vertical line here?

Posted by: David Corfield on May 24, 2013 9:11 AM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

The people gathering for Topology, Algebra, and Categories in Logic in Marseilles this July ought to be able to answer Question 3, especially if the program committee attends.

Posted by: David Corfield on April 5, 2011 9:42 AM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

Surely you must need some additional structure/conditions/something to define modal hyperdoctrines beyond just letting them be arbitrary functors B opMAB^\mathrm{op} \to \mathit{MA}?

If we think of the category BB as a category of contexts and substitutions, then BB’s functoriality ensures that formulas’ truth-values are well-behaved with respect to substitution, since substitutions induce modal algebra homomorphisms. However, it seems quite common for the domain of quantification to depend on the world. For example, we may wish the domain of the quantifier “for all dogs d” to range over the set of dogs in each world.

It’s not immediately obvious to me how to adapt hyperdoctrines to this case. Is this not interesting, or simply not part of the definition of first-order modal logic you are using?

Posted by: Neel Krishnaswami on April 5, 2011 4:15 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

I certainly didn’t mean general functors from B opB^{op} to MAMA. I took Kracht and Kurz’s word that the case was similar to Boolean hyperdoctrines:

A modal hyperdoctrine is a covariant functor HH from Σ\Sigma [natural numbers and mappings between them] into the category MAMA of modal algebras. H(n)H(n) may be thought of as the algebra of meanings of formulae containing nn free variables. To be well–defined, HH must satisfy among other the so–called Beck-Chevalley-condition, which ensures that cylindrification has the same meaning on all levels. (p. 43)

Are you saying more conditions should apply? Going over to the semantics side (with some sort of spec operation here?), there’s certainly debate as to quantification in a frame. Some want you to be able to quantify from a world over all individuals of all worlds, i.e., all possible individuals. Others want you to be able to quantify only over individuals in one world. Yet others have objects as traces (‘bundle sections’) across all worlds.

So, yes, I ought to work out if one form of quantification works better with modal hyperdoctrines.

Posted by: David Corfield on April 5, 2011 5:21 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

Yes, I think you need more than the Beck-Chevalley conditions (which I forgot to mention). Beck-Chevalley corresponds to the fact substitution goes through the quantifiers – i.e., that [t/x](y.ϕ)=y.([t/x]ϕ)[t/x](\forall y.\;\phi) = \forall y.\;([t/x]\phi) (and similarly for existentials).

The case I was thinking of was that in Kripke semantics, the forcing condition for quantification is often written as:

w γx.ϕ[x]vI(w).w (γ,xv)ϕ[x] w \models_\gamma \forall x.\;\phi[x] \iff \forall v \in I(w).\; w \models_{(\gamma,x \mapsto v)} \phi[x]

Here ww is a world, γ\gamma is a context assigning individuals to variables, and I:WorldSetI : \mathrm{World} \to \mathrm{Set} is a function that tells you what the individuals available in ww are. So this condition states that x.ϕ\forall x.\;\phi holds in ww when ϕ\phi holds for every vI(w)v \in I(w).

It’s the fact that II is world-dependent that makes me concerned about this, since a hyperdoctrine uses products in BB to model the environment, but the forcing condition gives you a product of a whole bunch of different collections of individuals.

I’m sure that there must be some nice categorical description of this, but I don’t know what it should be offhand.

Some googling turns up Hilken and Rydeheard’s “A First Order Modal Logic and its Sheaf Models”, whose abstract (and a quick skim) seems to suggest it is concerned with this problem:

Abstract: We present a new way of formulating rst order modal logic which circumvents the usual difficulties associated with variables changing their reference on moving between states. This formulation allows a very general notion of model (sheaf models). The key idea is the introduction of syntax for describing relations between individuals in related states. This adds an extra degree of expressiveness to the logic, and also appears to provide a means of describing the dynamic behaviour of computational systems in a way somewhat dierent from traditional program logics.

I don’t know what its connection to Awodey and Kishida is though.

Posted by: Neel Krishnaswami on April 6, 2011 9:11 AM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

“I don’t know what its connection to Awodey and Kishida is though.”

the former (from 1999) is superseded by the latter (from 2008): we clean up and generalize the sheaf semantics given there, and prove a strengthened version of the completeness theorem wished for in that paper.

Posted by: Steve Awodey on April 6, 2011 6:38 PM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

Hi David,
I haven’t read the Awodey and Kishida paper you’ve mentioned. yet. I just ‘discovered’ this thread. but there are at least two other approaches to categorical modal logic that I like ‘better’. One is mine with Gavin Bierman, for S4, you can read it in “On an Intuitionistic Modal Logic”, Studia Logica (65):383-416, 2000 and follow-up work like “Categorical and Kripke Semantics for Constructive S4 Modal Logic” (with Natasha Alechina and and Michael Mendler and Eike Ritter). In Proc. of Computer Science Logic (CSL’01), LNCS 2142, ed L. Fribourg. 2001.. (ok, I guess I’m a little biased…)
but joking apart, even if you don’t buy into the whole idea of extending the categorical Curry-Howard isomorphism to modal types (which I and lots of other people do) there is also the work of Claudio Hermida,
A categorical outlook on relational modalities and simulations
http://maggie.cs.queensu.ca/chermida/papers/sat-sim-IandC.pdf that you should/could check up.
Very best,
Valeria de Paiva

Posted by: Valeria de Paiva on October 12, 2011 7:05 AM | Permalink | Reply to this

Re: Category Theoretic Modal Logic


http://www.sciencedirect.com/science/article/pii/S1571066104051801

“This paper connects coalgebra with a long discussion in the foundations of game theory on the modeling of type spaces. We argue that type spaces are coalgebras, that universal type spaces are final coalgebras, and that the modal logics already proposed in the economic theory literature are closely related to those in recent work in coalgebraic modal logic. In the other direction, the categories of interest in this work are usually measurable spaces or compact (Hausdorff) topological spaces. A coalgebraic version of the construction of the universal type space due to Heifetz and Samet [Journal of Economic Theory 82 (2) (1998) 324–341] is generalized for some functors in those categories.”

I think in order to be foundational (more truly descriptive of reality in a broader sense) it has to be this way.

Posted by: Stephen Harris on October 17, 2011 8:27 AM | Permalink | Reply to this

Re: Category Theoretic Modal Logic

I wrote in the post that Richard Garner’s paper on ionads

doesn’t mention modal logic.

This was true of the version available on the ArXiv at the time (v2, 8 Dec 2009), however, looking at the latest version (v3, 15 Oct 2011) of the paper Ionads, we read

These, then, are two quite general grounds for preferring toposes over ionads; yet there remain good reasons for having the notion of ionad available to us. The first is that some particular applications of topos theory may be more perspicuously expressed in the language of ionads than of toposes: two examples that come to mind are the sheaf-theoretic semantics for first-order modal logic given in [1], and the generalised Stone duality of [5].

[1] is the Awodey and Kishida paper, and [5] Forssell’s PhD thesis, partially written up in the Awodey and Forssell paper, referred to in the post.

Posted by: David Corfield on March 10, 2013 3:27 PM | Permalink | Reply to this

Post a New Comment