Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: de dicto and de re

Bottom of Page

1 to 5 of 5

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2015
    • (edited Sep 4th 2015)

    started a minimum at de dicto and de re, mainly such as to have a place to point to section 4 of

    • Michael Makkai, Gonzalo Reyes, Completeness results for intuitionistic and modal logic in a categorical setting, Annals of Pure and Applied Logic 72 (1995) 25-101
    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 5th 2015

    I expanded this a bit,

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 6th 2015

    I think I’m still struggling with these quantifier-modal operator mixes, but maybe that’s because of the way I’d like to set things up.

    If we take a type, say People(w)People(w), to be dependent on a collection of worlds WW, then maybe we want to say that

    • Necessarily someone is oldest.

    So that’s fine read the de dicto way. The property of being oldest is world dependent. In each world there’s an oldest, so necessarily there’s an oldest person.

    Now the de re way, I need a notion of a person as existing across the worlds. This is why Awodey-Kishida have sheaves in their models.

    Perhaps we needed our WW to be a groupoid, or we represent the accessibility relation W→W′W \to W'.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 13th 2016

    Coming back to this, it suggests having a type base changed along W×X→XW \times X \to X, so H/X→H/X×W\mathbf{H}/X \to \mathbf{H}/X \times W to allow either order of quantifier and modality.

    ’Transworld identity’ keeps cropping up.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 13th 2016
    • (edited Sep 13th 2016)

    The worries in #3 and #4 are that what we have on this page is incompatible with necessity and possibility. So here we have:

    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:X□A(x)\underset{x \colon X}{\exists} \Box A(x);

    Where elsewhere we’ve set the modalities to work on world dependent types:

    (◊W⊣□W)≔((W *∘∃w:W)⊣(W *∘∀w:W)):H /W⟶H /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} \,.

    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 □ W∃x: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.

    So

    the failure of a modal operator to commute with base change

    is not quite so straightforward.

1 to 5 of 5

  1.