## November 18, 2018

### Modal Types Revisited

#### Posted by David Corfield

We’ve discussed the prospects for adding modalities to type theory for many a year, e.g., here at the Café back at Modal Types, and frequently at the nLab. So now I’ve written up some thoughts on what philosophy might make of modal types in this preprint. My debt to the people who helped work out these ideas will be acknowledged when I publish the book.

This is to be the fourth chapter of a book which provides reasons for philosophy to embrace modal homotopy type theory. The book takes in order the components: types, dependency, homotopy, and finally modality.

The chapter ends all too briefly with mention of Mike Shulman et al.’s project, which he described in his post – What Is an n-Theory?. I’m convinced this is the way to go.

PS. I already know of the typo on line 8 of page 4.

Posted at November 18, 2018 9:14 AM UTC

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

### Re: Modal Types Revisited

This is very nice! I’m about halfway through it. I really like the replacement of global “possible worlds” (which I could never really make sense of metaphysically) by a local “domain of variation” or “implicitly understood collection of relevant situations” for every usage of modalities like “necessary” and “possible” in natural language.

One suggestion: I found the notation on p13 to be kind of confusing. You seem to be using “$7(w)$” to denote the “function which sends any argument $w$ to the constant $7$”, which is the opposite of the usual convention by which $f$ denotes a function and $f(x)$ denotes its value at an argument $x$. I had trouble even parsing the more complicated constructions like $\Box_W(8(w)\gt 7(w))(w)$ — is this supposed to mean $\Box_W((8(w)\gt 7(w))(w))$ or $(\Box_W(8(w)\gt 7(w)))(w)$? Do both of those even make sense? What do they mean? In “(the number of planets$(w) \gt 7(w))(a)$” do the two $(w)$s denote simply “making something a function” while the $(a)$ ambiguously denotes evaluating a function at a point $a$?

I suggest a notation for making functions that is different from the notation for evaluating functions. Would your intended audience be able to deal with $\lambda$-notation? If “the number of planets” is implicitly considered a function of world, then the latter example could be written “(the number of planets $\gt_W (\lambda w.7))(a)$” (where $\gt_W$ denotes the pointwise application of $\gt$ to functions), which I find much clearer, and which can be $\beta$-reduced to “(the number of planets)$(a) \gt (\lambda w.7)(a) = 7$”.

Posted by: Mike Shulman on November 19, 2018 1:14 PM | Permalink | Reply to this

### Re: Modal Types Revisited

Ah good, thanks. I was having doubts about that notation.

More to add to the acknowledgements of your contribution – you will shortly come across the account of temporal types that you initiated.

I’m increasingly thinking the idea here of variation leading to a form of modality can be made to fit well with Robert Brandom’s research program. This program looks to understand vocabularies in which it is possible to express, or ‘make explicit’, what it is to use other more basic vocabularies. So one of his examples is that modal vocabulary makes explicit what we do in ordinary empirical descriptive practices of assertion under counterfactual modification.

Another case is the use of talk of ‘implies’ and ‘hypothetical’ as making explicit usage of these same empirical descriptive vocabularies. Perhaps a category-theoretic expression of this case is the passage from a deductive system to its associated cartesian closure. In the richer latter language we now have exponential objects, whose elements include hypotheticals.

In sum, there’s some mileage to be had from those internalizations of judgmental structure.

Posted by: David Corfield on November 19, 2018 3:39 PM | Permalink | Reply to this

### Re: Modal Types Revisited

Although, the “local domain of variation” perspective does make me wonder whether it still makes sense to regard “necessarily” and “possibly” as endomorphisms of propositions. Maybe it would make more sense to regard them as “implicit quantifiers” over the appropriate domain of variation. So for instance “this emerald is necessarily green” would be essentially syntactic sugar for “here is an emerald, and all emeralds are green”.

Posted by: Mike Shulman on November 19, 2018 6:10 PM | Permalink | Reply to this

### Re: Modal Types Revisited

I think this fits well with what Brandom takes from Wilfred Sellars’ deflationary account of modality as concerning ranges of counterfactual robustness’.

In the anti-metaphysical heyday of the Vienna Circle and logical empiricism, modalities were to be treated with great suspicion. Things were turned on their head in the last third of the 20th century with the flourishing of possible worlds treatments.

Sellars and Brandom are offering us a way to understand our modal talk as making explicit aspects of the inferential network in which what appear to be simple empirical claims sit. Someone asserts That is an oak tree’ and we know they’re committed to that still being the case were it to start to rain, were the neighbouring beech tree to be cut down, were a bear to climb it, but not were it to have grown from a conker.

