David Corfield Modal logic

Propositional modal logic

First-order modal logic

Syntactic side: Modal syntactic category in Makkai and Reyes, modal hyperdoctrine, Ghilardi and Meloni?

Semantic side: Metaframes, counterpart frames, coherence frames (Kracht&Kutz, Shehtman/Skvortsov, Shirasu). Where do ionads (Richard Garner) and sheaf semantics (Awodey-Kishida) feature?

In hyperdoctrine picture, on syntax side map type to terminal induces injection of closed sentences into propositions free in variables of type; on semantics side corrsponding map induces fibring of entities of that type over their respective worlds.

Horizontal relations: (a) Awodey-Forssell, (b)??, (c) Dion Coumans slides

Question: Do we gain generality in the top layer, so avoid the need for monadic modalities?

Modal homotopy type theory

There should be an account of modal homotopy type theory which projects to ordinary modal logic.

Is there some idea with modal type theory to think about its version of the Barcan formula

$$\Diamond \exists \to \exists \Diamond?$$

For example, we could compare

$$\diamond \sum_{x \colon X} A(x)$$

and

$$\sum_{x \colon X} \Diamond A(x).$$

If $\Diamond$ were truncation to Prop, the former is a further projection of the latter, suggesting converse Barcan holds, but Barcan doesn’t.

But it would be nice to illustrate things using the language of possibility. If the dependent type represents players for a Premiership team, we could talk of a possible Premiership player and some Premiership team’s possible player, the latter being more informative as evidence would require that the team be mentioned.

Blog posts

I, II, III, IV.