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 23, 2013

Modal Types

Posted by David Corfield

If Martin-Löf dependent type theory is a formal system which projects down via truncation to (typed) first-order logic, might we not expect there to be a modal type theory which would project down to first-order modal logic? I’ll use this post to play around with the idea.

Normally we take a modal logic to be a system which allows us to study certain ways of qualifying propositions.

It is necessarily the case that P; It is obligatory that P ; It is known that P, etc.

With first-order modal logic, these propositions may have free variables which we can then bind by a quantifier. This allows us to express controversial metaphysical theses such as:

‘Everything is necessarily self-identical’ or ‘For every thing, it is necessarily the case that that thing is identical to itself’ (x(x=x)\forall x \Box (x = x)).

It still seems that only propositions are modalised. But given all we’ve been hearing at the Café from Mike on type theory, we know that propositions can be considered as just a certain kind of type. Then, if we can modalise proposition-as-types, why not modalise all types? This is what happens in modal type theory.

Despite the enormous amount of attention given over to modal logic by philosophers, I’m unaware of any mention of the idea that modal operators could apply to anything other than propositions. Instead, the majority of the work in modal type theory occurs in computer science. To pick out one interpretation of ‘necessity’ from de Paiva, Goré and Mendler’s useful summary Modalities in constructive logics and type theories

…the constructive A\Box A singles out those terms of type AA that are “closed”, i.e., which are completely built from constructors over which primitive recursion is well-defined.

On the other hand, we’ve seen Urs and Mike working out higher modalities for physics, in the case of cohesive structures.

But in view of the fact that dependent type theory seems to fit well with natural language, is it not possible that we already have a trace of modal types in our everyday conversations? Let’s think. A director might say while casting

He’s a possible Hamlet.

Now, we might try to rewrite every instance of

X is a possible Y

as

It is possibly the case that X is a Y,

but this may do some violence to our inclination to attach the modality directly to a noun phrase. When cooking, some things are necessary ingredients for a dish, others optional. Beef is a necessary ingredient of a beef stew, while ale is only a possible ingredient.

Looking now at the epistemic modality, in my current state of knowledge, I may have France and Germany as known EU members, and China as a known non-EU member. I may also have Norway as a possible EU-member. Indeed, I can tag on ‘known (to me)’ to most noun phrases, and the dual ‘possible’ = ‘not known to be not’.

Thinking of dependent types, I may not know for sure someone’s nationality.

Karen is a possible citizen of Norway, hence, since I think Norway a possible EU country, as far as I know she is a possible EU citizen.

We would then need to see how modalities and dependent types interact. It seems we have

( c:EUCitizen(c)) c:EUCitizen(c)\diamond(\sum_{c: EU} Citizen(c)) \cong \sum_{c: \diamond EU} \diamond Citizen(c).

Given that dependent sum is what projects down to existential quantification, this might put us in mind of the so-called ‘Barcan formula’. One of the originators of first-order modal logic was the philosopher Ruth Barcan, who gave her name to a postulated entailment and its converse. These postulated entailments run between \exists \diamond and \diamond \exists.

I like that idea that intuitions concerning one level of logic or mathematics often arise from something deeper behind the scenes. So the intuitionists had picked up on something when they saw that P¬¬PP \to \not \not P was acceptable but not the converse. Behind the scenes, the former is natural, arising from currying the evaluation of an exponential (B A×ABB^A \times A \to B, where BB is falsity here).

What then of the Barcan and converse Barcan formulas? Well we had some discussion over at the nForum, and came to see that the converse Barcan was a projection of something natural in the presence of a certain pullback. So

XE X XE XE pb X X. \array{ \underset{X}{\sum}E \\ & \searrow \\ & & \underset{X}{\sum} \diamond_X E &\to& \diamond \underset{X}{\sum} E \\ && \downarrow &pb& \downarrow \\ && X &\to& \diamond X. } \,

Let’s illustrate this using the dependent type of players of teams:

playersofactualteams poss.playersofactualteams poss.playersofposs.teams pb actualteams poss.teams, \array{ players\, of\, actual\, teams \\ & \searrow \\ & & poss.\, players\, of\, actual\, teams &\to& poss.\, players\, of\, poss.\, teams \\ && \downarrow &pb& \downarrow \\ && actual\, teams &\to& poss.\, teams } \,,

where that top right entry can be formulated differently

possible players of possible teams = possible (players of teams).

Converse Barcan is a projected shadow of the inclusion of possible players of actual teams within possible (players of teams), i.e., possible players of possible teams. Only when all possible teams are actual teams do we have Barcan, that is, that every possibly player is a possible player of an actual team.

In view of the large philosophical literature on topics such as possible objects, there are opportunities for modal dependent type theory and philosophy to interact. One thing to work out would be how to think about modalities applied to the universe of types itself. Semantically, are we to imagine a collection of possible worlds over which the given types vary? We may want the base here to be a full \infinity-groupoid.

Posted at April 23, 2013 10:34 AM UTC

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

20 Comments & 0 Trackbacks

Re: Modal Types

Maybe I’m missing something really obvious here, but what about well known interpretation of “modal types” where modalities are taken to be type constructors (or type formation rules) satisfying functor, monad or comonad laws? This interpretation is discussed extensively on the modal logic and modal type theory pages at nLab, with references.

Posted by: John Smith on April 23, 2013 2:54 PM | Permalink | Reply to this

Re: Modal Types

Which is why I specifically linked to modal type theory and said that computer scientists work on such matters.

My (evidently unclear) point was that philosophers don’t talk about modal operators applied to types.

Posted by: David Corfield on April 23, 2013 3:05 PM | Permalink | Reply to this

Re: Modal Types

Hmm. I was under the impression that modal type theories and set theories were relatively well-studied, via the connection between Kripke models and presheaf categories. That is, you can view a Kripke structure (or any partial order, really) 𝕎=(W,)\mathbb{W} = (W, \leq) as a category, and then take the presheaf category 𝕎Set\mathbb{W} \to \mathrm{Set} to give an interpretation for “WW-varying sets”.

For example, I’ve used the presheaf category Set\mathbb{N} \to \mathrm{Set} to model “time-varying sets”, letting me interpret programming languages with type operators controlling when different computations occur. This naturally gives rise to a variety of modalities on sets corresponding to the propositional operators in temporal logic. This is all a fairly mechanical generalization of Kripke models, and IMO shouldn’t be viewed as giving a foundational type-theoretic account of modal logic. (OTOH, the fact that you can turn the crank to get a result makes it very easy to use!)

If you’re more interested in that direction, I would recommend something like Pfenning and Davies’ A Judgemental Reconstruction of Modal Logic, which takes Per Martin-Löf’s judgmental methodology, and extends it with new judgements corresponding to modal qualifications, and then shows how the modal operators arise as internalizations of these judgements.

Posted by: Neel Krishnaswami on April 23, 2013 2:58 PM | Permalink | Reply to this

Re: Modal Types

I’m not quite sure what point of mine you’re addressing in your first two paragraphs. I dare say there may even be a handful of philosophers who know of Kripke models as presheaves. But what does this have to do their knowing about modal type theory, or about trying to understand ordinary language statements in its terms?

Or do I get things wrong? Do you and Pfenning and Davies see yourselves as doing a kind of philosophy? Maybe disciplinary boundaries are murky if Martin-Löf is a philosopher and logician, and you work in his area? If so, perhaps some of you would propose yourselves to write some material on dependent type theory, modal type theory, etc. for SEP, where it’s sorely lacking.

Anyway, looking at your suggestion A Judgemental Reconstruction of Modal Logic, aren’t modalities only applied here to propositions? Or are we working here with what Mike called

Any type can be a proposition?

But then I’d be more interested in any work in the “only some types can be propositions” tradition.

Posted by: David Corfield on April 23, 2013 5:11 PM | Permalink | Reply to this

