Modal Types

April 23, 2013

Posted by David Corfield

$MathML-enabled post (click for more details).$

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’ ( $\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.

$MathML-enabled post (click for more details).$

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 $\Box 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

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

$\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 \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 \times A \to 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

$\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:

$\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: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2614

23 Comments & 0 Trackbacks

Re: Modal Types

$MathML-enabled post (click for more details).$

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

$MathML-enabled post (click for more details).$

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

$MathML-enabled post (click for more details).$

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) $\mathbb{W} = (W, \leq)$ as a category, and then take the presheaf category $\mathbb{W} \to \mathrm{Set}$ to give an interpretation for “ $W$ -varying sets”.

For example, I’ve used the presheaf category $\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

$MathML-enabled post (click for more details).$

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

$MathML-enabled post (click for more details).$

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! :)
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

$MathML-enabled post (click for more details).$

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

$MathML-enabled post (click for more details).$

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 $\,\diamond \exists x A \to \exists x \diamond A$

CBF $\,\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 $A$ , then there is something that could have met condition $A$ ’, 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

$MathML-enabled post (click for more details).$

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?$

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

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

for some world-dependent type $C$ . We might have, say, $C(w)$ the cats in world $w$ , and $F(c)$ the fleas on cat $c$ . So then dependent sum list triples $\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 $\diamond \diamond P \to \diamond P$ and $P \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

$MathML-enabled post (click for more details).$

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

$x$ is a possible proof of $P$ and that
$x$ is a proof of “possibly $P$ ”

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

Re: Modal Types

$MathML-enabled post (click for more details).$

I wouldn’t think so. Isn’t

$\,\,\,\,x$ is a possible proof of $P$

like taking the judgement $x: 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

$MathML-enabled post (click for more details).$

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

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

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

Re: Modal Types

$MathML-enabled post (click for more details).$

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

$MathML-enabled post (click for more details).$

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 $\Diamond A$ as internalizations of categories of judgment.

That is, in Martin-Löf’s judgmental methodology, we take the assertion “ $P$ is true”, and then introduce a judgement of “ $P$ is true”, which explains what constitutes evidence for $P$ (the introduction rules), and how to use a $P$ (the elimination rules). We can extend this to modalities by introducing new judgements to represent new categories of assertion. So in addition to “ $P$ is true”, we might also have categories of judgment such as “ $P$ is known to $X$ ”, “ $P$ will eventually be true”, “ $P$ is possible”, and so on. Then, a modal type like $\Diamond A$ is an internalization of a judgement. That is, we can say that the introduction rule for the judgement “ $\Diamond A$ is true”, is actually evidence for the judgement “ $A$ 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 : \Gamma \to A$ (with the context $\Gamma$ represented by some kind of tensor product), and type constructors interpreted by (possibly $n$ -ary and contravariant) endofunctors $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 $\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

$MathML-enabled post (click for more details).$

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

$MathML-enabled post (click for more details).$

So your $\mathbb{C}$ and $\mathbb{D}$ are like the $\infty-Grpd$ and $\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

$MathML-enabled post (click for more details).$

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

$MathML-enabled post (click for more details).$

Cute!

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

Re: Modal Types

$MathML-enabled post (click for more details).$

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

$MathML-enabled post (click for more details).$

Is your thought that I need to know more than the possibility of $A$ and the possibility of $B$ to conclude from $A \wedge B \to C$ the possibility of $C$ , i.e., that I need to know that $A \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

$MathML-enabled post (click for more details).$

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

Re: Modal Types

$MathML-enabled post (click for more details).$

What do you think about Justification Logic of Artemov and Fitting? I’m very interested in the exact relation between Justification Logic and Type Theory. Informed me please if someone has thoughts about this…

Posted by: Frank on January 9, 2018 4:47 AM | Permalink | Reply to this

Re: Modal Types

$MathML-enabled post (click for more details).$

Hi David, what an exciting article!

Speaking of your noun phrase ideas here, here is how I think of noun phrases in English (which converges on the same idea!). But it is far more inherent in grammar than you might think.

For context: theory is to model is as boolean algebra is to stone space (see “First-Order Logical Duality” by Steve Awodey and Henrick Forssel). Hom-ing with 2 goes back and forth between them.

Broadly, one could think of there as being two sorts of noun-phrase-like types in English. One is more like a collection, and another is more like an element. We might think of “bear” in the sentence “the bear eats honey” as being more like a set (much like the set of bears) and “the bear” as being more like an element (much like a particular bear contained in the set of bears). We could then hypothesize two fundamental types for noun phrases: “collections” [C] and “elements” [E]. (If this is our hypothesis, then in type theory based syntax, we should say that “the” has type lambda C.E as it takes collections like “bear” to elements like “the bear”). In general, if we suspect a singular noun such as “bear” (call it X) to be a collection-like, we can test by trying to put it in the sentence “a(n) X is a thing”, thing being essentially the largest set-like. If we have a (singular!) noun like “redness” we can test that it is an element like by putting it in the sentence “X is a thing”, without the “a”.

So “thing” is like the largest collection, and all elements are contained within it. “thing” is therefore the unit element in a boolean algebra, and element-type noun phrases are all “contained in thing”, in the way points are contained in a stone space.

Now for the magic: adjectives like “red” are of type lambda C.C. For instance, “ball” has type C and “red ball” has type C as well. “lambda x. red x” has an effect much like intersecting with “red thing”, and has all the formal properties of a comonad. The morphisms are given by set inclusion, and we can say x : C is contained in y : C when we can say “a(n) x is a(n) y” (singular nouns only- the problem with plural nouns is that english omits the plural article). So, for instance, “a red ball is a ball” (counit natural transformation), “a red ball is a red red ball” (comultiplication natural transformation). After some contemplation, most English adjectives are comonads, not monads.

Under this interpretation of noun phrases, what would the monads be? Often, when we find a comonad, we have already found the corresponding monad. For instance, “necessary (x)” means that “not possible (not x)”. “for all” means “not exists not”, “unfalsifiable” means “not verifiable that not”, etc. But I can’t seem to find what negation would be!

Posted by: Dean Young on December 24, 2019 12:53 AM | Permalink | Reply to this

Re: Modal Types

$MathML-enabled post (click for more details).$

Thanks for this, Dean. Later thinking appears in the article mentioned in a more recent post.

Something about the use of generic ‘the’ occurs in a chapter3 of my forthcoming book.

Posted by: David Corfield on January 3, 2020 3:02 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

April 23, 2013

Modal Types

Posted by David Corfield

23 Comments & 0 Trackbacks

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Access Keys:

The n-Category Café

Skip to the Main Content

April 23, 2013

Modal Types

Posted by David Corfield

Some Related Entries

23 Comments & 0 Trackbacks

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Re: Modal Types

Access Keys: