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

  • I believe that the person downstairs is my mother

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

  • Someone is necessarily the monarch of this country

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

  • de dicto if the modal operator is applied after the quantifier

    x:XA(x)\Box \underset{x \colon X}{\exists} A(x);

  • de re if it is the other way around

    x:XA(x)\underset{x \colon X}{\exists} \Box A(x);

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

  • Michael Makkai, Gonzalo Reyes, section 4 of Completeness results for intuitionistic and modal logic in a categorical setting, Annals of Pure and Applied Logic 72 (1995) 25-101

Related comments are in

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

  • Gianluca Giorgolo, Ash Asudeh, Monads as a Solution for Generalized Opacity, Proceedings of the EACL 2014 Workshop on Type Theory and Natural Language Semantics (TTNLS), pp. 19-27. (pdf)

.

Last revised on September 29, 2016 at 06:13:49. See the history of this page for a list of all contributions to it.