Re: Modal Types

  1. I had assumed that using presheaves to interpret set theories was “common currency”, mainly because casual Googling had show me things like John L. Bell’s advocacy of the “causal sets” approach to the philosophy of spacetime (see Causal Sets and Frame-Valued Set Theory), and since the Wikipedia article on Kripke frames suggests the connection is widely-known.

    That, plus the fact that a huge fraction of the work on modal logic is done in philosophy departments, led me to assume that this connection was well-known to philosophers, too. It’s surprising that it’s not, but then, I’ve been surprised before! :)

  2. Yes, Pfenning works with a props-as-types perspective.

    I don’t know if he’s put this into print, but in lectures I’ve heard him explain the judgmental methodology in explicitly philosophical terms: in particular, he sees it as a revival of the older Aristotelian view of logic (i.e., with multiple categories of statement), in contrast with the newer Fregean, truth-functional view.

Posted by: Neel Krishnaswami on April 23, 2013 5:56 PM | Permalink | Reply to this

Re: Modal Types

Boundaries are clearly not sharp. I would have John Bell placed more as a logician. What I can say is that your typical mainstream Anglo-American analytic metaphysician who employs modal logic does not think in terms of monads or presheaves.

Case in point, Oxford University’s Wykeham Professor of Logic, Timothy Williamson, who has just published Modal Logic as Metaphysics.

Let me just take the chance to shock Mike Shulman (here) by quoting the blurb:

Are there such things as merely possible people, who would have lived if our ancestors had acted differently? Are there future people, who have not yet been conceived? Questions like those raise deep issues about both the nature of being and its logical relations with contingency and change. In Modal Logic as Metaphysics, Timothy Williamson argues for positive answers to those questions on the basis of an integrated approach to the issues, applying the technical resources of modal logic to provide structural cores for metaphysical theories. He rejects the search for a metaphysically neutral logic as futile. The book contains detailed historical discussion of how the metaphysical issues emerged in the twentieth century development of quantified modal logic, through the work of such figures as Rudolf Carnap, Ruth Barcan Marcus, Arthur Prior, and Saul Kripke. It proposes higher-order modal logic as a new setting in which to resolve such metaphysical questions scientifically, by the construction of systematic logical theories embodying rival answers and their comparison by normal scientific standards. Williamson provides both a rigorous introduction to the technical background needed to understand metaphysical questions in quantified modal logic and an extended argument for controversial, provocative answers to them. He gives original, precise treatments of topics including the relation between logic and metaphysics, the methodology of theory choice in philosophy, the nature of possible worlds and their role in semantics, plural quantification compared to quantification into predicate position, communication across metaphysical disagreement, and problems for truthmaker theory.

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

Re: Modal Types

Here’s an extract from an interview with Timothy Williamson which has a bearing on my post.

PA: …Two modal principles that stand out as crucial in your view of modal metaphysics is the Barcan formula (BF) and its converse (CBF). In their existential version, they may be stated as follows.

BF xAxA\,\diamond \exists x A \to \exists x \diamond A

CBF xAxA\,\exists x \diamond A \to \diamond \exists x A

The claim BF reads informally as saying that ‘If there could have been something that met the condition AA, then there is something that could have met condition AA’, and the claim CBF reads with the opposite direction. If BF is true, the everything that could have existed must in some sense already exist. One motivation for rejecting BF is that, on many understandings of the sense of ‘exist’, it contains a metaphysical commitment that is highly implausible. How can the Barcan formulas be reconciled with or improve on our intuitions about existence?

