# Start a new discussion

## Not signed in

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

## Discussion Tag Cloud

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

• 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)$, to be dependent on a collection of worlds $W$, 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 $W$ to be a groupoid, or we represent the accessibility relation $W \to W'$.

• CommentRowNumber4.
• CommentAuthorDavid_Corfield
• CommentTimeJun 13th 2016

Coming back to this, it suggests having a type base changed along $W \times X \to X$, so $\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

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

• de re if it is the other way around

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

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

$(\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 $\Box \underset{x \colon X}{\exists} A(x)$ that we have a world-dependent type $X(w)$, and then put $\Box_W \underset{x \colon X(w)}{\exists} A(w, x)$. But this $A$ is a dependent type $w: W, x:X(w) \vdash A(w, x):Prop$.

However, de re, I need to have world-independent $X$, to allow the modal operator $\Box_W: \mathbf{H}/(X \times W) \to \mathbf{H}/(X \times W)$ and then $\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.