Modal Types

Modal Types:

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)).

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 singles out those terms of type A 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:⋄EU⋄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 ∃⋄ and ⋄∃.

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→¬¬P was acceptable but not the converse. Behind the scenes, the former is natural, arising from currying the evaluation of an exponential (B A×A→B, where B 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.

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

playersofactualteams ↘ poss.playersofactualteams → poss.playersofposs.teams ↓ pb ↓ actualteams → 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 ∞-groupoid.

DIGITAL JUICE