TW: The first thing we need to do is to distinguish between material existence and existence in general. Numbers may be an example of things that exist without having material existence. By existence I mean ‘being something or other’. What is overwhelmingly plausible is that it is contingent what material things there are. There could have been more or fewer material things than there in fact are. That is consistent with BF and CBF, because it is consistent with the idea that if, for example, the table we’re sitting at had not been material it would still have been something. It would just not have been something material. Initially, that sounds like a strange claim, and the immediate question is: well, what would it have been? I’m not talking about the table as being a collection scattered atoms. That is still something material, and even those atoms might never have been. What I’m suggesting is that if there had been no such table and no such atoms, there would still have been a possible table, in other words, something that could have been a table and that could have been a material thing. But in those circumstances, it would not have been material, it would not have been a table, and so it would not have been located in space and time. It would have been a merely possible table, a merely possible material thing. Once we see that that is what BF and CBF is claiming, when they are understood with the quantifiers completely unrestricted and not limited to material things, it is much less obvious that there is any inconsistency between what those formulas are committing us to and what common sense is in any position to assert or have any special authority over. It seems that scientifically informed common sense may have some authority over what materially and contingent things there are, but once the question is what merely possible material things there are, that sort of abstract questions is not to be decided by common sense. That question is to be decided by systematic theory. Of course, it is not at all obvious such theoretical considerations themselves will favour BF and CBF, but what I have tried to argue in a series of works is that in fact they do. When we try to develop a systematic theory of metaphysics of quantified modal logic, we get into a mess unless we accept BF and CBF. So, in the end, we are driven, not by some immediately intuitive consideration, but by considerations of the needs of systematic theory into accepting these formulas.

It’s a very foreign philosophical tradition from mine. Where does the idea come from that completely unrestricted quantification is meaningful?

And yet, the abstract speculations of a Barcan have bumped up against subtle issues about monads preserving pullbacks so that fiberwise closure works as it should, which is needed for cohesive homotopy type theory to do its job in physics.

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

Re: Modal Types

If we take modal logic as talking about how things are in possible worlds, why not just treat worlds as a new type:

world:Type? world: Type?

Then possibility and necessity just involves quantification over worlds.

But if quantification is a projection from dependent sum and product, why not look at the full picture of dependency over worlds? So we might form types like

w:world c:C(w)F(c), \sum_{w:world} \sum_{c:C(w)} F(c),

for some world-dependent type CC. We might have, say, C(w)C(w) the cats in world ww, and F(c)F(c) the fleas on cat cc. So then dependent sum list triples world,cat,flea\langle world, cat, flea \rangle, the bracket type of which is the proposition asserting the possibility that some cat has a flea.

So what then is introducing modality to (homotopy) dependent type theory? Isn’t it just semantically the provision of an ultimate base space of worlds?

But then in quantified modal logic we allow the modality to occur after a quantifier, so not only do we have

Possibly some cat has a flea,

but also

Some cat possibly has a flea.

This latter seems to involve the notion that a particular cat in our world, say Tibbles, exists spread out over the worlds, or that it has a counterpart in each other world. So saying ‘Tibbles possibly has a flea’ means that Tibbles in at least one world has a flea.

If you read the metaphysical literature, these are rival options: Modal counterpart theory has each object confined to a world, but with counterparts in different worlds, while Modal dimensionalism has each object defined not only as a region of space-time, but also as spread out over modal dimensions.

Modal counterpart theory, it seems to me, fits best with a notion of fibration, where to a path in the space of worlds and an object in the world at one end of the path, there corresponds a ‘lift’ to an object in the world at the other end. Of course, one may then have different counterparts in the same world – think of the boundary of a Moebius strip, and the two counterparts of a point belonging to it, depending on whether we move a half turn clockwise or anticlockwise over the base space. So a point is a counterpart of the other point in the same fibre. Were there a global section, at least we could individuate objects.

Perhaps in the case of modal dimensionalism, we just pick out a subspace of the total space. In any case, you see why sheaves appear so prominently in Awodey and Kishida’s work.

Have we lost sight of the (co)monadic aspect of modality? In the different varieties of modal logic, reaching S4 where PP\diamond \diamond P \to \diamond P and PPP \to \diamond P hold is a big deal. These conditions correspond to conditions on the way the possible worlds are glued together, here transitivity and reflexivity. Perhaps the full story will need us to modalise directed homotopy type theory.

Posted by: David Corfield on April 25, 2013 10:00 AM | Permalink | Reply to this

Re: Modal Types

Does the interpretation of x:Ax:\diamond A as “xx is a possible AA” faithfully extend the usual propositional meaning of \diamond via propositions-as-types? That is, if PP is a proposition regarded as a type, then we regard x:Px:P as meaning “xx is a proof of PP” — is it the same thing to say that

  • xx is a possible proof of PP and that
  • xx is a proof of “possibly PP

?

Posted by: Mike Shulman on April 25, 2013 7:52 PM | Permalink | Reply to this

Re: Modal Types

I wouldn’t think so. Isn’t

x\,\,\,\,x is a possible proof of PP

like taking the judgement x:Px: P as a type and trying to apply \diamond to it?

Don’t modalities only apply to types?

Posted by: David Corfield on April 25, 2013 9:57 PM | Permalink | Reply to this

Re: Modal Types

It sounded to me like you’re suggesting that for a general type AA, the judgment x:Ax:\diamond A could be pronounced as “xx is a possible element of AA”. I’m not sure exactly what that means, but if so, then it should apply also when “elements of AA” have another more common name. For instance, x:x:\diamond \mathbb{R} would be “xx is a possible real number”. And when AA is the type representing a proposition PP, the more common name for elements of AA is “proofs of PP”; thus the judgment x:Ax:\diamond A ought to be pronounced as “xx is a possible proof of PP”.

If instead we considered a modality operating at the meta-theoretic level, we could consider a judgment like (x:A)\diamond (x:A), but it seems that that would be pronounced instead as “it is possible that xx is an element of AA”. I also don’t know how that would be related to “xx is a possible element of AA”.

Posted by: Mike Shulman on April 25, 2013 10:06 PM | Permalink | Reply to this

Re: Modal Types

I suppose it seems weird looking for an interpretation of a possible proof or real in the context of ‘metaphysical modalities’ whatever they are, when they don’t appear to be the kinds of thing that could change with variation over worlds.

Epistemically, it wouldn’t be so bad to have ‘so far as I know, this root of a polynomial could be a real number’. Then I guess after Wiles announced his first proof of FLT, people were saying it was a possible proof.

Posted by: David Corfield on April 25, 2013 10:57 PM | Permalink | Reply to this

Re: Modal Types

I just figured out how to explain the judgmental approach in categorical terms, at least for simple types. Thanks for making me think about this.

In the judgmental approach to modal type theory, we view modal types A\Diamond A as internalizations of categories of judgment.

That is, in Martin-Löf’s judgmental methodology, we take the assertionPP is true”, and then introduce a judgement of “PP is true”, which explains what constitutes evidence for PP (the introduction rules), and how to use a PP (the elimination rules). We can extend this to modalities by introducing new judgements to represent new categories of assertion. So in addition to “PP is true”, we might also have categories of judgment such as “PP is known to XX”, “PP will eventually be true”, “PP is possible”, and so on. Then, a modal type like A\Diamond A is an internalization of a judgement. That is, we can say that the introduction rule for the judgement “A\Diamond A is true”, is actually evidence for the judgement “AA is possible”.

In categorical proof theory, we typically take a judgement to be a category \mathbb{C}, with the types represented by the objects of \mathbb{C}, derivations of judgements given by morphisms f:ΓAf : \Gamma \to A (with the context Γ\Gamma represented by some kind of tensor product), and type constructors interpreted by (possibly nn-ary and contravariant) endofunctors T:T : \mathbb{C} \to \mathbb{C}.

To extend this to judgmental modal type theory, we can introduce categories ,𝔻\mathbb{C}, \mathbb{D} and so on for each category of judgment, and then take type constructors to be functors between these different categories. This makes the appearance of monads and comonads in modal type theory very natural. In some sense, adjoint functors give an “optimal” way of relating different categories, and composing a pair of adjoint functors gives you a comonad or monad, depending on which way around you go.

As a concrete example, take \mathbb{C} to be the category of predomains and continuous functions, and 𝔻\mathbb{D} to be the category of pointed domains and strict continuous functions. Then, we can interpret morphisms of \mathbb{C} as proofs that a proposition is true, and 𝔻\mathbb{D} as “possible proofs”. That is, 𝔻\mathbb{D} supports unrestricted recursion (has a natural transformation 𝕗𝕚𝕩 A:(AA)A\mathbb{fix}_A : (A \Rightarrow A) \to A), and so non-normalizing terms can be defined, by taking fixed points that don’t decrease along a well-order.