To be in the game of making even simple assertions, you’re already someone who understands invariance under counterfactual change.

Posted by: David Corfield on November 20, 2018 8:33 AM | Permalink | Reply to this

### Re: Modal Types Revisited

Your MathOverflow answer here is part of this story of providing a constant standard to allow comparison over variation.

Posted by: David Corfield on November 20, 2018 11:00 AM | Permalink | Reply to this

### Re: Modal Types Revisited

I also really like the idea of necessary elements of types as “essential characteristics” on p15:

An element generated in such a way might be said to refer to an essential characteristic of a dog. If I point to the front right leg of a dog and show you another dog, you will probably choose the same leg. It might be holding this paw in the air, so you could have chosen the left rear leg of the second dog who is cocking this now at a lamp post, but it does seem that the same element of the body plan is the most reasonable choice.

It reminds me of some psychological research I’ve encountered on the way even children intuitively generalize in some ways in preference to others. I don’t have any actual citations to point to (maybe some bystander can supply some); my “encounter” consisted of a 5-minute research study that my 4-year-old son participated in at our local science museum.

I don’t remember the details exactly, but I think the researcher had some collection of objects that varied along two axes, maybe size and color, and the kid’s job was to sort them according to whether they made a light bulb (secretly controlled by the experimenter) light up when placed in front of it. For each object the kid was asked first what they thought it would do and why, before placing it in front of the bulb and putting it in the correct pile and then explaining why it behaved that way. I think the actual pattern was that the green objects made the bulb light up and the blue ones didn’t, but supposedly a lot of young children have a deeply embedded idea that “larger things are more effective” which they maintain in the face of evidence that in this case it’s the color rather than the size that matters. Or maybe the other way around?

Anyway, it occurred to me that you could describe what is happening as the children incorrectly guessing the appropriate map with respect to which the modalities should be defined. In your example, when pointing to the right front leg of a dog and asking me to point to the “same” leg of another dog, our experience with the world suggests that it is more useful to consider Fido’s legs as pulled back along $Animal \to Species$ than as pulled back along $Animal \to AnimalWithOneLegInTheAir$. (For instance, one reason for this is that the former map is fiberwise over $Time$ whereas the latter isn’t.) But a hypothetical alien or visitor from another dimension might not be trained to make the same assumption.

Minor comment: I was briefly a bit confused by the introduction of the map $spec : Animal \to Species$ in the middle of page 15, since it seemed like it was introducing something new, but we had already been talking about this map before. Of course soon I realized you were just giving a name at last to this map which had not been previously named. But it might be clearer to name this map when it is first introduced back on p14.

Posted by: Mike Shulman on November 19, 2018 8:48 PM | Permalink | Reply to this

### Re: Modal Types Revisited

I remember from writing my health book that researchers had shown that size and colour of a sugar pill make a difference for its effectiveness. Apparently small and red is good. But then a saline injection generally trumps any pill.

Thanks again for the suggestion to clarify.

Posted by: David Corfield on November 20, 2018 8:14 AM | Permalink | Reply to this

### Re: Modal Types Revisited

The example with dogs and paws reminds me of another one, which always made me curious: mirrors.

We commonly think that mirrors reverse left and right. Now clearly if we refer to “left and right” as spatial orientations, in the sense of “determinants”, this is correct.

However, we seem also to think that mirrors reverse left and right as directions, which is of course not true. (For example, why would a mirror reverse left and right, but not top and bottom?) One of the directions (or all three) clearly has to be reversed if we want the orientation to be reversed, and this direction is front-back: what is “forward” for me is “backward” for the me-in-the-mirror. Not left-right. The only reason why we think that mirrors reverse the left-right axis is that we are used to have (non-mirrored) people standing in front of us. Compared to these people, a person in the mirror has left and right inverted.

Which hand is the right hand of the person in the mirror?

Posted by: Paolo Perrone on November 20, 2018 2:57 PM | Permalink | Reply to this

### Re: Modal Types Revisited

Maybe a case for the treatment via a context which is a looped group, which is where we can study types under actions. It only appears briefly in this chapter, but at greater length in the preprint mention as forming the previous chapter.

I wonder whether one could make more of the connection between necessity and group invariance. Objects seem real to us by their images varying in the right way as we move, factoring out our own movement.

Posted by: David Corfield on November 20, 2018 7:12 PM | Permalink | Reply to this

Post a New Comment