nLab
de re and de dicto

Contents

Idea

The de re/ de dicto distinction has different meanings, as explained in (SEP), but it typically concerns the two readings that are possible in sentences where a modal operator or propositional attitude verb is applied to a claim about some subject. For example, consider

The usual de dicto reading would express my strong hunch about the person who is downstairs that she is my mother. The de re reading would take the expression ‘the person downstairs’ to designate the person who is actually there, for example, it may in fact be my father. This would entail that I am crazy enough to believe my father to be my mother.

Similarly in the case of modal logic, we could consider a statement such as

De dicto this means that it has to be the case at this time that there be a monarch (as soon as one monarch dies, their successor becomes monarch). On the other hand, de re this means that some specific individual has to be monarch. This reading leads to a false claim since that person might in fact not have been monarch. They might, say, have abdicated earlier or have been killed by their uncle when a child.

Formalization in modal logic

In modal logic a proposition involving the consecutive application of a modal operator and an existential quantifier is called

Hence a difference between de dicto and de re statements is related to the failure of a modal operator to commute with base change.

However, according to the treatment at necessity and possibility, these modalities operate on world dependent types:

(WW)((W *w:W)(W *w:W)):H /WH /W. (\underset{W}{\lozenge} \dashv \underset{W}{\Box}) \coloneqq \left( \left( W^\ast \circ \underset{w\colon W}{\exists} \right) \dashv \left( W^\ast \circ \underset{w\colon W}{\forall} \right) \right) \;\colon\; \mathbf{H}_{/W} \longrightarrow \mathbf{H}_{/W} \,.

Then, de dicto, I could mean by x:XA(x)\Box \underset{x \colon X}{\exists} A(x) that we have a world-dependent type X(w)X(w), and then put Wx:X(w)A(w,x)\Box_W \underset{x \colon X(w)}{\exists} A(w, x). But this AA is a dependent type w:W,x:X(w)A(w,x):Propw: W, x:X(w) \vdash A(w, x):Prop.

However, de re, I need to have world-independent XX, to allow the modal operator W:H/(X×W)H/(X×W)\Box_W: \mathbf{H}/(X \times W) \to \mathbf{H}/(X \times W) and then x:X:H/(X×W)H/W\underset{x \colon X}{\exists}: \mathbf{H}/(X \times W) \to \mathbf{H}/W.

References

Detailed discussion of compatibility of modal operators with base change in a hyperdoctrine is in

Related comments are in

For an attempt to represent the kinds of opaque contexts considered here using the reader monad, see

.