If you move back to model theory, all this is is a way of saying that models are lattices, and modal operators come via monotone functions between lattices and Galois connections. This all makes me feel that some variant of the Stone representation theorem should enable you to produce worlds and Kripke models from this “point-free” account of modal logic.

Posted by: Neel Krishnaswami on May 2, 2013 9:39 AM | Permalink | Reply to this

Re: Modal Types

This seems in accord with Curry’s idea, as described by Fairtlough and Mendler:

Curry’s proposal was to take ϕ\bigcirc \phi as the statement “in some stronger (outer) theory, ϕ\phi holds”. As examples of such nested systems of reasoning (with two levels) he suggested Mathematics as the inner and Physics as the outer system, or Physics as the inner system and Biology as the Outer. In both examples the outer system is more encompassing than the inner system where reasoning follows a more rigid notion of truth and deduction. The modality \bigcirc, which Curry Conceived of as a modality of possibility, is a way of reflecting the relaxed, outer notion of truth within the inner system. (On the Logical Content of Computational Type Theory: A Solution to Curry’s Problem)

Posted by: David Corfield on January 13, 2014 9:49 AM | Permalink | Reply to this

Re: Modal Types

So your \mathbb{C} and 𝔻\mathbb{D} are like the Grpd\infty-Grpd and H\mathbf{H} of the cohesive modalities?

I wonder if with this idea of categories of judgement we can make any sense of Peirce’s gamma graphs and the idea of asserting propositions on phemic sheets (see, e.g., here or here).

Posted by: David Corfield on May 2, 2013 10:22 AM | Permalink | Reply to this

Re: Modal Types

Regarding your thought on model theory, is that the same as doing what the coalgebra people do in forming a duality between modal algebras on Boolean algebras and coalgebras on Stone spaces, but now on the Forssell-Awodey Stone duality between first-order theories and Stone groupoids of models, as I suggested back here?

Posted by: David Corfield on May 2, 2013 1:00 PM | Permalink | Reply to this

Re: Modal Types

Cute!

Posted by: Mike Shulman on May 2, 2013 9:21 PM | Permalink | Reply to this

Re: Modal Types

Thinking of dependent types, I may not know for sure someone’s nationality. Karen is a possible citizen of Norway, hence, since I think Norway a possible EU country, as far as I know she is a possible EU citizen.

This doesn’t seem right to me. If I knew that Karen was not an EU citizen, that wouldn’t necessarily tell me whether it was because she wasn’t a Norwegian or because Norway wasn’t EU.

Posted by: Jay Doe on May 2, 2013 11:49 PM | Permalink | Reply to this

Re: Modal Types

Is your thought that I need to know more than the possibility of AA and the possibility of BB to conclude from ABCA \wedge B \to C the possibility of CC, i.e., that I need to know that ABA \wedge B is possible?

You give me a number chosen at random from 10 to 100, it might be even, it might prime, but it can’t be both.

Were I to run the Karen story with possible worlds, there may be worlds in which Karen is Norwegian, but there Norway is not in the EU, and there may be worlds where Norway is in the EU, but Karen is not Norwegian.

I see. Back to the drawing board.

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

Re: Modal Types

I guess naming Karen and Norway complicates the issues here, since then we have to have settled on our policy on counterparts. I was tempted to call Karen a possible EU citizen, because she is a member of the counterpart of Norway in some world, and the counterpart of Norway in some (possibly different) world is in the EU. It seems we might say she’s a possible citizen of a possible EU country.

But I see that attraction of not allowing this, and pegging a world down once only. So a possible cat’s flea has us cite a world, a cat in that world, and a flea on that cat in that world, and we don’t mean anything more by a possible cat’s possible flea.

Now I remember, this issue came up on the nForum in Mike’s response to my comment.

Posted by: David Corfield on May 3, 2013 10:13 AM | Permalink | Reply to this

Post a New Comment