Contents

# Contents

## Idea

A modality in philosophy and formally in formal logic/type theory expresses a certain mode (or “moment” as in Hegel 12) of being.

### In philosophy

According to (Kant 1900) (see WP) the four “categories” are

1. Quantity

2. Quality

3. Relation

4. Modality

and the modalities contain the three pairs of opposites

### In formal logic

#### General

In formal logic and type theory modalities are formalized by modal operator or closure operator $\sharp$, that send propositions/types $X$ to new propositions/types $\sharp X$, satisfying some properties.

Adding such modalities to propositional logic or similar produces what is called modal logic. Here operators that are meant to formalize necessity and possibility (S4 modal logic) are maybe most famous. Adding modalities more generally to type theory yields modal type theory. See there for more details.

The categorical semantics of these modalities is that $\sharp$ is interpreted an idempotent monad/comonad on the category of contexts.

This has a refinement to homotopy type theory, where the categorical semantics of a higher modality or homotopy modality as an idempotent (infinity,1)-monad (Shulman 12, Rijke, Shulman, Spitters ).

#### Notation

Typical notation (e.g. SEP, Reyes 91, but not Hermida 10) is as follows:

• a co-modality represented by an idempotent comonad is typically denoted by $\Box$, following the traditional example of necessity in modal logic;

• a modality represented by an idempotent monad is typically denoted by $\lozenge$ or (less often) by $\bigcirc$, following the traditional example of possibility in modal logic.

When adjunctions between modalities matter (adjoint modalities), then some authors (Reyes 91, p. 367 RRZ 04, p. 116, Hermida 10, p.11) use $\lozenge$ for a left adjoint of a $\Box$. That leaves $\bigcirc$ as the natural choice of notation for a right adjoint (if any) of a $\Box$-modality.

This way for instance for cohesion with shape modality $\dashv$ flat comodality $\dashv$ sharp modality the generic notation would be:

$\array{ monad && comonad && monad \\ \lozenge &\dashv& \Box &\dashv& \bigcirc \\ \\ shape && flat && sharp \\ ʃ &\dashv& \flat &\dashv& \sharp }$

## References

### In formal logic

Discussion in formal logic and homotopy type theory (modal type theory):

### In philosopy

• Kant, AA III, 93– KrV B 106
• German Wikipedia, Modalität (Philosophie)

• Stanford Encyclopedia of Philosophy, Modal Logic

• Gonzalo Reyes, A topos-theoretic approach to reference and modality, Notre Dame J. Formal Logic Volume 32, Number 3 (1991), 359-391 (Euclid)

• Reyes/Reyes/Zolfaghari, Generic Figures and Their Glueings 2004, Polimetrica

• Claudio Hermida, section 3.3. of A categorical outlook on relational modalities and simulations, 2010 (pdf)

Last revised on July 7, 2019 at 09:01:35. See the history of this page for a list of all contributions to it.