David Corfield
Modal logic


Propositional modal logic

Layer 1 Descriptive general frame Stone space Boolean algebra Modal algebra

First-order modal logic

Layer 1 Boolean Hyperdoctrine Modal Hyperdoctrine Syntactic category Modal Syntactic category Stone groupoid of models Indexed Stone spaces Indexed descriptive general frames a b c d <image height='100' width='100' x='0' y='0'></image>

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?

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

x:XA(x) \diamond \sum_{x \colon X} A(x)


x:XA(x). \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


Last revised on May 24, 2013 at 12:08:32. See the history of this page for a list of all contributions to it.